awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
⊢ (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty
have obtain : ∀ (b : Ordinal.{u}) (hb : b ∈ s) (hba : a < b), (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty
Tactic: obtain ⟨b, hb, hba⟩ := hs a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ enumOrd s o ∈ s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}
have rw : sInf (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}) ∈ s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}
Tactic: rw [enumOrd]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
⊢ enumOrd s (succ b) ≤ a
have apply : ∀ b_1 < succ b, enumOrd s b_1 < a
Tactic: apply enumOrd_le_of_forall_lt ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (hypothesis)
Goal:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
hc : c < succ b
⊢ enumOrd s c < a
have hc₁ : c ≤ b
Tactic: rw [lt_succ_iff] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ range (enumOrd s) = s
have h : ∀ (a : Ordinal.{u}), a ∈ range (enumOrd s) ↔ a ∈ s
Tactic: ext a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
⊢ a ∈ range (enumOrd s) ↔ a ∈ s
have h : a ∈ range (enumOrd s) → a ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
h : a ∈ range (enumOrd s) → a ∈ s
⊢ a ∈ range (enumOrd s) ↔ a ∈ s
have h₁ : a ∈ s → a ∈ range (enumOrd s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ∈ range (enumOrd s)
have h : ∀ b < sInf t, enumOrd s b < a
Tactic: refine ⟨sInf t, (enumOrd_le_of_forall_lt ha ?_).antisymm ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
ha : a ∈ s
h : ∀ b < sInf t, enumOrd s b < a
⊢ a ∈ range (enumOrd s)
have h₁ : a ≤ enumOrd s (sInf t)
Tactic: refine ⟨sInf t, (enumOrd_le_of_forall_lt ha ?_).antisymm ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b : Ordinal.{u} | a ≤ enumOrd s b}
ha : a ∈ s
b : Ordinal.{u}
hb : b < sInf t
⊢ enumOrd s b < a
have h : ∀ (hb' : a ≤ enumOrd s b), False
Tactic: by_contra! hb'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
hb : b ∈ s
⊢ ∃ (a : Ordinal.{u}), enumOrd s a = b
have rwa : ∀ (hb : b ∈ range (enumOrd s)), ∃ (a : Ordinal.{u}), enumOrd s a = b
Tactic: rwa [← range_enumOrd hs] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ enumOrd t a ≤ enumOrd s a
have rw : sInf (t ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd t c < b}) ≤ sInf (s ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd s c < b})
Tactic: rw [enumOrd, enumOrd]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ sInf (t ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd t c < b}) ≤ sInf (s ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd s c < b})
have h₁ : (s ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd s c < b}).Nonempty
Tactic: gcongr with b c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
h₁ : (s ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd s c < b}).Nonempty
⊢ sInf (t ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd t c < b}) ≤ sInf (s ∩ {b : Ordinal.{u} | ∀ c < a, enumOrd s c < b})
have h₂ : ∀ (b c : Ordinal.{u}), c < a → enumOrd t c ≤ enumOrd s c
Tactic: gcongr with b c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ enumOrd s = f ↔ StrictMono f ∧ range f = s
have mp : enumOrd s = f → StrictMono f ∧ range f = s
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
mp : enumOrd s = f → StrictMono f ∧ range f = s
⊢ enumOrd s = f ↔ StrictMono f ∧ range f = s
have mpr : StrictMono f ∧ range f = s → enumOrd s = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ enumOrd s = f
have mpr : range (enumOrd s) = range f
Tactic: rwa [← (enumOrd_strictMono hs).range_inj h₁, range_enumOrd hs, eq_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
mpr : range (enumOrd s) = range f
⊢ enumOrd s = f
have mpr₁ : s = range f
Tactic: rwa [← (enumOrd_strictMono hs).range_inj h₁, range_enumOrd hs, eq_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
⊢ IsNormal (enumOrd s)
have refine : ∀ (o : Ordinal.{u}) (ho : IsSuccLimit o) (a : Ordinal.{u}) (ha : ∀ b < o, enumOrd s b ≤ a), enumOrd s o ≤ a
Tactic: refine isNormal_iff.2 ⟨enumOrd_strictMono hs, fun o ho a ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ enumOrd s o ≤ a
have trans : enumOrd s o ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})
Tactic: trans ⨆ b : Iio o, enumOrd s b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
trans : enumOrd s o ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})
⊢ enumOrd s o ≤ a
have trans₁ : ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u}) ≤ a
Tactic: trans ⨆ b : Iio o, enumOrd s b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ enumOrd s o ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})
have refine_1 : ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u}) ∈ s
Tactic: refine enumOrd_le_of_forall_lt ?_ (fun b hb ↦ (enumOrd_strictMono hs (lt_succ b)).trans_le ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
refine_1 : ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u}) ∈ s
⊢ enumOrd s o ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})
have refine_2 : ∀ (b : Ordinal.{u}) (hb : b < o), enumOrd s (succ b) ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})
Tactic: refine enumOrd_le_of_forall_lt ?_ (fun b hb ↦ (enumOrd_strictMono hs (lt_succ b)).trans_le ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (hypothesis)
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u}) ∈ s
have this : Nonempty.{u + 2} (↑(Iio o) : Type (u + 1))
Tactic: have : Nonempty (Iio o) := ⟨0, ho.bot_lt⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
this : Nonempty.{u + 2} (↑(Iio o) : Type (u + 1))
⊢ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u}) ∈ s
have apply : (range fun (b : (↑(Iio o) : Type (u + 1))) ↦ enumOrd s (↑b : Ordinal.{u})) ⊆ s
Tactic: apply H _ _ (range_nonempty _) bddAbove_of_small
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
⊢ enumOrd univ = id
have rw : enumOrd (range id) = id
Tactic: rw [← range_id]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
⊢ enumOrd s 0 = sInf s
have rw : sInf (s ∩ {b : Ordinal.{u} | ∀ c < 0, enumOrd s c < b}) = sInf s
Tactic: rw [enumOrd]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 a ≤ 1
have rw : 1 - a ≤ 1
Tactic: rw [zero_opow']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 a = 0
have rwa : 1 - a = 0
Tactic: rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
a0 : a ≠ 0
rwa : 1 - a = 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 a = 0
have rwa₁ : 1 ≤ a
Tactic: rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
⊢ HPow.hPow (β := Ordinal.{u_1}) a 0 = 1
have inl : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0 = 1
Tactic: obtain rfl | h := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
inl : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0 = 1
⊢ HPow.hPow (β := Ordinal.{u_1}) a 0 = 1
have inr : ∀ (h : a ≠ 0), HPow.hPow (β := Ordinal.{u_1}) a 0 = 1
Tactic: obtain rfl | h := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
⊢ HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0 = 1
have inl : HSub.hSub (α := Ordinal.{u_1}) 1 0 = 1
Tactic: rw [zero_opow', Ordinal.sub_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
inl : HSub.hSub (α := Ordinal.{u_1}) 1 0 = 1
⊢ HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0 = 1
have inl₁ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 1 1
Tactic: rw [zero_opow', Ordinal.sub_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
h : a ≠ 0
⊢ HPow.hPow (β := Ordinal.{u_1}) a 0 = 1
have inr : Eq.{u_1 + 2} (α := Ordinal.{u_1})
  (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) 0 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
      fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
      ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) sorry :
    Ordinal.{u_1})
  1
Tactic: rw [opow_of_ne_zero h, limitRecOn_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
h : a ≠ 0
inr :
  Eq.{u_1 + 2} (α := Ordinal.{u_1})
    (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) 0 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
        fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
        ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯ :
      Ordinal.{u_1})
    1
⊢ HPow.hPow (β := Ordinal.{u_1}) a 0 = 1
have inr₁ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 1 1
Tactic: rw [opow_of_ne_zero h, limitRecOn_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a ^ (b + 1) = a ^ b * a
have inl : HPow.hPow (α := Ordinal.{u_1}) 0 (b + 1) = HPow.hPow (α := Ordinal.{u_1}) 0 b * 0
Tactic: obtain rfl | h := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
inl : HPow.hPow (α := Ordinal.{u_1}) 0 (b + 1) = HPow.hPow (α := Ordinal.{u_1}) 0 b * 0
⊢ a ^ (b + 1) = a ^ b * a
have inr : ∀ (h : a ≠ 0), a ^ (b + 1) = a ^ b * a
Tactic: obtain rfl | h := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b + 1) = HPow.hPow (α := Ordinal.{u_1}) 0 b * 0
have inl : 0 = HPow.hPow (α := Ordinal.{u_1}) 0 b * 0
Tactic: rw [zero_opow (add_pos_of_right zero_lt_one b).ne', mul_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
inl : 0 = HPow.hPow (α := Ordinal.{u_1}) 0 b * 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b + 1) = HPow.hPow (α := Ordinal.{u_1}) 0 b * 0
have inl₁ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0
Tactic: rw [zero_opow (add_pos_of_right zero_lt_one b).ne', mul_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ (b + 1) = a ^ b * a
have inr : (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (b + 1) 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
    fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
    ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) sorry) =
  HMul.hMul (α := Ordinal.{u_1})
    (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) b 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
        fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
        ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) sorry :
      Ordinal.{u_1})
    a
