Theorem: PowerSeries.isExponential_self_mul_neg_eq_one (DividedPowers/ExponentialModule/Basic.lean)

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
⊢ f * scale (-1) f = 1
Tactic:
convert (isExponential_scale_add (1 : A) (-1 : A) hf).symm
State after:
case h.e'_2.h.e'_5
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
⊢ f = scale 1 f

case h.e'_3
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
⊢ 1 = scale (1 + -1) f

State before:
case h.e'_2.h.e'_5
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
⊢ f = scale 1 f
Tactic:
rw [scale_one, id_eq]
State after:
no goals

State before:
case h.e'_3
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
⊢ 1 = scale (1 + -1) f
Tactic:
simp only [add_right_neg, scale_zero_apply, hf.constantCoeff, map_one]
State after:
no goals