case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
⊢ IsUnit x → IsUnit (coeff x (order x))

case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
⊢ IsUnit (coeff x (order x)) → IsUnit x
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
⊢ IsUnit x ↔ IsUnit (coeff x (order x))
constructor
case mp.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ IsUnit
    (coeff (↑{ val := u, inv := i, val_inv := ui, inv_val := iu })
      (order ↑{ val := u, inv := i, val_inv := ui, inv_val := iu }))
case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
⊢ IsUnit x → IsUnit (coeff x (order x))
rintro ⟨⟨u, i, ui, iu⟩, rfl⟩
case mp.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ coeff (u * i) (order u + order i) = 1
case mp.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ IsUnit
    (coeff (↑{ val := u, inv := i, val_inv := ui, inv_val := iu })
      (order ↑{ val := u, inv := i, val_inv := ui, inv_val := iu }))
refine'
  isUnit_of_mul_eq_one (u.coeff u.order) (i.coeff i.order)
    ((mul_coeff_order_add_order u i).symm.trans _)
case mp.intro.mk.hc
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ order u + order i = 0
case mp.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ coeff (u * i) (order u + order i) = 1
rw [ui, one_coeff, if_pos]
no goals
case mp.intro.mk.hc
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
u i : HahnSeries Γ R
ui : u * i = 1
iu : i * u = 1
⊢ order u + order i = 0
rw [← order_mul (left_ne_zero_of_mul_eq_one ui) (right_ne_zero_of_mul_eq_one ui), ui, order_one]
case mpr.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * u = 1
h : ↑{ val := u, inv := i, val_inv := ui, inv_val := iu } = coeff x (order x)
⊢ IsUnit x
case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
⊢ IsUnit (coeff x (order x)) → IsUnit x
rintro ⟨⟨u, i, ui, iu⟩, h⟩
case mpr.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * u = 1
h : u = coeff x (order x)
⊢ IsUnit x
case mpr.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * u = 1
h : ↑{ val := u, inv := i, val_inv := ui, inv_val := iu } = coeff x (order x)
⊢ IsUnit x
rw [Units.val_mk] at h
case mpr.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * coeff x (order x) = 1
h : u = coeff x (order x)
⊢ IsUnit x
case mpr.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * u = 1
h : u = coeff x (order x)
⊢ IsUnit x
rw [h] at iu
case mpr.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * coeff x (order x) = 1
h✝ : u = coeff x (order x)
h :
  (1 - (1 - ↑C i * ↑(single (-order x)) 1 * x)) *
      SummableFamily.hsum
        (SummableFamily.powers (1 - ↑C i * ↑(single (-order x)) 1 * x)
          (_ : 0 < ↑(addVal Γ R) (1 - ↑C i * ↑(single (-order x)) 1 * x))) =
    1
⊢ IsUnit x
case mpr.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * coeff x (order x) = 1
h : u = coeff x (order x)
⊢ IsUnit x
have h := SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu)
case mpr.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * coeff x (order x) = 1
h✝ : u = coeff x (order x)
h :
  ↑C i * ↑(single (-order x)) 1 * x *
      SummableFamily.hsum
        (SummableFamily.powers (1 - ↑C i * ↑(single (-order x)) 1 * x)
          (_ : 0 < ↑(addVal Γ R) (1 - ↑C i * ↑(single (-order x)) 1 * x))) =
    1
⊢ IsUnit x
case mpr.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * coeff x (order x) = 1
h✝ : u = coeff x (order x)
h :
  (1 - (1 - ↑C i * ↑(single (-order x)) 1 * x)) *
      SummableFamily.hsum
        (SummableFamily.powers (1 - ↑C i * ↑(single (-order x)) 1 * x)
          (_ : 0 < ↑(addVal Γ R) (1 - ↑C i * ↑(single (-order x)) 1 * x))) =
    1
⊢ IsUnit x
rw [sub_sub_cancel] at h
no goals
case mpr.intro.mk
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
u i : R
ui : u * i = 1
iu : i * coeff x (order x) = 1
h✝ : u = coeff x (order x)
h :
  ↑C i * ↑(single (-order x)) 1 * x *
      SummableFamily.hsum
        (SummableFamily.powers (1 - ↑C i * ↑(single (-order x)) 1 * x)
          (_ : 0 < ↑(addVal Γ R) (1 - ↑C i * ↑(single (-order x)) 1 * x))) =
    1
⊢ IsUnit x
exact isUnit_of_mul_isUnit_right (isUnit_of_mul_eq_one _ _ h)