awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
h : a * ω ≤ b
⊢ a * ω + (b - a * ω) = b

Tactic:
have := Ordinal.add_sub_cancel_of_le h
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
refine_2 : a + (a * ω + (b - a * ω)) = b
⊢ a + b = b

Tactic:
nth_rw 1 [← this]
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
refine_2 : a + a * ω + (b - a * ω) = b
refine_2₁ : a * (1 + ω) + (b - a * ω) = b
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b

Tactic:
rwa [← add_assoc, ← mul_one_add, one_add_omega0]

Premises used: add_assoc, Ordinal.one_add_omega0, mul_one_add
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
rw : a + b ≤ b ↔ a + b = b
⊢ a + b ≤ b ↔ a * ω ≤ b

Tactic:
rw [← add_eq_right_iff_mul_omega0_le]

Premises used: Ordinal.add_eq_right_iff_mul_omega0_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a + b = b

Tactic:
(isNormal_add_right a).strictMono.le_apply.ge_iff_eq'

Premises used: StrictMono.le_apply, LE.le.ge_iff_eq', Ordinal.isNormal_add_right, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a + b = b

Tactic:
exact (isNormal_add_right a).strictMono.le_apply.ge_iff_eq'

Premises used: StrictMono.le_apply, LE.le.ge_iff_eq', Ordinal.isNormal_add_right, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u}
revert : ∀ (b : Ordinal.{u}), deriv (fun (x : Ordinal.{u}) ↦ a + x) b = a * ω + b
⊢ deriv (fun (x : Ordinal.{u}) ↦ a + x) b = a * ω + b

Tactic:
revert b
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
rw :
  deriv (fun (x : Ordinal.{u}) ↦ a + x) ⊥ = a * ω + ⊥ ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun (x : Ordinal.{u}) ↦ a + x) a_1 = a * ω + a_1 →
        deriv (fun (x : Ordinal.{u}) ↦ a + x) (succ a_1) = a * ω + succ a_1
⊢ ∀ (b : Ordinal.{u}), deriv (fun (x : Ordinal.{u}) ↦ a + x) b = a * ω + b

Tactic:
rw [← funext_iff, IsNormal.ext_iff (isNormal_deriv _) (isNormal_add_right _)]

Premises used: funext_iff, Ordinal.isNormal_deriv, Order.IsNormal.ext_iff, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
⊢ deriv (fun (x : Ordinal.{u}) ↦ a + x) ⊥ = a * ω + ⊥ ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun (x : Ordinal.{u}) ↦ a + x) a_1 = a * ω + a_1 →
        deriv (fun (x : Ordinal.{u}) ↦ a + x) (succ a_1) = a * ω + succ a_1

Tactic:
⟨?_, fun a h => ?_⟩

Premises used: And.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a + x) ⊥ = a * ω + ⊥
refine_2 :
  ∀ (a_1 : Ordinal.{u}) (h : deriv (fun (x : Ordinal.{u}) ↦ a + x) a_1 = a * ω + a_1),
    deriv (fun (x : Ordinal.{u}) ↦ a + x) (succ a_1) = a * ω + succ a_1
⊢ deriv (fun (x : Ordinal.{u}) ↦ a + x) ⊥ = a * ω + ⊥ ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun (x : Ordinal.{u}) ↦ a + x) a_1 = a * ω + a_1 →
        deriv (fun (x : Ordinal.{u}) ↦ a + x) (succ a_1) = a * ω + succ a_1

Tactic:
refine ⟨?_, fun a h => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
refine_1 : nfp (fun (x : Ordinal.{u}) ↦ a + x) 0 = a * ω
⊢ deriv (fun (x : Ordinal.{u}) ↦ a + x) ⊥ = a * ω + ⊥

Tactic:
rw [bot_eq_zero, deriv_zero_right, add_zero]

Premises used: Ordinal.bot_eq_zero, Ordinal.deriv_zero_right, add_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
⊢ nfp (fun (x : Ordinal.{u}) ↦ a + x) 0 = a * ω

Tactic:
nfp_add_zero a

Premises used: Ordinal.nfp_add_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
⊢ nfp (fun (x : Ordinal.{u}) ↦ a + x) 0 = a * ω

Tactic:
exact nfp_add_zero a

