pith. machine review for the scientific record. sign in
theorem proved tactic proof

V_quadratic_at_origin

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  92theorem V_quadratic_at_origin (phi_inf : ℝ) (h : -1 < phi_inf) :
  93    V phi_inf * (2 * (1 + phi_inf)) = phi_inf ^ 2 := by

proof body

Tactic-mode proof.

  94  rw [V_eq_quadratic h]
  95  have h_pos : (0 : ℝ) < 1 + phi_inf := by linarith
  96  have h_ne : (1 : ℝ) + phi_inf ≠ 0 := ne_of_gt h_pos
  97  have h2_ne : (2 : ℝ) * (1 + phi_inf) ≠ 0 := by positivity
  98  field_simp [h_ne, h2_ne]
  99

depends on (4)

Lean names referenced from this declaration's body.