-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem isUnit_iff {x : HahnSeries Γ R} : IsUnit x ↔ IsUnit (x.leadingCoeff)

Proof state:
case mp.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ IsUnit (↑{ val := u, inv := i, val_inv := ui, inv_val := iu }).leadingCoeff

Tactic:
refine
  isUnit_of_mul_eq_one (u.leadingCoeff) (i.leadingCoeff)
    ((coeff_mul_order_add_order u i).symm.trans ?_)

Result:
case mp.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ (u * i).coeff (u.order + i.order) = 1

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
⊢ IsUnit x ↔ IsUnit x.leadingCoeff

Tactic:
constructor

Result:
case mp
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
⊢ IsUnit x → IsUnit x.leadingCoeff

case mpr
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
⊢ IsUnit x.leadingCoeff → IsUnit x

Proof state:
case mp
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
⊢ IsUnit x → IsUnit x.leadingCoeff

Tactic:
rintro ⟨⟨u, i, ui, iu⟩, rfl⟩

Result:
case mp.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ IsUnit (↑{ val := u, inv := i, val_inv := ui, inv_val := iu }).leadingCoeff

Proof state:
case mp.intro.mk.hc
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ u.order + i.order = 0

Tactic:
rw [← order_mul (left_ne_zero_of_mul_eq_one ui) (right_ne_zero_of_mul_eq_one ui), ui, order_one]

Result:
no goals

Proof state:
case mpr.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h : (single ⋯.addUnit.neg) i * x * (SummableFamily.powers (1 - (single ⋯.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:
case mpr.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * u = 1
hx : u = x.leadingCoeff
⊢ IsUnit x

Tactic:
rw [hx] at iu

Result:
case mpr.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
⊢ IsUnit x

Proof state:
case mpr.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h : (1 - (1 - (single ⋯.addUnit.neg) i * x)) * (SummableFamily.powers (1 - (single ⋯.addUnit.neg) i * x) ⋯).hsum = 1
⊢ IsUnit x

Tactic:
rw [sub_sub_cancel] at h

Result:
case mpr.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h : (single ⋯.addUnit.neg) i * x * (SummableFamily.powers (1 - (single ⋯.addUnit.neg) i * x) ⋯).hsum = 1
⊢ IsUnit x

Proof state:
case mpr
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
⊢ IsUnit x.leadingCoeff → IsUnit x

Tactic:
rintro ⟨⟨u, i, ui, iu⟩, hx⟩

Result:
case mpr.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * u = 1
hx : ↑{ val := u, inv := i, val_inv := ui, inv_val := iu } = x.leadingCoeff
⊢ IsUnit x

Proof state:
case mpr.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
⊢ IsUnit x

Tactic:
have h :=
  SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu (AddGroup.isAddUnit x.order))

Result:
case mpr.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h : (1 - (1 - (single ⋯.addUnit.neg) i * x)) * (SummableFamily.powers (1 - (single ⋯.addUnit.neg) i * x) ⋯).hsum = 1
⊢ IsUnit x

Proof state:
case mpr.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * u = 1
hx : ↑{ val := u, inv := i, val_inv := ui, inv_val := iu } = x.leadingCoeff
⊢ IsUnit x

Tactic:
rw [Units.val_mk] at hx

Result:
case mpr.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * u = 1
hx : u = x.leadingCoeff
⊢ IsUnit x

Proof state:
case mp.intro.mk
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ (u * i).coeff (u.order + i.order) = 1

Tactic:
rw [ui, coeff_one, if_pos]

Result:
case mp.intro.mk.hc
Γ : Type u_1
R : Type u_3
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ u.order + i.order = 0