-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem isUnit_of_isUnit_leadingCoeff_AddUnitOrder {x : HahnSeries Γ R} (hx : IsUnit x.leadingCoeff)
    (hxo : IsAddUnit x.order) : IsUnit x

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
h' :
  (1 - (1 - (single hxo.addUnit.neg) i * x)) * (SummableFamily.powers (1 - (single hxo.addUnit.neg) i * x) ⋯).hsum = 1
⊢ IsUnit x

Tactic:
rw [sub_sub_cancel] at h'

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
h' : (single hxo.addUnit.neg) i * x * (SummableFamily.powers (1 - (single hxo.addUnit.neg) i * x) ⋯).hsum = 1
⊢ IsUnit x

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
h' : (single hxo.addUnit.neg) i * x * (SummableFamily.powers (1 - (single hxo.addUnit.neg) i * x) ⋯).hsum = 1
⊢ IsUnit x

Tactic:
exact isUnit_of_mul_isUnit_right (isUnit_of_mul_eq_one _ _ h')

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * u = 1
h : u = x.leadingCoeff
⊢ IsUnit x

Tactic:
rw [h] at iu

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
⊢ IsUnit x

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
⊢ IsUnit x

Tactic:
let ⟨⟨u, i, ui, iu⟩, h⟩ := hx

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * u = 1
h : ↑{ val := u, inv := i, val_inv := ui, inv_val := iu } = x.leadingCoeff
⊢ IsUnit x

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * u = 1
h : ↑{ val := u, inv := i, val_inv := ui, inv_val := iu } = x.leadingCoeff
⊢ IsUnit x

Tactic:
rw [Units.val_mk] at h

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * u = 1
h : u = x.leadingCoeff
⊢ IsUnit x

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
⊢ IsUnit x

Tactic:
have h' := SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu hxo)

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
h' :
  (1 - (1 - (single hxo.addUnit.neg) i * x)) * (SummableFamily.powers (1 - (single hxo.addUnit.neg) i * x) ⋯).hsum = 1
⊢ IsUnit x