case refine'_1
a b : Ordinal
h : a + b = b
⊢ a * ω ≤ b

case refine'_2
a b : Ordinal
h : a * ω ≤ b
⊢ a + b = b
a b : Ordinal
⊢ a + b = b ↔ a * ω ≤ b
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
a b : Ordinal
h : a + b = b
⊢ deriv (fun x => a + x) 0 ≤ b
case refine'_1
a b : Ordinal
h : a + b = b
⊢ a * ω ≤ b
rw [← nfp_add_zero a, ← deriv_zero]
case refine'_1.intro
a b : Ordinal
h : a + b = b
c : Ordinal
hc : deriv ((fun x x_1 => x + x_1) a) c = b
⊢ deriv (fun x => a + x) 0 ≤ b
case refine'_1
a b : Ordinal
h : a + b = b
⊢ deriv (fun x => a + x) 0 ≤ b
cases' (add_isNormal a).fp_iff_deriv.1 h with c hc
case refine'_1.intro
a b : Ordinal
h : a + b = b
c : Ordinal
hc : deriv ((fun x x_1 => x + x_1) a) c = b
⊢ deriv (fun x => a + x) 0 ≤ deriv ((fun x x_1 => x + x_1) a) c
case refine'_1.intro
a b : Ordinal
h : a + b = b
c : Ordinal
hc : deriv ((fun x x_1 => x + x_1) a) c = b
⊢ deriv (fun x => a + x) 0 ≤ b
rw [← hc]
no goals
case refine'_1.intro
a b : Ordinal
h : a + b = b
c : Ordinal
hc : deriv ((fun x x_1 => x + x_1) a) c = b
⊢ deriv (fun x => a + x) 0 ≤ deriv ((fun x x_1 => x + x_1) a) c
exact (deriv_isNormal _).monotone (Ordinal.zero_le _)
case refine'_2
a b : Ordinal
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + b = b
case refine'_2
a b : Ordinal
h : a * ω ≤ b
⊢ a + b = b
have := Ordinal.add_sub_cancel_of_le h
case refine'_2
a b : Ordinal
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b
case refine'_2
a b : Ordinal
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + b = b
nth_rw 1 [← this]
no goals
case refine'_2
a b : Ordinal
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b
rwa [← add_assoc, ← mul_one_add, one_add_omega]