awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
succ₃ : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) * a = a ^ n * a
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑(n + 1) : Ordinal.{u_1}) = a ^ (n + 1)
have succ₄ : a ^ n * a = a ^ n * a
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 : ℕ
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) = a ^ n
have zero : HPow.hPow (β := Ordinal.{u_1}) a (↑0 : Ordinal.{u_1}) = HPow.hPow (β := ℕ) a 0
Tactic: induction n with
  | zero => rw [Nat.cast_zero, opow_zero, pow_zero]
  | succ n IH => rw [Nat.cast_succ, ← succ_eq_add_one, opow_succ, pow_succ, IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
n : ℕ
zero : HPow.hPow (β := Ordinal.{u_1}) a (↑0 : Ordinal.{u_1}) = HPow.hPow (β := ℕ) a 0
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) = a ^ n
have succ : ∀ (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)
Tactic: induction n with
  | zero => rw [Nat.cast_zero, opow_zero, pow_zero]
  | succ n IH => rw [Nat.cast_succ, ← succ_eq_add_one, opow_succ, pow_succ, IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (hypothesis)
Goal:
a : Ordinal.{u_1}
h : 1 < a
⊢ IsNormal (β := Ordinal.{u_1}) fun (x : Ordinal.{u_1}) ↦ a ^ x
have ha : 0 < a
Tactic: have ha : 0 < a := zero_lt_one.trans h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ IsNormal (β := Ordinal.{u_1}) fun (x : Ordinal.{u_1}) ↦ a ^ x
have refine_1 : ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ succ a_1
Tactic: refine IsNormal.of_succ_lt ?_ fun hl ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
refine_1 : ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ succ a_1
⊢ IsNormal (β := Ordinal.{u_1}) fun (x : Ordinal.{u_1}) ↦ a ^ x
have refine_2 : ∀ {a_1 : Ordinal.{u_1}} (hl : IsSuccLimit a_1), IsLUB ((fun (x : Ordinal.{u_1}) ↦ a ^ x) '' Iio a_1) (a ^ a_1)
Tactic: refine IsNormal.of_succ_lt ?_ fun hl ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
⊢ 1 < a ^ b ↔ 1 < a ∧ b ≠ 0
have refine_1 : 1 < a ^ b → 1 < a ∧ b ≠ 0
Tactic: refine ⟨?_, fun ⟨ha, hb⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
refine_1 : 1 < a ^ b → 1 < a ∧ b ≠ 0
⊢ 1 < a ^ b ↔ 1 < a ∧ b ≠ 0
have refine_2 : 1 < a ∧ b ≠ 0 → ∀ (ha : 1 < a) (hb : b ≠ 0), 1 < a ^ b
Tactic: refine ⟨?_, fun ⟨ha, hb⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
⊢ 1 < a ^ b → 1 < a ∧ b ≠ 0
have refine_1 : a ≤ 1 ∨ b = 0 → a ^ b ≤ 1
Tactic: contrapose! +distrib
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a ≤ 1 ∨ b = 0 → a ^ b ≤ 1
have refine_1 : (a = 0 ∨ a = 1) ∨ b = 0 → a ^ b ≤ 1
Tactic: rw [le_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
⊢ 1 < a ^ b
have refine_2 : HPow.hPow (β := Ordinal.{u_1}) a 0 < a ^ b
Tactic: rwa [← opow_zero a, opow_lt_opow_iff_right ha, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
refine_2 : HPow.hPow (β := Ordinal.{u_1}) a 0 < a ^ b
⊢ 1 < a ^ b
have refine_2₁ : 0 < b
Tactic: rwa [← opow_zero a, opow_lt_opow_iff_right ha, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a ^ b = 1 ↔ a = 1 ∨ b = 0
have refine : ∀ (h : a ^ b = 1), a = 1 ∨ b = 0
Tactic: refine ⟨fun h ↦ ?_, by simp +contextual [or_imp]⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : a ^ b = 1
⊢ a = 1 ∨ b = 0
have contrapose! : ∀ (h : a ≠ 1 ∧ b ≠ 0), a ^ b ≠ 1
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
⊢ a ^ b ≠ 1
have inl : ∀ (ha : a ≤ 1), a ^ b ≠ 1
Tactic: obtain ha | ha := le_or_gt a 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
inl : ∀ (ha : a ≤ 1), a ^ b ≠ 1
⊢ a ^ b ≠ 1
have inr : ∀ (ha : 1 < a), a ^ b ≠ 1
Tactic: obtain ha | ha := le_or_gt a 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
⊢ IsSuccLimit (a ^ b)
have inl : ∀ (e : b = 0), IsSuccLimit (a ^ b)
Tactic: rcases zero_or_succ_or_isSuccLimit b with (e | ⟨b, rfl⟩ | l')
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
inl : ∀ (e : b = 0), IsSuccLimit (a ^ b)
⊢ IsSuccLimit (a ^ b)
have inr : ∀ (b : Ordinal.{u_1}) (hb : succ b ≠ 0), IsSuccLimit (a ^ succ b)
Tactic: rcases zero_or_succ_or_isSuccLimit b with (e | ⟨b, rfl⟩ | l')
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
inl : ∀ (e : b = 0), IsSuccLimit (a ^ b)
inr : ∀ (b : Ordinal.{u_1}) (hb : succ b ≠ 0), IsSuccLimit (a ^ succ b)
⊢ IsSuccLimit (a ^ b)
have inr₁ : ∀ (l' : IsSuccLimit b), IsSuccLimit (a ^ b)
Tactic: rcases zero_or_succ_or_isSuccLimit b with (e | ⟨b, rfl⟩ | l')
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a : Ordinal.{u_1}
l : IsSuccLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsSuccLimit (a ^ succ b)
have inr : IsSuccLimit (a ^ b * a)
Tactic: rw [opow_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
h₁ : 0 < a
h₂ : b ≤ c
⊢ a ^ b ≤ a ^ c
have inl : ∀ (h₁ : a = 1), a ^ b ≤ a ^ c
Tactic: rcases (one_le_iff_pos.2 h₁).eq_or_lt' with h₁ | h₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
h₁ : 0 < a
h₂ : b ≤ c
inl : ∀ (h₁ : a = 1), a ^ b ≤ a ^ c
⊢ a ^ b ≤ a ^ c
have inr : ∀ (h₁ : 1 < a), a ^ b ≤ a ^ c
Tactic: rcases (one_le_iff_pos.2 h₁).eq_or_lt' with h₁ | h₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
⊢ a ^ c ≤ b ^ c
have pos : ∀ (ha : a = 0), a ^ c ≤ b ^ c
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
pos : ∀ (ha : a = 0), a ^ c ≤ b ^ c
⊢ a ^ c ≤ b ^ c
have neg : ∀ (ha : ¬a = 0), a ^ c ≤ b ^ c
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
⊢ a ^ c ≤ b ^ c
have pos : c = 0 → a ^ c ≤ b ^ c
Tactic: by_cases c = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
pos : c = 0 → a ^ c ≤ b ^ c
⊢ a ^ c ≤ b ^ c
have neg : ¬c = 0 → a ^ c ≤ b ^ c
Tactic: by_cases c = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
⊢ a ^ c ≤ b ^ c
have neg : HPow.hPow (β := Ordinal.{u_1}) a 0 ≤ HPow.hPow (β := Ordinal.{u_1}) b 0
Tactic: induction c using limitRecOn with
    | zero => simp
    | add_one c IH => simpa using mul_le_mul' IH ab
    | limit c l IH =>
      exact (opow_le_of_isSuccLimit ha l).2 fun b' h ↦
        (IH _ h).trans (opow_le_opow_right ((pos_iff_ne_zero.2 ha).trans_le ab) h.le)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
neg : HPow.hPow (β := Ordinal.{u_1}) a 0 ≤ HPow.hPow (β := Ordinal.{u_1}) b 0
⊢ a ^ c ≤ b ^ c
have neg₁ : ∀ (c : Ordinal.{u_1}) (IH : a ^ c ≤ b ^ c), a ^ (c + 1) ≤ b ^ (c + 1)
Tactic: induction c using limitRecOn with
    | zero => simp
    | add_one c IH => simpa using mul_le_mul' IH ab
    | limit c l IH =>
      exact (opow_le_of_isSuccLimit ha l).2 fun b' h ↦
        (IH _ h).trans (opow_le_opow_right ((pos_iff_ne_zero.2 ha).trans_le ab) h.le)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
neg : HPow.hPow (β := Ordinal.{u_1}) a 0 ≤ HPow.hPow (β := Ordinal.{u_1}) b 0
neg₁ : ∀ (c : Ordinal.{u_1}) (IH : a ^ c ≤ b ^ c), a ^ (c + 1) ≤ b ^ (c + 1)
⊢ a ^ c ≤ b ^ c
have neg₂ : ∀ (c : Ordinal.{u_1}) (l : IsSuccLimit c) (IH : ∀ o' < c, a ^ o' ≤ b ^ o'), a ^ c ≤ b ^ c
Tactic: induction c using limitRecOn with
    | zero => simp
    | add_one c IH => simpa using mul_le_mul' IH ab
    | limit c l IH =>
      exact (opow_le_of_isSuccLimit ha l).2 fun b' h ↦
        (IH _ h).trans (opow_le_opow_right ((pos_iff_ne_zero.2 ha).trans_le ab) h.le)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ≤ a ^ b
have nth_rw : HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
Tactic: nth_rw 1 [← opow_one a]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
have inl : ∀ (a1 : a ≤ 1), HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
Tactic: rcases le_or_gt a 1 with a1 | a1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
inl : ∀ (a1 : a ≤ 1), HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
have inr : ∀ (a1 : 1 < a), HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
Tactic: rcases le_or_gt a 1 with a1 | a1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
have inl : ∀ (a0 : a < 1), HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
Tactic: rcases lt_or_eq_of_le a1 with a0 | a1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
inl : ∀ (a0 : a < 1), HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
have inl₁ : ∀ (a1 : a = 1), HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
Tactic: rcases lt_or_eq_of_le a1 with a0 | a1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (hypothesis)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
have a0₁ : a = 0
Tactic: rw [lt_one_iff] at a0
Cleared hypotheses: a0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
have inl : 0 ≤ HPow.hPow (α := Ordinal.{u_1}) 0 b
Tactic: rw [a0, zero_opow one_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1_1 : a ≤ 1
a1 : a = 1
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
have inl : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 1 1 ≤ HPow.hPow (α := Ordinal.{u_1}) 1 b
Tactic: rw [a1, one_opow, one_opow]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1_1 : a ≤ 1
a1 : a = 1
inl : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 1 1 ≤ HPow.hPow (α := Ordinal.{u_1}) 1 b
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
have inl₁ : 1 ≤ HPow.hPow (α := Ordinal.{u_1}) 1 b
Tactic: rw [a1, one_opow, one_opow]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1_1 : a ≤ 1
a1 : a = 1
inl : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 1 1 ≤ HPow.hPow (α := Ordinal.{u_1}) 1 b
inl₁ : 1 ≤ HPow.hPow (α := Ordinal.{u_1}) 1 b
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
have inl₂ : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
Tactic: rw [a1, one_opow, one_opow]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : 1 < a
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
have inr : 1 ≤ b
Tactic: rwa [opow_le_opow_iff_right a1, one_le_iff_pos]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
| a
have rw : HPow.hPow (β := Ordinal.{u_1}) a 1
Tactic: rw [← opow_one a]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
⊢ a < a ^ b
have conv_lhs : HPow.hPow (β := Ordinal.{u_1}) a 1 < a ^ b
Tactic: conv_lhs => rw [← opow_one a]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ succ c < b ^ succ c
have rw : a ^ c * a < b ^ c * b
Tactic: rw [opow_succ, opow_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
⊢ a ^ (b + c) = a ^ b * a ^ c
have inl : HPow.hPow (α := Ordinal.{u_1}) 0 (b + c) = HPow.hPow (α := Ordinal.{u_1}) 0 b * HPow.hPow (α := Ordinal.{u_1}) 0 c
Tactic: obtain rfl | ha := eq_zero_or_pos a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
inl : HPow.hPow (α := Ordinal.{u_1}) 0 (b + c) = HPow.hPow (α := Ordinal.{u_1}) 0 b * HPow.hPow (α := Ordinal.{u_1}) 0 c
⊢ a ^ (b + c) = a ^ b * a ^ c
have inr : ∀ (ha : 0 < a), a ^ (b + c) = a ^ b * a ^ c
Tactic: obtain rfl | ha := eq_zero_or_pos a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b c : Ordinal.{u_1}
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b + c) = HPow.hPow (α := Ordinal.{u_1}) 0 b * HPow.hPow (α := Ordinal.{u_1}) 0 c
have inl : HPow.hPow (α := Ordinal.{u_1}) 0 (b + 0) =
  HPow.hPow (α := Ordinal.{u_1}) 0 b * HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0
Tactic: obtain rfl | hc := eq_zero_or_pos c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b c : Ordinal.{u_1}
inl :
  HPow.hPow (α := Ordinal.{u_1}) 0 (b + 0) =
    HPow.hPow (α := Ordinal.{u_1}) 0 b * HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b + c) = HPow.hPow (α := Ordinal.{u_1}) 0 b * HPow.hPow (α := Ordinal.{u_1}) 0 c
have inl₁ : ∀ (hc : 0 < c),
  HPow.hPow (α := Ordinal.{u_1}) 0 (b + c) = HPow.hPow (α := Ordinal.{u_1}) 0 b * HPow.hPow (α := Ordinal.{u_1}) 0 c
Tactic: obtain rfl | hc := eq_zero_or_pos c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (hypothesis)
Goal:
b c : Ordinal.{u_1}
hc : 0 < c
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b + c) = HPow.hPow (α := Ordinal.{u_1}) 0 b * HPow.hPow (α := Ordinal.{u_1}) 0 c
have this : b + c ≠ 0
Tactic: have : b + c ≠ 0 := (hc.trans_le le_add_self).ne'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ha : 0 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
have inr : ∀ (ha : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 0 1),
  HPow.hPow (α := Ordinal.{u_1}) 1 (b + c) = HPow.hPow (α := Ordinal.{u_1}) 1 b * HPow.hPow (α := Ordinal.{u_1}) 1 c
Tactic: obtain rfl | ha' := (one_le_iff_ne_zero.2 ha.ne').eq_or_lt
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ha : 0 < a
inr :
  ∀ (ha : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 0 1),
    HPow.hPow (α := Ordinal.{u_1}) 1 (b + c) = HPow.hPow (α := Ordinal.{u_1}) 1 b * HPow.hPow (α := Ordinal.{u_1}) 1 c
⊢ a ^ (b + c) = a ^ b * a ^ c
have inr₁ : ∀ (ha' : 1 < a), a ^ (b + c) = a ^ b * a ^ c
Tactic: obtain rfl | ha' := (one_le_iff_ne_zero.2 ha.ne').eq_or_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + (c + 1)) = a ^ b * a ^ (c + 1)
have inr : a ^ (b + c + 1) = a ^ b * a ^ (c + 1)
Tactic: rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
inr : a ^ (b + c + 1) = a ^ b * a ^ (c + 1)
⊢ a ^ (b + (c + 1)) = a ^ b * a ^ (c + 1)
have inr₁ : a ^ (b + c) * a = a ^ b * a ^ (c + 1)
Tactic: rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
inr : a ^ (b + c + 1) = a ^ b * a ^ (c + 1)
inr₁ : a ^ (b + c) * a = a ^ b * a ^ (c + 1)
⊢ a ^ (b + (c + 1)) = a ^ b * a ^ (c + 1)
have inr₂ : a ^ b * a ^ c * a = a ^ b * a ^ (c + 1)
Tactic: rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
inr : a ^ (b + c + 1) = a ^ b * a ^ (c + 1)
inr₁ : a ^ (b + c) * a = a ^ b * a ^ (c + 1)
inr₂ : a ^ b * a ^ c * a = a ^ b * a ^ (c + 1)
⊢ a ^ (b + (c + 1)) = a ^ b * a ^ (c + 1)
have inr₃ : a ^ b * a ^ c * a = a ^ b * (a ^ c * a)
Tactic: rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
inr : a ^ (b + c + 1) = a ^ b * a ^ (c + 1)
inr₁ : a ^ (b + c) * a = a ^ b * a ^ (c + 1)
inr₂ : a ^ b * a ^ c * a = a ^ b * a ^ (c + 1)
inr₃ : a ^ b * a ^ c * a = a ^ b * (a ^ c * a)
⊢ a ^ (b + (c + 1)) = a ^ b * a ^ (c + 1)
have inr₄ : a ^ b * (a ^ c * a) = a ^ b * (a ^ c * a)
Tactic: rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
⊢ a ^ (b + c) = a ^ b * a ^ c
have inr : ∀ (d : Ordinal.{u_1}),
  (∀ a' < c, ((fun (x : Ordinal.{u_1}) ↦ a ^ x) ∘ fun (x : Ordinal.{u_1}) ↦ b + x) a' ≤ d) ↔ a ^ b * a ^ c ≤ d
Tactic: refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
have inr : a ^ (b + 0) = a ^ b * HPow.hPow (β := Ordinal.{u_1}) a 0
Tactic: induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using
      (((isNormal_mul_right <| opow_pos b (pos_iff_ne_zero.2 ha.ne')).comp
        (isNormal_opow ha')).le_iff_forall_le l).symm
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
inr : a ^ (b + 0) = a ^ b * HPow.hPow (β := Ordinal.{u_1}) a 0
⊢ a ^ (b + c) = a ^ b * a ^ c
have inr₁ : ∀ (c : Ordinal.{u_1}) (IH : a ^ (b + c) = a ^ b * a ^ c), a ^ (b + (c + 1)) = a ^ b * a ^ (c + 1)
Tactic: induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using
      (((isNormal_mul_right <| opow_pos b (pos_iff_ne_zero.2 ha.ne')).comp
        (isNormal_opow ha')).le_iff_forall_le l).symm
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
inr : a ^ (b + 0) = a ^ b * HPow.hPow (β := Ordinal.{u_1}) a 0
inr₁ : ∀ (c : Ordinal.{u_1}) (IH : a ^ (b + c) = a ^ b * a ^ c), a ^ (b + (c + 1)) = a ^ b * a ^ (c + 1)
⊢ a ^ (b + c) = a ^ b * a ^ c
have inr₂ : ∀ (c : Ordinal.{u_1}) (l : IsSuccLimit c) (IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'), a ^ (b + c) = a ^ b * a ^ c
Tactic: induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using
      (((isNormal_mul_right <| opow_pos b (pos_iff_ne_zero.2 ha.ne')).comp
        (isNormal_opow ha')).le_iff_forall_le l).symm
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a ^ (1 + b) = a * a ^ b
have rw : HPow.hPow (β := Ordinal.{u_1}) a 1 * a ^ b = a * a ^ b
Tactic: rw [opow_add, opow_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
rw : HPow.hPow (β := Ordinal.{u_1}) a 1 * a ^ b = a * a ^ b
⊢ a ^ (1 + b) = a * a ^ b
have rw₁ : a * a ^ b = a * a ^ b
Tactic: rw [opow_add, opow_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
h : b ≤ c
⊢ a ^ c = a ^ b * a ^ (c - b)
have rw : a ^ c = a ^ (b + (c - b))
Tactic: rw [← opow_add, Ordinal.add_sub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
h : b ≤ c
rw : a ^ c = a ^ (b + (c - b))
⊢ a ^ c = a ^ b * a ^ (c - b)
have rw₁ : a ^ c = a ^ c
Tactic: rw [← opow_add, Ordinal.add_sub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
⊢ a ^ (b * c) = (a ^ b) ^ c
have inl : a ^ (0 * c) = HPow.hPow (β := Ordinal.{u_1}) a 0 ^ c
Tactic: obtain rfl | hb := eq_zero_or_pos b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
inl : a ^ (0 * c) = HPow.hPow (β := Ordinal.{u_1}) a 0 ^ c
⊢ a ^ (b * c) = (a ^ b) ^ c
have inr : ∀ (hb : 0 < b), a ^ (b * c) = (a ^ b) ^ c
Tactic: obtain rfl | hb := eq_zero_or_pos b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
hb : 0 < b
⊢ a ^ (b * c) = (a ^ b) ^ c
have inr : HPow.hPow (α := Ordinal.{u_1}) 0 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 0 b ^ c
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
hb : 0 < b
inr : HPow.hPow (α := Ordinal.{u_1}) 0 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 0 b ^ c
⊢ a ^ (b * c) = (a ^ b) ^ c
have inr₁ : ∀ (ha : a ≠ 0), a ^ (b * c) = (a ^ b) ^ c
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (hypothesis)
Goal:
b c : Ordinal.{u_1}
hb : 0 < b
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 0 b ^ c
have this : b ≠ 0
Tactic: have := hb.ne'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 0 b ^ c
have pos : c = 0 → HPow.hPow (α := Ordinal.{u_1}) 0 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 0 b ^ c
Tactic: by_cases c = 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
pos : c = 0 → HPow.hPow (α := Ordinal.{u_1}) 0 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 0 b ^ c
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 0 b ^ c
have neg : ¬c = 0 → HPow.hPow (α := Ordinal.{u_1}) 0 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 0 b ^ c
Tactic: by_cases c = 0