awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ⨆ (n : ℕ), f^[n] a ≤ nfp f a
have a₁ : ∀ (i : ℕ), f^[i] a ≤ nfp f a
Tactic: rw [Ordinal.iSup_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ f^[n] a ≤ nfp f a
have a₁ : List.foldr (fun (x : Unit) ↦ f) a (List.replicate n ()) ≤ nfp f a
Tactic: rw [← List.length_replicate (n := n) (a := Unit.unit), ← List.foldr_const f a]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ nfp f a ≤ ⨆ (n : ℕ), f^[n] a
have a₁ : ∀ (i : List Unit), List.foldr (fun (x : Unit) ↦ f) a i ≤ ⨆ (n : ℕ), f^[n] a
Tactic: apply Ordinal.iSup_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ List.foldr (fun (x : Unit) ↦ f) a l ≤ ⨆ (n : ℕ), f^[n] a
have a₁ : f^[l.length] a ≤ ⨆ (n : ℕ), f^[n] a
Tactic: rw [List.foldr_const f a l]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ nfp f a
have rw : f^[n] a ≤ ⨆ (n : ℕ), f^[n] a
Tactic: rw [← iSup_iterate_eq_nfp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < nfp f b ↔ ∃ (n : ℕ), a < f^[n] b
have rw : a < ⨆ (n : ℕ), f^[n] b ↔ ∃ (n : ℕ), a < f^[n] b
Tactic: rw [← iSup_iterate_eq_nfp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
have rw : ⨆ (n : ℕ), f^[n] a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
Tactic: rw [← iSup_iterate_eq_nfp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
⊢ nfp id = id
have h : ∀ (x : Ordinal.{u_1}), nfp id x = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
x : Ordinal.{u_1}
⊢ nfp id x = id x
have h : ⨆ (n : ℕ), id x = id x
Tactic: simp_rw [← iSup_iterate_eq_nfp, iterate_id]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n] a < nfp f a
have apply : f^[n] (f a) ≤ nfp f a
Tactic: apply (hf.iterate n h).trans_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n] (f a) ≤ nfp f a
have rw : f^[n.succ] a ≤ nfp f a
Tactic: rw [← iterate_succ_apply]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfp f a ↔ b < nfp f a
have unfold : f b < nfpFamily (fun (x : Unit) ↦ f) a ↔ b < nfpFamily (fun (x : Unit) ↦ f) a
Tactic: unfold nfp
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfpFamily (fun (x : Unit) ↦ f) a ↔ b < nfpFamily (fun (x : Unit) ↦ f) a
have rw : f b < nfpFamily (fun (x : Unit) ↦ f) a ↔ ∀ (i : Unit), f b < nfpFamily (fun (x : Unit) ↦ f) a
Tactic: rw [← @apply_lt_nfpFamily_iff Unit (fun _ => f) _ _ (fun _ => H) a b]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ ¬BddAbove (fixedPoints f)
have h : fixedPoints f = ⋂ (i : Unit), fixedPoints f
Tactic: convert! not_bddAbove_fp_family fun _ : Unit => H
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∃ (o : Ordinal.{u}), derivFamily (fun (x : Unit) ↦ f) o = a
have rw : f a ≤ a ↔ ∀ (i : Unit), f a ≤ a
Tactic: rw [← le_iff_derivFamily fun _ : Unit => H]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ a ∈ Set.range (deriv f) ↔ f a = a
have rw : (∃ (y : Ordinal.{u}), deriv f y = a) ↔ f a = a
Tactic: rw [Set.mem_range, ← H.strictMono.le_apply.ge_iff_eq', le_iff_deriv H]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
rw : (∃ (y : Ordinal.{u}), deriv f y = a) ↔ f a = a
⊢ a ∈ Set.range (deriv f) ↔ f a = a
have rw₁ : (∃ (y : Ordinal.{u}), deriv f y = a) ↔ f a ≤ a
Tactic: rw [Set.mem_range, ← H.strictMono.le_apply.ge_iff_eq', le_iff_deriv H]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
rw : (∃ (y : Ordinal.{u}), deriv f y = a) ↔ f a = a
rw₁ : (∃ (y : Ordinal.{u}), deriv f y = a) ↔ f a ≤ a
⊢ a ∈ Set.range (deriv f) ↔ f a = a
have rw₂ : (∃ (y : Ordinal.{u}), deriv f y = a) ↔ ∃ (o : Ordinal.{u}), deriv f o = a
Tactic: rw [Set.mem_range, ← H.strictMono.le_apply.ge_iff_eq', le_iff_deriv H]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ deriv f = enumOrd (fixedPoints f)
have h : fixedPoints f = ⋂ (i : Unit), fixedPoints f
Tactic: convert! derivFamily_eq_enumOrd fun _ : Unit => H
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u_1}
⊢ nfp 0 a = a
have rw : ⨆ (n : ℕ), 0^[n] a = a
Tactic: rw [← iSup_iterate_eq_nfp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u_1}
⊢ ⨆ (n : ℕ), 0^[n] a = a
have apply : ∀ (i : ℕ), 0^[i] a ≤ 0^[0] a
Tactic: apply (Ordinal.iSup_le ?_).antisymm (Ordinal.le_iSup _ 0)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u_1}
n : ℕ
⊢ 0^[n] a ≤ 0^[0] a
have zero : 0^[0] a ≤ 0^[0] a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u_1}
n : ℕ
zero : 0^[0] a ≤ 0^[0] a
⊢ 0^[n] a ≤ 0^[0] a
have succ : ∀ (n : ℕ), 0^[n + 1] a ≤ 0^[0] a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u_1}
n : ℕ
⊢ 0^[n + 1] a ≤ 0^[0] a
have succ : (0 ∘ 0^[n]) a ≤ 0^[0] a
Tactic: rw [Function.iterate_succ']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
⊢ nfp 0 = id
have h : ∀ (x : Ordinal.{u_1}), nfp 0 x = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u_1}
⊢ deriv 0 a = a
have rw : id a = a
Tactic: rw [deriv_zero, id_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u_1}
rw : id a = a
⊢ deriv 0 a = a
have rw₁ : a = a
Tactic: rw [deriv_zero, id_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b = a * ω
have apply : a * ω ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b
Tactic: apply le_antisymm (nfp_le_fp (isNormal_add_right a).monotone hba _)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
apply : a * ω ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b = a * ω
have apply₁ : a + a * ω ≤ a * ω
Tactic: apply le_antisymm (nfp_le_fp (isNormal_add_right a).monotone hba _)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * ω ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b
have rw : nfp (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a + x) b
Tactic: rw [← nfp_add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω
have rw : a * (1 + ω) ≤ a * ω
Tactic: rw [← mul_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
rw : a * (1 + ω) ≤ a * ω
⊢ a + a * ω ≤ a * ω
have rw₁ : a * ω ≤ a * ω
Tactic: rw [← mul_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a + b = b ↔ a * ω ≤ b
have refine_1 : ∀ (h : a + b = b), a * ω ≤ b
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
refine_1 : ∀ (h : a + b = b), a * ω ≤ b
⊢ a + b = b ↔ a * ω ≤ b
have refine_2 : ∀ (h : a * ω ≤ b), a + b = b
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
h : a + b = b
⊢ a * ω ≤ b
have refine_1 : deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ b
Tactic: rw [← nfp_add_zero a, ← deriv_zero_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
h : a + b = b
⊢ deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ b
have refine_1 : ∀ (c : Ordinal.{u_1}) (hc : deriv (fun (x : Ordinal.{u_1}) ↦ a + x) c = b),
  deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ b
Tactic: obtain ⟨c, hc⟩ := (mem_range_deriv (isNormal_add_right a)).2 h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun (x : Ordinal.{u_1}) ↦ a + x) c = b
⊢ deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ b
have refine_1 : deriv (fun (x : Ordinal.{u_1}) ↦ a + x) 0 ≤ deriv (fun (x : Ordinal.{u_1}) ↦ a + x) c
Tactic: rw [← hc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
Goal:
a b : Ordinal.{u_1}
h : a * ω ≤ b
⊢ a + b = b
have this : a * ω + (b - a * ω) = b
Tactic: have := Ordinal.add_sub_cancel_of_le h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + b = b
have refine_2 : a + (a * ω + (b - a * ω)) = b
Tactic: nth_rw 1 [← this]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b
have refine_2 : a + a * ω + (b - a * ω) = b
Tactic: rwa [← add_assoc, ← mul_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
refine_2 : a + a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b
have refine_2₁ : a * (1 + ω) + (b - a * ω) = b
Tactic: rwa [← add_assoc, ← mul_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a * ω ≤ b
have rw : a + b ≤ b ↔ a + b = b
Tactic: rw [← add_eq_right_iff_mul_omega0_le]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u}
⊢ deriv (fun (x : Ordinal.{u}) ↦ a + x) b = a * ω + b
have revert : ∀ (b : Ordinal.{u}), deriv (fun (x : Ordinal.{u}) ↦ a + x) b = a * ω + b
Tactic: revert b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
⊢ ∀ (b : Ordinal.{u}), deriv (fun (x : Ordinal.{u}) ↦ a + x) b = a * ω + b
have 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
Tactic: rw [← funext_iff, IsNormal.ext_iff (isNormal_deriv _) (isNormal_add_right _)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
have refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a + x) ⊥ = a * ω + ⊥
Tactic: refine ⟨?_, fun a h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
refine_1 : deriv (fun (x : Ordinal.{u}) ↦ a + x) ⊥ = 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
have 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
Tactic: refine ⟨?_, fun a h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u}
⊢ deriv (fun (x : Ordinal.{u}) ↦ a + x) ⊥ = a * ω + ⊥
have refine_1 : nfp (fun (x : Ordinal.{u}) ↦ a + x) 0 = a * ω
Tactic: rw [bot_eq_zero, deriv_zero_right, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a_1 a : Ordinal.{u}
h : deriv (fun (x : Ordinal.{u}) ↦ a_1 + x) a = a_1 * ω + a
⊢ deriv (fun (x : Ordinal.{u}) ↦ a_1 + x) (succ a) = a_1 * ω + succ a
have refine_2 : nfp (fun (x : Ordinal.{u}) ↦ a_1 + x) (a_1 * ω + a + 1) = a_1 * ω + a + 1
Tactic: rw [succ_eq_add_one, deriv_add_one, h, ← add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u_1}
ha : 0 < a
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 = a ^ ω
have rw : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (n : ℕ), (fun (x : Ordinal.{u_1}) ↦ a * x)^[n] 1) (⨆ (n : ℕ), a ^ n)
Tactic: rw [← iSup_iterate_eq_nfp, ← iSup_pow_natCast ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a : Ordinal.{u_1}
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 0 = 0
have rw : ∀ (n : ℕ), LE.le.{u_1 + 1} (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ a * x)^[n] 0) 0
Tactic: rw [← nonpos_iff_eq_zero, nfp_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b = a ^ ω
have inl : ∀ (hba : b ≤ HPow.hPow (α := Ordinal.{u_1}) 0 ω),
  nfp (fun (x : Ordinal.{u_1}) ↦ 0 * x) b = HPow.hPow (α := Ordinal.{u_1}) 0 ω
Tactic: rcases eq_zero_or_pos a with rfl | ha
Cleared hypotheses: a, hba
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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 ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b = a ^ ω
have inr : ∀ (ha : 0 < a), nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b = a ^ ω
Tactic: rcases eq_zero_or_pos a with rfl | ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
Goal:
b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ HPow.hPow (α := Ordinal.{u_1}) 0 ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ 0 * x) b = HPow.hPow (α := Ordinal.{u_1}) 0 ω
have hba₁ : b ≤ 0
Tactic: rw [zero_opow omega0_ne_zero] at hba
Cleared hypotheses: hba
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b = a ^ ω
have inr : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b ≤ a ^ ω
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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 ^ ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b = a ^ ω
have inr₁ : a ^ ω ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b ≤ a ^ ω
have inr : a * a ^ ω ≤ a ^ ω
Tactic: apply nfp_le_fp (isNormal_mul_right ha).monotone hba
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a * a ^ ω ≤ a ^ ω
have inr : a ^ (1 + ω) ≤ a ^ ω
Tactic: rw [← opow_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
inr : a ^ (1 + ω) ≤ a ^ ω
⊢ a * a ^ ω ≤ a ^ ω
have inr₁ : a ^ ω ≤ a ^ ω
Tactic: rw [← opow_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b
have inr : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) b
Tactic: rw [← nfp_mul_one ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
⊢ b = 0 ∨ a ^ ω ≤ b
have inl : ∀ (ha : a = 0), b = 0 ∨ a ^ ω ≤ b
Tactic: rcases eq_zero_or_pos a with ha | ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
inl : ∀ (ha : a = 0), b = 0 ∨ a ^ ω ≤ b
⊢ b = 0 ∨ a ^ ω ≤ b
have inr : ∀ (ha : 0 < a), b = 0 ∨ a ^ ω ≤ b
Tactic: rcases eq_zero_or_pos a with ha | ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ a ^ ω ≤ b
have inl : b = 0 ∨ 0 ≤ b
Tactic: rw [ha, zero_opow omega0_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ b = 0 ∨ a ^ ω ≤ b
have inr : ¬b = 0 → a ^ ω ≤ b
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ a ^ ω ≤ b
have inr : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 ≤ b
Tactic: rw [← nfp_mul_one ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
Goal:
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) 1 ≤ b
have hb₁ : 1 ≤ b
Tactic: rw [← Ne, ← one_le_iff_ne_zero] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a * b = b ↔ a ^ ω ∣ b
have inl : ∀ (ha : a = 0), a * b = b ↔ a ^ ω ∣ b
Tactic: rcases eq_zero_or_pos a with ha | ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
inl : ∀ (ha : a = 0), a * b = b ↔ a ^ ω ∣ b
⊢ a * b = b ↔ a ^ ω ∣ b
have inr : ∀ (ha : 0 < a), a * b = b ↔ a ^ ω ∣ b
Tactic: rcases eq_zero_or_pos a with ha | ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : a = 0
⊢ a * b = b ↔ a ^ ω ∣ b
have inl : 0 = b ↔ b = 0
Tactic: rw [ha, zero_mul, zero_opow omega0_ne_zero, zero_dvd_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b = b ↔ a ^ ω ∣ b
have inr : ∀ (hab : a * b = b), a ^ ω ∣ b
Tactic: refine ⟨fun hab => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
inr : ∀ (hab : a * b = b), a ^ ω ∣ b
⊢ a * b = b ↔ a ^ ω ∣ b
have inr₁ : ∀ (h : a ^ ω ∣ b), a * b = b
Tactic: refine ⟨fun hab => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ a ^ ω ∣ b
have inr : b % a ^ ω = 0
Tactic: rw [dvd_iff_mod_eq_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (hypothesis)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0
have hab₁ : 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
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
⊢ b % a ^ ω = 0
have inr : ∀ (hab : b % a ^ ω = 0), b % a ^ ω = 0
Tactic: rcases eq_zero_or_opow_omega0_le_of_mul_eq_right hab with hab | hab
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
inr : ∀ (hab : b % a ^ ω = 0), b % a ^ ω = 0
⊢ b % a ^ ω = 0
have inr₁ : ∀ (hab : a ^ ω ≤ b % a ^ ω), b % a ^ ω = 0
Tactic: rcases eq_zero_or_opow_omega0_le_of_mul_eq_right hab with hab | hab
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
hab_1 : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ b % a ^ ω = 0
have inr : a ≠ 0
Tactic: refine (not_lt_of_ge hab (mod_lt b (opow_ne_zero ω ?_))).elim
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
h : a ^ ω ∣ b
⊢ a * b = b
have inr : ∀ (c : Ordinal.{u_1}) (hc : b = a ^ ω * c), a * b = b
Tactic: obtain ⟨c, hc⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a * b = b
have inr : a * (a ^ ω * c) = a ^ ω * c
Tactic: rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
inr : a * (a ^ ω * c) = a ^ ω * c
⊢ a * b = b
have inr₁ : a * a ^ ω * c = a ^ ω * c
Tactic: rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ a * b = b
have inr₂ : a ^ (1 + ω) * c = a ^ ω * c
Tactic: rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ a * b = b
have inr₃ : a ^ ω * c = a ^ ω * c
Tactic: rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a ^ ω ∣ b
have rw : a * b ≤ b ↔ a * b = b
Tactic: rw [← mul_eq_right_iff_opow_omega0_dvd]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * succ b
have a₁ : nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) = a ^ ω * succ b
have a₂ : a ^ ω * succ b ≤ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b
have a₁ : a ^ ω * b + c ≤ a ^ ω * succ b
Tactic: apply nfp_le_fp (isNormal_mul_right ha).monotone
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
a₁ : a ^ ω * b + c ≤ a ^ ω * succ b
⊢ nfp (fun (x : Ordinal.{u_1}) ↦ a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b
have a₂ : a * (a ^ ω * succ b) ≤ a ^ ω * succ b
Tactic: apply nfp_le_fp (isNormal_mul_right ha).monotone
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * succ b
have a₁ : a ^ ω * b + c ≤ a ^ ω * b + a ^ ω
Tactic: rw [mul_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
Goal:
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a * (a ^ ω * succ b) ≤ a ^ ω * succ b
have a₁ : a * a ^ ω * succ b ≤ a ^ ω * succ b
Tactic: rw [← mul_assoc, ← opow_one_add, one_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.FixedPoint (goal)
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 ^ ω * succ b) ≤ a ^ ω * succ b
have a₂ : a ^ (1 + ω) * succ b ≤ a ^ ω * succ b
Tactic: rw [← mul_assoc, ← opow_one_add, one_add_omega0]