Tactic: rw [opow_of_ne_zero h, opow_of_ne_zero h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccLimit b
⊢ a ^ b = ⨆ (x : (↑(Iio b) : Type (u_1 + 1))), a ^ (↑x : Ordinal.{u_1})
have simp_rw : Eq (α := Ordinal.{u_1})
  (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) b 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
      fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
      ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) sorry :
    Ordinal.{u_1})
  (⨆ (x : (↑(Iio b) : Type (u_1 + 1))),
    limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (↑x : Ordinal.{u_1}) 1
      (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
      fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
      ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) sorry)
Tactic: simp_rw [opow_of_ne_zero ha, limitRecOn_limit _ _ _ _ hb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c
have rw : (∀ (a_1 : Ordinal.{u_1}) (b_1 : a_1 ∈ Iio b),
    a ^ (↑(Subtype.mk (p := fun (a : Ordinal.{u_1}) ↦ a ∈ Iio b) a_1 b_1) : Ordinal.{u_1}) ≤ c) ↔
  ∀ b' < b, a ^ b' ≤ c
Tactic: rw [opow_limit a0 h, Ordinal.iSup_le_iff, Subtype.forall]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, HPow.hPow (α := Ordinal.{u_1}) 1 o' = 1
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 b = 1
have limit : ∀ (c : Ordinal.{u_1}), HPow.hPow (α := Ordinal.{u_1}) 1 b ≤ c ↔ 1 ≤ c
Tactic: refine eq_of_forall_ge_iff fun c => ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, HPow.hPow (α := Ordinal.{u_1}) 1 o' = 1
c : Ordinal.{u_1}
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 b ≤ c ↔ 1 ≤ c
have limit : (∀ b' < b, HPow.hPow (α := Ordinal.{u_1}) 1 b' ≤ c) ↔ 1 ≤ c
Tactic: rw [opow_le_of_isSuccLimit one_ne_zero l]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 a = 1
have zero : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 1 0 = 1
Tactic: induction a using limitRecOn with
  | zero => simp
  | add_one _ IH => simp [IH, mul_one]
  | limit b l IH =>
    refine eq_of_forall_ge_iff fun c => ?_
    rw [opow_le_of_isSuccLimit one_ne_zero l]
    exact ⟨fun H => by simpa only [opow_zero] using H 0 l.bot_lt, fun H b' h => by rwa [IH _ h]⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
zero : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 1 0 = 1
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 a = 1
have add_one : ∀ (o : Ordinal.{u_1}) (IH : HPow.hPow (α := Ordinal.{u_1}) 1 o = 1), HPow.hPow (α := Ordinal.{u_1}) 1 (o + 1) = 1
Tactic: induction a using limitRecOn with
  | zero => simp
  | add_one _ IH => simp [IH, mul_one]
  | limit b l IH =>
    refine eq_of_forall_ge_iff fun c => ?_
    rw [opow_le_of_isSuccLimit one_ne_zero l]
    exact ⟨fun H => by simpa only [opow_zero] using H 0 l.bot_lt, fun H b' h => by rwa [IH _ h]⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
zero : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 1 0 = 1
add_one :
  ∀ (o : Ordinal.{u_1}) (IH : HPow.hPow (α := Ordinal.{u_1}) 1 o = 1), HPow.hPow (α := Ordinal.{u_1}) 1 (o + 1) = 1
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 a = 1
have limit : ∀ (b : Ordinal.{u_1}) (l : IsSuccLimit b) (IH : ∀ o' < b, HPow.hPow (α := Ordinal.{u_1}) 1 o' = 1),
  HPow.hPow (α := Ordinal.{u_1}) 1 b = 1
Tactic: induction a using limitRecOn with
  | zero => simp
  | add_one _ IH => simp [IH, mul_one]
  | limit b l IH =>
    refine eq_of_forall_ge_iff fun c => ?_
    rw [opow_le_of_isSuccLimit one_ne_zero l]
    exact ⟨fun H => by simpa only [opow_zero] using H 0 l.bot_lt, fun H b' h => by rwa [IH _ h]⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (hypothesis)
Goal:
a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ b
have h0 : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
Tactic: have h0 : 0 < a ^ (0 : Ordinal) := by simp
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
zero : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
⊢ 0 < a ^ b
have add_one : ∀ (b : Ordinal.{u_1}) (IH : 0 < a ^ b), 0 < a ^ (b + 1)
Tactic: induction b using limitRecOn with
  | zero => exact h0
  | add_one b IH => simpa using mul_pos IH a0
  | limit b l _ => exact (lt_opow_of_isSuccLimit (pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
zero : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
add_one : ∀ (b : Ordinal.{u_1}) (IH : 0 < a ^ b), 0 < a ^ (b + 1)
⊢ 0 < a ^ b
have limit : ∀ (b : Ordinal.{u_1}) (l : IsSuccLimit b), (∀ o' < b, 0 < a ^ o') → 0 < a ^ b
Tactic: induction b using limitRecOn with
  | zero => exact h0
  | add_one b IH => simpa using mul_pos IH a0
  | limit b l _ => exact (lt_opow_of_isSuccLimit (pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
have pos : a = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
Tactic: by_cases a = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
pos : a = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
have neg : ¬a = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
Tactic: by_cases a = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : a = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
have pos : b = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
Tactic: by_cases b = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : a = 0
pos : b = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
have neg : ¬b = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
Tactic: by_cases b = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : ¬a = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
have pos : b = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
Tactic: by_cases b = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : ¬a = 0
pos : b = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
have neg : ¬b = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
Tactic: by_cases b = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑0 : Ordinal.{u_1}) = HPow.hPow (β := ℕ) a 0
have zero : HPow.hPow (β := Ordinal.{u_1}) a 0 = HPow.hPow (β := ℕ) a 0
Tactic: rw [Nat.cast_zero, opow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
zero : HPow.hPow (β := Ordinal.{u_1}) a 0 = HPow.hPow (β := ℕ) a 0
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑0 : Ordinal.{u_1}) = HPow.hPow (β := ℕ) a 0
have zero₁ : 1 = HPow.hPow (β := ℕ) a 0
Tactic: rw [Nat.cast_zero, opow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
zero : HPow.hPow (β := Ordinal.{u_1}) a 0 = HPow.hPow (β := ℕ) a 0
zero₁ : 1 = HPow.hPow (β := ℕ) a 0
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑0 : Ordinal.{u_1}) = HPow.hPow (β := ℕ) a 0
have zero₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 1 1
Tactic: rw [Nat.cast_zero, opow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
n : ℕ
IH : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) = a ^ n
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑(n + 1) : Ordinal.{u_1}) = a ^ (n + 1)
have succ : a ^ HAdd.hAdd (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) 1 = a ^ (n + 1)
Tactic: rw [Nat.cast_succ, ← succ_eq_add_one, opow_succ, pow_succ, IH]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
n : ℕ
IH : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) = a ^ n
succ : a ^ HAdd.hAdd (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) 1 = a ^ (n + 1)
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑(n + 1) : Ordinal.{u_1}) = a ^ (n + 1)
have succ₁ : HPow.hPow (β := Ordinal.{u_1}) a (Order.succ (↑n : Ordinal.{u_1})) = a ^ (n + 1)
Tactic: rw [Nat.cast_succ, ← succ_eq_add_one, opow_succ, pow_succ, IH]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
n : ℕ
IH : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) = a ^ n
succ : a ^ HAdd.hAdd (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) 1 = a ^ (n + 1)
succ₁ : HPow.hPow (β := Ordinal.{u_1}) a (Order.succ (↑n : Ordinal.{u_1})) = a ^ (n + 1)
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑(n + 1) : Ordinal.{u_1}) = a ^ (n + 1)
have succ₂ : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) * a = a ^ (n + 1)
Tactic: rw [Nat.cast_succ, ← succ_eq_add_one, opow_succ, pow_succ, IH]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
n : ℕ
IH : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) = a ^ n
succ : a ^ HAdd.hAdd (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) 1 = a ^ (n + 1)
succ₁ : HPow.hPow (β := Ordinal.{u_1}) a (Order.succ (↑n : Ordinal.{u_1})) = a ^ (n + 1)
succ₂ : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) * a = a ^ (n + 1)
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑(n + 1) : Ordinal.{u_1}) = a ^ (n + 1)
have succ₃ : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) * a = a ^ n * a
Tactic: rw [Nat.cast_succ, ← succ_eq_add_one, opow_succ, pow_succ, IH]