Premises used: Ordinal.nfp_add_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a_1 a : Ordinal.{u}
h : deriv (fun (x : Ordinal.{u}) ↦ a_1 + x) a = a_1 * ω + a
refine_2 : nfp (fun (x : Ordinal.{u}) ↦ a_1 + x) (a_1 * ω + a + 1) = a_1 * ω + a + 1
⊢ deriv (fun (x : Ordinal.{u}) ↦ a_1 + x) (succ a) = a_1 * ω + succ a

Tactic:
rw [succ_eq_add_one, deriv_add_one, h, ← add_assoc]

Premises used: Order.succ_eq_add_one, add_assoc, Ordinal.deriv_add_one
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a_1 a : Ordinal.{u}
h : deriv (fun (x : Ordinal.{u}) ↦ a_1 + x) a = a_1 * ω + a
⊢ nfp (fun (x : Ordinal.{u}) ↦ a_1 + x) (a_1 * ω + a + 1) = a_1 * ω + a + 1

Tactic:
nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 (le_self_add.trans (le_succ _)))

Premises used: Iff.mpr, Ordinal.add_eq_right_iff_mul_omega0_le, Order.le_succ, LE.le.trans, le_self_add, Ordinal.nfp_eq_self
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a_1 a : Ordinal.{u}
h : deriv (fun (x : Ordinal.{u}) ↦ a_1 + x) a = a_1 * ω + a
⊢ nfp (fun (x : Ordinal.{u}) ↦ a_1 + x) (a_1 * ω + a + 1) = a_1 * ω + a + 1

Tactic:
exact nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 (le_self_add.trans (le_succ _)))

Premises used: Iff.mpr, Ordinal.add_eq_right_iff_mul_omega0_le, Order.le_succ, LE.le.trans, le_self_add, Ordinal.nfp_eq_self
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
ha : 0 < a
rw : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (n : ℕ), (fun (x : Ordinal.{u_1}) ↦ a * x)^[n] 1) (⨆ (n : ℕ), a ^ n)
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 = a ^ ω

Tactic:
rw [← iSup_iterate_eq_nfp, ← iSup_pow_natCast ha]

Premises used: Ordinal.iSup_pow_natCast, Ordinal.iSup_iterate_eq_nfp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
ha : 0 < a
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (n : ℕ), (fun (x : Ordinal.{u_1}) ↦ a * x)^[n] 1) (⨆ (n : ℕ), a ^ n)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
rw : ∀ (n : ℕ), LE.le.{u_1 + 1} (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ a * x)^[n] 0) 0
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 0 = 0

Tactic:
rw [← nonpos_iff_eq_zero, nfp_le_iff]

Premises used: Ordinal.nfp_le_iff, nonpos_iff_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u_1}
⊢ ∀ (n : ℕ), LE.le.{u_1 + 1} (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ a * x)^[n] 0) 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
inl :
  ∀ (hba : b ≤ HPow.hPow (α := Ordinal.{u_1}) 0 ω),
    nfp (fun (x : Ordinal.{u_1}) ↦ 0 * x) b = HPow.hPow (α := Ordinal.{u_1}) 0 ω
inr : ∀ (ha : 0 < a), nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b = a ^ ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b = a ^ ω

Tactic:
rcases eq_zero_or_pos a with rfl | ha

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ HPow.hPow (α := Ordinal.{u_1}) 0 ω
⊢ b ≤ 0

Tactic:
rw [zero_opow omega0_ne_zero] at hba

Premises used: Ordinal.omega0_ne_zero, Ordinal.zero_opow
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ 0 * x) b = HPow.hPow (α := Ordinal.{u_1}) 0 ω

Tactic:
cases hba.not_gt hb

Premises used: LE.le.not_gt
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
inr : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b ≤ a ^ ω
inr₁ : a ^ ω ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b = a ^ ω

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
inr : a * a ^ ω ≤ a ^ ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b ≤ a ^ ω

Tactic:
apply nfp_le_fp (isNormal_mul_right ha).monotone hba

Premises used: Ordinal.isNormal_mul_right, Ordinal.nfp_le_fp, Order.IsNormal.monotone
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
inr : a ^ (1 + ω) ≤ a ^ ω
inr₁ inr₂ : a ^ ω ≤ a ^ ω
⊢ a * a ^ ω ≤ a ^ ω

Tactic:
rw [← opow_one_add, one_add_omega0]

Premises used: Ordinal.one_add_omega0, Ordinal.opow_one_add
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
inr : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b
⊢ a ^ ω ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b

Tactic:
rw [← nfp_mul_one ha]

