-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfp_mul_opow_omega0_add {a c : Ordinal} (b) (ha : 0 < a) (hc : 0 < c)
    (hca : c ≤ a ^ ω) : nfp (a * ·) (a ^ ω * b + c) = a ^ ω * succ b

Proof state:
case a.ab
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * b + a ^ ω

Tactic:
apply add_le_add_left hca

Result:
no goals

Proof state:
case a.h
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a * (a ^ ω * succ b) ≤ a ^ ω * succ b

Tactic:
rw [← mul_assoc, ← opow_one_add, one_add_omega0]

Result:
no goals

Proof state:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * succ b

Tactic:
apply le_antisymm

Result:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun x => a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b

case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)

Proof state:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun x => a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b

Tactic:
apply nfp_le_fp (isNormal_mul_right ha).monotone

Result:
case a.ab
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * succ b

case a.h
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a * (a ^ ω * succ b) ≤ a ^ ω * succ b

Proof state:
case a.intro.bc
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ succ b ≤ d

Tactic:
rwa [succ_le_iff]

Result:
no goals

Proof state:
case a.intro
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ a ^ ω * d

Tactic:
apply mul_le_mul_left'

Result:
case a.intro.bc
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ succ b ≤ d

Proof state:
case a.intro.bc
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ a ^ ω * d
⊢ succ b ≤ d

Tactic:
have := (add_lt_add_left hc (a ^ ω * b)).trans_le this

Result:
case a.intro.bc
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b + 0 < a ^ ω * d
⊢ succ b ≤ d

Proof state:
case a.ab
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * succ b

Tactic:
rw [mul_succ]

Result:
case a.ab
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * b + a ^ ω

Proof state:
case a.intro.bc
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b + 0 < a ^ ω * d
⊢ succ b ≤ d

Tactic:
rw [add_zero, mul_lt_mul_iff_left (opow_pos ω ha)] at this

Result:
case a.intro.bc
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ succ b ≤ d

Proof state:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)

Tactic:
obtain ⟨d, hd⟩ :=
  mul_eq_right_iff_opow_omega0_dvd.1 ((isNormal_mul_right ha).nfp_fp ((a ^ ω) * b + c))

Result:
case a.intro
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)

Proof state:
case a.intro
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ nfp (fun x => a * x) (a ^ ω * b + c)

Tactic:
rw [hd]

Result:
case a.intro
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ a ^ ω * d

Proof state:
case a.intro.bc
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ nfp (fun x => a * x) (a ^ ω * b + c)
⊢ succ b ≤ d

Tactic:
rw [hd] at this

Result:
case a.intro.bc
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x => a * x) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ a ^ ω * d
⊢ succ b ≤ d