-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem unit_aux (x : HahnSeries Γ R) {r : R} (hr : r * x.leadingCoeff = 1)
    (hxo : IsAddUnit x.order) : 0 < (1 - single (IsAddUnit.addUnit hxo).neg r * x).orderTop

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : y = 0
hrx : (single hxo.addUnit.neg) r * x = 1
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Tactic:
simp only [hrx, sub_self, orderTop_zero, WithTop.top_pos]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ (single hxo.addUnit.neg) r * (single x.order) x.leadingCoeff = 1

Tactic:
simp only [AddUnits.neg_eq_val_neg, ← leadingCoeff_eq, single_mul_single,
  IsAddUnit.val_neg_add, hr, single_zero_one]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ 0 < hxo.addUnit.neg + y.order

Tactic:
refine pos_of_lt_add_right (a := x.order) ?_

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ x.order < x.order + (hxo.addUnit.neg + y.order)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ x.order < x.order + (hxo.addUnit.neg + y.order)

Tactic:
rw [← add_assoc, add_comm x.order, AddUnits.neg_eq_val_neg, IsAddUnit.val_neg_add, zero_add]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ x.order < y.order

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ x.order < y.order

Tactic:
exact order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Tactic:
by_cases hy : y = 0

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Tactic:
have hrx : (single (IsAddUnit.addUnit hxo).neg) r * x = 1 := by
  nth_rw 2 [eq_of_sub_eq_zero hy] simp only [AddUnits.neg_eq_val_neg, ← leadingCoeff_eq, single_mul_single,
    IsAddUnit.val_neg_add, hr, single_zero_one]

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : y = 0
hrx : (single hxo.addUnit.neg) r * x = 1
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
hy' : 0 < ((single hxo.addUnit.neg) r * y).order
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Tactic:
rw [one_minus_single_neg_mul hr (sub_add_cancel x _).symm, orderTop_neg]

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
hy' : 0 < ((single hxo.addUnit.neg) r * y).order
⊢ 0 < ((single hxo.addUnit.neg) r * (x - (single x.order) x.leadingCoeff)).orderTop

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Tactic:
have hy' : 0 < (single (IsAddUnit.addUnit hxo).neg r * y).order := by
  rw [(order_single_mul_of_isRegular hr' hy)]
  refine pos_of_lt_add_right (a := x.order) ?_
  rw [← add_assoc, add_comm x.order, AddUnits.neg_eq_val_neg, IsAddUnit.val_neg_add, zero_add]
  exact order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
hy' : 0 < ((single hxo.addUnit.neg) r * y).order
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Tactic:
have hr' : IsRegular r := IsUnit.isRegular <| isUnit_of_mul_eq_one r x.leadingCoeff hr

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ 0 < ((single hxo.addUnit.neg) r * y).order

Tactic:
rw [(order_single_mul_of_isRegular hr' hy)]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
r : R
hr : r * x.leadingCoeff = 1
hxo : IsAddUnit x.order
y : HahnSeries Γ R := x - (single x.order) x.leadingCoeff
hy : ¬y = 0
hr' : IsRegular r
⊢ 0 < hxo.addUnit.neg + y.order