Premises used: Ordinal.nfp_mul_one
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b

Tactic:
nfp_monotone (isNormal_mul_right ha).monotone (one_le_iff_pos.2 hb)

Premises used: Iff.mpr, Ordinal.isNormal_mul_right, Order.IsNormal.monotone, Ordinal.nfp_monotone, Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b

Tactic:
exact nfp_monotone (isNormal_mul_right ha).monotone (one_le_iff_pos.2 hb)

Premises used: Iff.mpr, Ordinal.isNormal_mul_right, Order.IsNormal.monotone, Ordinal.nfp_monotone, Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
inl : ∀ (ha : a = 0), b = 0 ∨ a ^ ω ≤ b
inr : ∀ (ha : 0 < a), b = 0 ∨ a ^ ω ≤ b
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
rcases eq_zero_or_pos a with ha | ha

Premises used: eq_zero_or_pos
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
inl : b = 0 ∨ 0 ≤ b
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
rw [ha, zero_opow omega0_ne_zero]

Premises used: Ordinal.omega0_ne_zero, Ordinal.zero_opow
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b

Tactic:
.inr zero_le

Premises used: zero_le, Or.inr
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b

Tactic:
exact .inr zero_le
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
inr : ¬b = 0 → a ^ ω ≤ b
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
inr : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 ≤ b
⊢ a ^ ω ≤ b

Tactic:
rw [← nfp_mul_one ha]

Premises used: Ordinal.nfp_mul_one
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ 1 ≤ b

Tactic:
rw [← Ne, ← one_le_iff_ne_zero] at hb

Premises used: Ne, Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 ≤ b

Tactic:
nfp_le_fp (isNormal_mul_right ha).monotone hb (le_of_eq hab)

Premises used: Ordinal.isNormal_mul_right, Ordinal.nfp_le_fp, Order.IsNormal.monotone, le_of_eq
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 ≤ b

Tactic:
exact nfp_le_fp (isNormal_mul_right ha).monotone hb (le_of_eq hab)

Premises used: Ordinal.isNormal_mul_right, Ordinal.nfp_le_fp, Order.IsNormal.monotone, le_of_eq
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
inl : ∀ (ha : a = 0), a * b = b ↔ a ^ ω ∣ b
inr : ∀ (ha : 0 < a), a * b = b ↔ a ^ ω ∣ b
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
rcases eq_zero_or_pos a with ha | ha

Premises used: eq_zero_or_pos
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : a = 0
inl : 0 = b ↔ b = 0
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
rw [ha, zero_mul, zero_opow omega0_ne_zero, zero_dvd_iff]

Premises used: MulZeroClass.zero_mul, zero_dvd_iff, Ordinal.omega0_ne_zero, Ordinal.zero_opow
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : a = 0
⊢ 0 = b ↔ b = 0

Tactic:
eq_comm

Premises used: eq_comm
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : a = 0
⊢ 0 = b ↔ b = 0

Tactic:
exact eq_comm

Premises used: eq_comm
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
⟨fun hab => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
inr : ∀ (hab : a * b = b), a ^ ω ∣ b
inr₁ : ∀ (h : a ^ ω ∣ b), a * b = b
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
refine ⟨fun hab => ?_, fun h => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
inr : b % a ^ ω = 0
⊢ a ^ ω ∣ b

Tactic:
rw [dvd_iff_mod_eq_zero]

Premises used: Ordinal.dvd_iff_mod_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ a * (b % a ^ ω) = b % a ^ ω

Tactic:
rw [← div_add_mod b (a ^ ω), mul_add, ← mul_assoc, ← opow_one_add, one_add_omega0,
      add_left_cancel_iff] at hab

Premises used: Ordinal.omega0, Ordinal.div_add_mod, mul_assoc, Ordinal.one_add_omega0, Ordinal.opow_one_add, add_left_cancel_iff, HPow.hPow, mul_add
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
inr : ∀ (hab : b % a ^ ω = 0), b % a ^ ω = 0
inr₁ : ∀ (hab : a ^ ω ≤ b % a ^ ω), b % a ^ ω = 0
⊢ b % a ^ ω = 0

Tactic:
rcases eq_zero_or_opow_omega0_le_of_mul_eq_right hab with hab | hab

Premises used: Ordinal.eq_zero_or_opow_omega0_le_of_mul_eq_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab_1 : a * (b % a ^ ω) = b % a ^ ω
hab : b % a ^ ω = 0
⊢ b % a ^ ω = 0

