Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
⊢ 0 < ↑(addVal Γ R) (1 - ↑C r * ↑(single (-order x)) 1 * x)
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
⊢ 0 < ↑(addVal Γ R) (1 - ↑C r * ↑(single (-order x)) 1 * x)
have h10 : (1 : R) ≠ 0 := one_ne_zero
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ 0 < ↑(addVal Γ R) (1 - ↑C r * ↑(single (-order x)) 1 * x)
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
⊢ 0 < ↑(addVal Γ R) (1 - ↑C r * ↑(single (-order x)) 1 * x)
have x0 : x ≠ 0 := ne_zero_of_coeff_ne_zero (right_ne_zero_of_mul_eq_one hr)
case refine'_1
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ 0 ≤ ↑(addVal Γ R) (↑C r * ↑(single (-order x)) 1 * x)

case refine'_2
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ 0 ≠ ↑(addVal Γ R) (1 - ↑C r * ↑(single (-order x)) 1 * x)
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ 0 < ↑(addVal Γ R) (1 - ↑C r * ↑(single (-order x)) 1 * x)
refine' lt_of_le_of_ne ((addVal Γ R).map_le_sub (ge_of_eq (addVal Γ R).map_one) _) _
case refine'_1
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ 0 ≤ ↑(addVal Γ R) (↑C r) + ↑(addVal Γ R) (↑(single (-order x)) 1) + ↑(addVal Γ R) x
case refine'_1
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ 0 ≤ ↑(addVal Γ R) (↑C r * ↑(single (-order x)) 1 * x)
simp only [AddValuation.map_mul]
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ ↑C r ≠ 0
case refine'_1
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ 0 ≤ ↑(addVal Γ R) (↑C r) + ↑(addVal Γ R) (↑(single (-order x)) 1) + ↑(addVal Γ R) x
rw [addVal_apply_of_ne x0, addVal_apply_of_ne (single_ne_zero h10), addVal_apply_of_ne _,
  order_C, order_single h10, WithTop.coe_zero, zero_add, ← WithTop.coe_add, neg_add_self,
  WithTop.coe_zero]
no goals
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ ↑C r ≠ 0
exact C_ne_zero (left_ne_zero_of_mul_eq_one hr)
case refine'_2
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ ↑0 ≠ if 1 - ↑C r * ↑(single (-order x)) 1 * x = 0 then ⊤ else ↑(order (1 - ↑C r * ↑(single (-order x)) 1 * x))
case refine'_2
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ 0 ≠ ↑(addVal Γ R) (1 - ↑C r * ↑(single (-order x)) 1 * x)
rw [addVal_apply, ← WithTop.coe_zero]
case refine'_2.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
h : 1 - ↑C r * ↑(single (-order x)) 1 * x = 0
⊢ ↑0 ≠ ⊤

case refine'_2.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
h : ¬1 - ↑C r * ↑(single (-order x)) 1 * x = 0
⊢ ↑0 ≠ ↑(order (1 - ↑C r * ↑(single (-order x)) 1 * x))
case refine'_2
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
⊢ ↑0 ≠ if 1 - ↑C r * ↑(single (-order x)) 1 * x = 0 then ⊤ else ↑(order (1 - ↑C r * ↑(single (-order x)) 1 * x))
split_ifs with h
case refine'_2.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
h : ¬1 - ↑C r * ↑(single (-order x)) 1 * x = 0
⊢ ¬0 = order (1 - ↑C r * ↑(single (-order x)) 1 * x)
case refine'_2.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
h : ¬1 - ↑C r * ↑(single (-order x)) 1 * x = 0
⊢ ↑0 ≠ ↑(order (1 - ↑C r * ↑(single (-order x)) 1 * x))
rw [Ne.def, WithTop.coe_eq_coe]
case refine'_2.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
h : ¬1 - ↑C r * ↑(single (-order x)) 1 * x = 0
con : 0 = order (1 - ↑C r * ↑(single (-order x)) 1 * x)
⊢ False
case refine'_2.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
h : ¬1 - ↑C r * ↑(single (-order x)) 1 * x = 0
⊢ ¬0 = order (1 - ↑C r * ↑(single (-order x)) 1 * x)
intro con
case refine'_2.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
h : ¬1 - ↑C r * ↑(single (-order x)) 1 * x = 0
con : 0 = order (1 - ↑C r * ↑(single (-order x)) 1 * x)
⊢ coeff (1 - ↑C r * ↑(single (-order x)) 1 * x) (order (1 - ↑C r * ↑(single (-order x)) 1 * x)) = 0
case refine'_2.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
h : ¬1 - ↑C r * ↑(single (-order x)) 1 * x = 0
con : 0 = order (1 - ↑C r * ↑(single (-order x)) 1 * x)
⊢ False
apply coeff_order_ne_zero h
no goals
case refine'_2.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
h : ¬1 - ↑C r * ↑(single (-order x)) 1 * x = 0
con : 0 = order (1 - ↑C r * ↑(single (-order x)) 1 * x)
⊢ coeff (1 - ↑C r * ↑(single (-order x)) 1 * x) (order (1 - ↑C r * ↑(single (-order x)) 1 * x)) = 0
rw [← con, mul_assoc, sub_coeff, one_coeff, if_pos rfl, C_mul_eq_smul, smul_coeff, smul_eq_mul,
  ← add_neg_self x.order, single_mul_coeff_add, one_mul, hr, sub_self]
no goals
case refine'_2.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedAddCommGroup Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
r : R
hr : r * coeff x (order x) = 1
h10 : 1 ≠ 0
x0 : x ≠ 0
h : 1 - ↑C r * ↑(single (-order x)) 1 * x = 0
⊢ ↑0 ≠ ⊤
apply WithTop.coe_ne_top