theorem
proved
tactic proof
Jcost_cosh_add_identity
show as:
view Lean formalization →
formal statement (Lean)
60theorem Jcost_cosh_add_identity : CoshAddIdentity Cost.Jcost := by
proof body
Tactic-mode proof.
61 intro t u
62 simp only [G, Jcost]
63 -- Use exp(t+u) = exp(t)*exp(u) and exp(t-u) = exp(t)/exp(u)
64 have he1 : Real.exp (t + u) = Real.exp t * Real.exp u := Real.exp_add t u
65 have he2 : Real.exp (t - u) = Real.exp t / Real.exp u := by
66 rw [sub_eq_add_neg, Real.exp_add, Real.exp_neg]
67 ring
68 have hpos_t : Real.exp t > 0 := Real.exp_pos t
69 have hpos_u : Real.exp u > 0 := Real.exp_pos u
70 have hne_t : Real.exp t ≠ 0 := hpos_t.ne'
71 have hne_u : Real.exp u ≠ 0 := hpos_u.ne'
72 rw [he1, he2]
73 field_simp
74 ring
75