Tactic:
hab
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab_1 : a * (b % a ^ ω) = b % a ^ ω
hab : b % a ^ ω = 0
⊢ b % a ^ ω = 0

Tactic:
exact hab
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab_1 : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ b % a ^ ω = 0

Tactic:
(not_lt_of_ge hab (mod_lt b (opow_ne_zero ω ?_))).elim

Premises used: Ordinal.omega0, False.elim, Ordinal.opow_ne_zero, Ordinal.mod_lt, not_lt_of_ge
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab_1 : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
inr : a ≠ 0
⊢ b % a ^ ω = 0

Tactic:
refine (not_lt_of_ge hab (mod_lt b (opow_ne_zero ω ?_))).elim

Premises used: Ordinal.omega0, False.elim, Ordinal.opow_ne_zero, Ordinal.mod_lt, not_lt_of_ge
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab_1 : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
inr inr₁ inr₂ inr₃ : 0 < a
⊢ a ≠ 0

Tactic:
rwa [← pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
h : a ^ ω ∣ b
inr : ∀ (c : Ordinal.{u_1}) (hc : b = a ^ ω * c), a * b = b
⊢ a * b = b

Tactic:
obtain ⟨c, hc⟩ := h
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
inr : a * (a ^ ω * c) = a ^ ω * c
inr₁ : a * a ^ ω * c = a ^ ω * c
inr₂ : a ^ (1 + ω) * c = a ^ ω * c
inr₃ inr₄ : a ^ ω * c = a ^ ω * c
⊢ a * b = b

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

Premises used: mul_assoc, Ordinal.one_add_omega0, Ordinal.opow_one_add
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
rw : a * b ≤ b ↔ a * b = b
⊢ a * b ≤ b ↔ a ^ ω ∣ b

Tactic:
rw [← mul_eq_right_iff_opow_omega0_dvd]

Premises used: Ordinal.mul_eq_right_iff_opow_omega0_dvd
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a * b = b

Tactic:
(isNormal_mul_right ha).strictMono.le_apply.ge_iff_eq'

Premises used: StrictMono.le_apply, Ordinal.isNormal_mul_right, LE.le.ge_iff_eq', Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a * b = b

Tactic:
exact (isNormal_mul_right ha).strictMono.le_apply.ge_iff_eq'

Premises used: StrictMono.le_apply, Ordinal.isNormal_mul_right, LE.le.ge_iff_eq', Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
a₁ : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b
a₂ : a ^ ω * succ b ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * succ b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
a₁ : a ^ ω * b + c ≤ a ^ ω * succ b
a₂ : a * (a ^ ω * succ b) ≤ a ^ ω * succ b
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b

Tactic:
apply nfp_le_fp (isNormal_mul_right ha).monotone

Premises used: Ordinal.isNormal_mul_right, Ordinal.nfp_le_fp, Order.IsNormal.monotone
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
a₁ : a ^ ω * b + c ≤ a ^ ω * b + a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * succ b

Tactic:
rw [mul_succ]

Premises used: Ordinal.mul_succ
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * b + a ^ ω

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
a₁ : a * a ^ ω * succ b ≤ a ^ ω * succ b
a₂ : a ^ (1 + ω) * succ b ≤ a ^ ω * succ b
a₃ a₄ : a ^ ω * succ b ≤ a ^ ω * succ b
⊢ a * (a ^ ω * succ b) ≤ a ^ ω * succ b

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

Premises used: mul_assoc, Ordinal.one_add_omega0, Ordinal.opow_one_add
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
a₁ :
  ∀ (d : Ordinal.{u_1}) (hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d),
    a ^ ω * succ b ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)
⊢ a ^ ω * succ b ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)

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

Premises used: Ordinal.isNormal_mul_right, HMul.hMul, Ordinal.omega0, Ordinal.nfp_fp, Ordinal.mul_eq_right_iff_opow_omega0_dvd, HPow.hPow, HAdd.hAdd, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
a₁ : a ^ ω * succ b ≤ a ^ ω * d
⊢ a ^ ω * succ b ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)

Tactic:
rw [hd]
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
a₁ : succ b ≤ d
⊢ a ^ ω * succ b ≤ a ^ ω * d

Tactic:
apply mul_le_mul_right

Premises used: mul_le_mul_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * b + c ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)

Tactic:
have := le_nfp (a * ·) (a ^ ω * b + c)
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)
⊢ a ^ ω * b + c ≤ a ^ ω * d

