lemma proved tactic proof

`sqrt5_lt_2_4`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  13private lemma sqrt5_lt_2_4 : Real.sqrt 5 < (2.4 : ℝ) := by

proof body

Tactic-mode proof.

  14  have h : (5 : ℝ) < 2.4^2 := by norm_num
  15  have h5_pos : (0 : ℝ) ≤ 5 := by norm_num
  16  have h2_4_pos : (0 : ℝ) ≤ 2.4 := by norm_num
  17  rw [← Real.sqrt_sq h2_4_pos]
  18  exact Real.sqrt_lt_sqrt h5_pos h
  19

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

phi_lt_1_7 in IndisputableMonolith.Support.PhiApprox decl_use