Tactic:
rw [hd] at this
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ a ^ ω * d
⊢ a ^ ω * b + 0 < a ^ ω * d

Tactic:
have := (add_lt_add_right hc (a ^ ω * b)).trans_le this
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this_1 : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b + 0 < a ^ ω * d
⊢ b < d

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

Premises used: Ordinal.omega0, mul_lt_mul_iff_right₀, add_zero, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this_1 : a ^ ω * b + c ≤ a ^ ω * d
this a₁ a₂ a₃ a₄ : b < d
⊢ succ b ≤ d

Tactic:
rwa [succ_le_iff]

Premises used: Order.succ_le_iff
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
ha : 0 < a
b : Ordinal.{u}
revert : ∀ (b : Ordinal.{u}), deriv (fun (x : Ordinal.{u}) ↦ a * x) b = a ^ ω * b
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) b = a ^ ω * b

Tactic:
revert b
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
ha : 0 < a
rw :
  deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥ ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun (x : Ordinal.{u}) ↦ a * x) a_1 = a ^ ω * a_1 →
        deriv (fun (x : Ordinal.{u}) ↦ a * x) (succ a_1) = a ^ ω * succ a_1
⊢ ∀ (b : Ordinal.{u}), deriv (fun (x : Ordinal.{u}) ↦ a * x) b = a ^ ω * b

Tactic:
rw [← funext_iff,
    IsNormal.ext_iff (isNormal_deriv _) (isNormal_mul_right (opow_pos ω ha))]

Premises used: Ordinal.isNormal_mul_right, Ordinal.omega0, funext_iff, Ordinal.isNormal_deriv, Order.IsNormal.ext_iff, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥ ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun (x : Ordinal.{u}) ↦ a * x) a_1 = a ^ ω * a_1 →
        deriv (fun (x : Ordinal.{u}) ↦ a * x) (succ a_1) = a ^ ω * succ a_1

Tactic:
⟨?_, fun c h => ?_⟩

Premises used: And.intro
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
ha : 0 < a
refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥
refine_2 :
  ∀ (c : Ordinal.{u}) (h : deriv (fun (x : Ordinal.{u}) ↦ a * x) c = a ^ ω * c),
    deriv (fun (x : Ordinal.{u}) ↦ a * x) (succ c) = a ^ ω * succ c
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥ ∧
    ∀ (a_1 : Ordinal.{u}),
      deriv (fun (x : Ordinal.{u}) ↦ a * x) a_1 = a ^ ω * a_1 →
        deriv (fun (x : Ordinal.{u}) ↦ a * x) (succ a_1) = a ^ ω * succ a_1

Tactic:
refine ⟨?_, fun c h => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
ha : 0 < a
refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a * x) 0 = a ^ ω * 0
refine_1₁ : nfp (fun (x : Ordinal.{u}) ↦ a * x) 0 = a ^ ω * 0
refine_1₂ : 0 = a ^ ω * 0
refine_1₃ refine_1₄ : Eq.{u + 2} (α := Ordinal.{u}) 0 0
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) ⊥ = a ^ ω * ⊥

Tactic:
rw [bot_eq_zero, deriv_zero_right, nfp_mul_zero, mul_zero]

Premises used: Ordinal.bot_eq_zero, Ordinal.nfp_mul_zero, MulZeroClass.mul_zero, Ordinal.deriv_zero_right
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun (x : Ordinal.{u}) ↦ a * x) c = a ^ ω * c
refine_2 : nfp (fun (x : Ordinal.{u}) ↦ a * x) (succ (a ^ ω * c)) = a ^ ω * succ c
⊢ deriv (fun (x : Ordinal.{u}) ↦ a * x) (succ c) = a ^ ω * succ c

Tactic:
rw [deriv_succ, h]

Premises used: Ordinal.deriv_succ
-- Module: Mathlib.SetTheory.Ordinal.FixedPoint
Goal:
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun (x : Ordinal.{u}) ↦ a * x) c = a ^ ω * c
⊢ nfp (fun (x : Ordinal.{u}) ↦ a * x) (succ (a ^ ω * c)) = a ^ ω * succ c

Tactic:
nfp_mul_opow_omega0_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))

Premises used: Iff.mpr, Order.succ, Ordinal.nfp_mul_opow_omega0_add, zero_lt_one, Ordinal.opow_pos, Order.one_le_iff_pos