awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ log b x = y
have mpr : log b x ≤ y
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
mpr : log b x ≤ y
⊢ log b x = y
have mpr₁ : y ≤ log b x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ log b x ≤ y
have mpr : log b x < y + 1
Tactic: rwa [← lt_add_one_iff, ← lt_opow_iff_log_lt hb hx]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ log b (b ^ u * v + w) = u + log b v
have rw : b ^ (u + log b v) ≤ b ^ u * v + w ∧ b ^ u * v + w < b ^ (u + log b v + 1)
Tactic: rw [log_eq_iff hb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
rw : b ^ (u + log b v) ≤ b ^ u * v + w ∧ b ^ u * v + w < b ^ (u + log b v + 1)
⊢ log b (b ^ u * v + w) = u + log b v
have hx : b ^ u * v + w ≠ 0
Tactic: rw [log_eq_iff hb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ (u + log b v) ≤ b ^ u * v + w ∧ b ^ u * v + w < b ^ (u + log b v + 1)
have left : b ^ (u + log b v) ≤ b ^ u * v + w
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
left : b ^ (u + log b v) ≤ b ^ u * v + w
⊢ b ^ (u + log b v) ≤ b ^ u * v + w ∧ b ^ u * v + w < b ^ (u + log b v + 1)
have right : b ^ u * v + w < b ^ (u + log b v + 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ (u + log b v) ≤ b ^ u * v + w
have left : b ^ u * b ^ log b v ≤ b ^ u * v + w
Tactic: grw [opow_add, opow_log_le_self b hv, ← le_self_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
left : b ^ u * b ^ log b v ≤ b ^ u * v + w
⊢ b ^ (u + log b v) ≤ b ^ u * v + w
have left₁ : b ^ u * v ≤ b ^ u * v + w
Tactic: grw [opow_add, opow_log_le_self b hv, ← le_self_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
left : b ^ u * b ^ log b v ≤ b ^ u * v + w
left₁ : b ^ u * v ≤ b ^ u * v + w
⊢ b ^ (u + log b v) ≤ b ^ u * v + w
have left₂ : b ^ u * v ≤ b ^ u * v
Tactic: grw [opow_add, opow_log_le_self b hv, ← le_self_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ (u + log b v + 1)
have right : b ^ u * v + b ^ u ≤ b ^ (u + log b v + 1)
Tactic: apply (add_lt_add_right hw _).trans_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + b ^ u ≤ b ^ (u + log b v + 1)
have right : b ^ u * (v + 1) ≤ b ^ u * b ^ (log b v + 1)
Tactic: rw [← mul_add_one, add_assoc, opow_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * (v + 1) ≤ b ^ u * b ^ (log b v + 1)
have right : v + 1 ≤ b ^ (log b v + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ v + 1 ≤ b ^ (log b v + 1)
have right : v < b ^ (log b v + 1)
Tactic: rw [add_one_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = x
have h : log b (b ^ x) = log b (b ^ x * 1)
Tactic: convert! log_opow_mul hb x zero_ne_one.symm using 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
h : log b (b ^ x) = log b (b ^ x * 1)
⊢ log b (b ^ x) = x
have h₁ : x = x + log b 1
Tactic: convert! log_opow_mul hb x zero_ne_one.symm using 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = log b (b ^ x * 1)
have h : log b (b ^ x) = log b (b ^ x)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x = x + log b 1
have h : x = x + 0
Tactic: rw [log_one_right, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
h : x = x + 0
⊢ x = x + log b 1
have h₁ : x = x
Tactic: rw [log_one_right, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / b ^ log b o
have inl : 0 < o / HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 o)
Tactic: rcases eq_zero_or_pos b with (rfl | hb)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
inl : 0 < o / HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 o)
⊢ 0 < o / b ^ log b o
have inr : ∀ (hb : 0 < b), 0 < o / b ^ log b o
Tactic: rcases eq_zero_or_pos b with (rfl | hb)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ 0 < o / b ^ log b o
have inr : b ^ log b o ≤ o
Tactic: rw [div_pos (opow_ne_zero _ hb.ne')]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o / b ^ log b o < b
have rw : o < b ^ succ (log b o)
Tactic: rw [← lt_mul_iff_div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) = 1
have a : o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) ≤ 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
a : o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) ≤ 1
⊢ o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) = 1
have a₁ : 1 ≤ o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) + o % HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) = o
have h : HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) =
  HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) * (o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o))
Tactic: convert! div_add_mod .. using 2
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) =
    HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) * (o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o))
have h : HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) = HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) * 1
Tactic: rw [div_two_opow_log ho, mul_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
h : HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) = HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) * 1
⊢ HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) =
    HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) * (o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o))
have h₁ : HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) = HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o)
Tactic: rw [div_two_opow_log ho, mul_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
⊢ log b x + log b y ≤ log b (x * y)
have inl : ∀ (hb : 1 < b), log b x + log b y ≤ log b (x * y)
Tactic: obtain hb | hb := lt_or_ge 1 b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
inl : ∀ (hb : 1 < b), log b x + log b y ≤ log b (x * y)
⊢ log b x + log b y ≤ log b (x * y)
have inr : ∀ (hb : b ≤ 1), log b x + log b y ≤ log b (x * y)
Tactic: obtain hb | hb := lt_or_ge 1 b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ log b x + log b y ≤ log b (x * y)
have inl : b ^ log b x * b ^ log b y ≤ x * y
Tactic: rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ b
have apply : ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ succ a
Tactic: apply lt_of_lt_of_le _ (opow_le_opow_right omega0_pos (succ_le_of_lt h))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ succ a
have rw : ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ a * ω
Tactic: rw [opow_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ a * ω
have ha : 0 < ω ^ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
ha : 0 < ω ^ a
⊢ ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ a * ω
have hbc : (↑n : Ordinal.{u_1}) < ω
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ a < ω ^ b ↔ ∃ c < b, ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})
have refine : ∀ (ha : a < ω ^ b), ∃ (n : ℕ), a < ω ^ log ω a * (↑n : Ordinal.{u_1})
Tactic: refine ⟨fun ha ↦ ⟨_, lt_log_of_lt_opow hb ha, ?_⟩,
    fun ⟨c, hc, n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt hc n)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
⊢ ∃ (n : ℕ), a < ω ^ log ω a * (↑n : Ordinal.{u_1})
have obtain : ∀ (n : ℕ) (hn : a / ω ^ log ω a = (↑n : Ordinal.{u_1})), ∃ (n : ℕ), a < ω ^ log ω a * (↑n : Ordinal.{u_1})
Tactic: obtain ⟨n, hn⟩ := lt_omega0.1 (div_opow_log_lt a one_lt_omega0)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = (↑n : Ordinal.{u_1})
⊢ ∃ (n : ℕ), a < ω ^ log ω a * (↑n : Ordinal.{u_1})
have h : a < ω ^ log ω a * (↑(n + 1) : Ordinal.{u_1})
Tactic: use n + 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = (↑n : Ordinal.{u_1})
⊢ a < ω ^ log ω a * (↑(n + 1) : Ordinal.{u_1})
have h : a < ω ^ log ω a * (a / ω ^ log ω a + 1)
Tactic: rw [Nat.cast_add_one, ← hn]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a < ω ^ succ b ↔ ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})
have refine : ∀ (ha : a < ω ^ succ b), ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})
Tactic: refine ⟨fun ha ↦ ?_, fun ⟨n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt (lt_succ b) n)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
⊢ ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})
have obtain : ∀ (c : Ordinal.{u_1}) (hc : c < b + 1) (n : ℕ) (hn : a < ω ^ c * (↑n : Ordinal.{u_1})),
  ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})
Tactic: obtain ⟨c, hc, n, hn⟩ := (lt_omega0_opow (add_pos_of_right zero_lt_one b).ne').1 ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * (↑n : Ordinal.{u_1})
⊢ ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})
have refine : ω ^ c * (↑n : Ordinal.{u_1}) ≤ ω ^ b * (↑n : Ordinal.{u_1})
Tactic: refine ⟨n, hn.trans_le ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * (↑n : Ordinal.{u_1})
⊢ ω ^ c * (↑n : Ordinal.{u_1}) ≤ ω ^ b * (↑n : Ordinal.{u_1})
have h₁ : 0 < ω
Tactic: grw [lt_succ_iff.1 hc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ a < ω ^ ω ^ b ↔ ∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))
have simp_rw : (∃ (c : Ordinal.{u_1}),
    (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})) ↔
  ∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))
Tactic: simp_rw [lt_omega0_opow (opow_ne_zero _ omega0_ne_zero), lt_omega0_opow hb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (∃ (c : Ordinal.{u_1}),
      (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})) ↔
    ∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))
have mp : (∃ (c : Ordinal.{u_1}),
    (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})) →
  ∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
mp :
  (∃ (c : Ordinal.{u_1}),
      (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})) →
    ∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))
⊢ (∃ (c : Ordinal.{u_1}),
      (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})) ↔
    ∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))
have mpr : (∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))) →
  ∃ (c : Ordinal.{u_1}),
    (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a_1 b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a_1 < ω ^ (ω ^ a * (↑n : Ordinal.{u_1}))
⊢ ∃ (c : Ordinal.{u_1}),
    (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a_1 < ω ^ c * (↑n : Ordinal.{u_1})
have mpr : ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ a * (↑(n + 1) : Ordinal.{u_1})
Tactic: refine ⟨ω ^ a * n, ⟨a, ha, n + 1, ?_⟩, 1, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a_1 b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a_1 < ω ^ (ω ^ a * (↑n : Ordinal.{u_1}))
mpr : ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ a * (↑(n + 1) : Ordinal.{u_1})
⊢ ∃ (c : Ordinal.{u_1}),
    (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a_1 < ω ^ c * (↑n : Ordinal.{u_1})
have mpr₁ : a_1 < ω ^ (ω ^ a * (↑n : Ordinal.{u_1})) * (↑1 : Ordinal.{u_1})
Tactic: refine ⟨ω ^ a * n, ⟨a, ha, n + 1, ?_⟩, 1, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
o : Ordinal.{u_1}
ho : 0 < o
⊢ ⨆ (n : ℕ), o ^ n = o ^ ω
have inl : ∀ (ho₁ : 1 < o), ⨆ (n : ℕ), o ^ n = o ^ ω
Tactic: rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
o : Ordinal.{u_1}
ho : 0 < o
inl : ∀ (ho₁ : 1 < o), ⨆ (n : ℕ), o ^ n = o ^ ω
⊢ ⨆ (n : ℕ), o ^ n = o ^ ω
have inr : ∀ (ho : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 0 1),
  ⨆ (n : ℕ), HPow.hPow (α := Ordinal.{u_1}) 1 n = HPow.hPow (α := Ordinal.{u_1}) 1 ω
Tactic: rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
m n : ℕ
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
have obtain : ∀ (hm : m ≤ 1), (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
Tactic: obtain hm | hm := le_or_gt m 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
m n : ℕ
obtain : ∀ (hm : m ≤ 1), (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
have inr : ∀ (hm : 1 < m), (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
Tactic: obtain hm | hm := le_or_gt m 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
m n : ℕ
hm : m ≤ 1
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
have rw_mod_cast : (↑0 : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
Tactic: rw_mod_cast [Nat.log_of_left_le_one hm, log_of_left_le_one (mod_cast hm)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
m n : ℕ
hm : 1 < m
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
have obtain : (↑(Nat.log m 0) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑0 : Ordinal.{u_1})
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
m n : ℕ
hm : 1 < m
obtain : (↑(Nat.log m 0) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑0 : Ordinal.{u_1})
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
have inr : ∀ (hn : n ≠ 0), (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
m n : ℕ
hm : 1 < m
hn : n ≠ 0
inr inr₁ inr₂ inr₃ inr₄ inr₅ : (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
have inr₆ : log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1}) = (↑(Nat.log m n) : Ordinal.{u_1})
Tactic: rw_mod_cast [eq_comm, log_eq_iff (mod_cast hm) (mod_cast hn), ← Nat.log_eq_iff (.inr ⟨hm, hn⟩)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
m n : ℕ
hm : 1 < m
hn : n ≠ 0
inr inr₁ inr₂ inr₃ inr₄ inr₅ : (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
inr₆ : log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1}) = (↑(Nat.log m n) : Ordinal.{u_1})
⊢ (↑(Nat.log m n) : Ordinal.{u_1}) = log (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1})
have inr₇ : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) (↑m : Ordinal.{u_1}) (↑(Nat.log m n) : Ordinal.{u_1}) ≤
    (↑n : Ordinal.{u_1}) ∧
  (↑n : Ordinal.{u_1}) <
    HPow.hPow (α := Ordinal.{u_1}) (↑m : Ordinal.{u_1})
      (HAdd.hAdd (α := Ordinal.{u_1}) (↑(Nat.log m n) : Ordinal.{u_1}) 1)
Tactic: rw_mod_cast [eq_comm, log_eq_iff (mod_cast hm) (mod_cast hn), ← Nat.log_eq_iff (.inr ⟨hm, hn⟩)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : ι
⊢ ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : ι) → Ordinal.{u}) i < o
have rw : ((typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : ι) → Ordinal.{u}) i < type r
Tactic: rw [← ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ i ∈ Iio (type r)
have rwa : i ∈ Iio o
Tactic: rwa [ho]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
⊢ range (familyOfBFamily' r ho f) = o.brange f
have refine_1 : ∀ a ∈ range (familyOfBFamily' r ho f), a ∈ o.brange f
Tactic: refine Set.ext fun a => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
refine_1 : ∀ a ∈ range (familyOfBFamily' r ho f), a ∈ o.brange f
⊢ range (familyOfBFamily' r ho f) = o.brange f
have refine_2 : ∀ a ∈ o.brange f, a ∈ range (familyOfBFamily' r ho f)
Tactic: refine Set.ext fun a => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → α
⊢ (type r).brange (bfamilyOfFamily' r f) = range f
have refine_1 : ∀ a ∈ (type r).brange (bfamilyOfFamily' r f), a ∈ range f
Tactic: refine Set.ext fun a => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst : IsWellOrder ι r
f : ι → α
refine_1 : ∀ a ∈ (type r).brange (bfamilyOfFamily' r f), a ∈ range f
⊢ (type r).brange (bfamilyOfFamily' r f) = range f
have refine_2 : ∀ a ∈ range f, a ∈ (type r).brange (bfamilyOfFamily' r f)
Tactic: refine Set.ext fun a => ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_1
o : Ordinal.{u_3}
ho : o ≠ 0
c : α
⊢ Eq (α := Set α) (o.brange fun (x : Ordinal.{u_3}) (x_1 : x < o) ↦ c) {c}
have rw : Eq (α := Set α) (range (o.familyOfBFamily fun (x : Ordinal.{u_3}) (x_1 : x < o) ↦ c)) {c}
Tactic: rw [← range_familyOfBFamily]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u}
inst : Small.{u, u + 1} (↑s : Type (u + 1))
⊢ BddAbove s
have obtain : ∀ (a : Cardinal.{u}) (ha : a ∈ upperBounds (succ ∘ card '' s)), BddAbove s
Tactic: obtain ⟨a, ha⟩ := Cardinal.bddAbove_of_small (s := (succ ∘ card) '' s)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u}
inst : Small.{u, u + 1} (↑s : Type (u + 1))
a : Cardinal.{u}
ha : a ∈ upperBounds (succ ∘ card '' s)
⊢ BddAbove s
have refine : ∀ (b : Ordinal.{u}) (hb : b ∈ s), b < a.ord
Tactic: refine ⟨a.ord, fun b hb ↦ le_of_lt ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
s : Set Ordinal.{u}
hf : BddAbove s
f : Ordinal.{u} → Ordinal.{max u v}
⊢ BddAbove (f '' s)
have rw : ∀ (hf : Small.{u, u + 1} (↑s : Type (u + 1))) (f : Ordinal.{u} → Ordinal.{max u v}),
  Small.{max u v, (max u v) + 1} (↑(f '' s) : Type ((max u v) + 1))
Tactic: rw [bddAbove_iff_small] at hf ⊢
Cleared hypotheses: hf, f
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
g : Ordinal.{v} → Ordinal.{max v w}
⊢ BddAbove (range (g ∘ f))
have rw : BddAbove (g '' range f)
Tactic: rw [range_comp]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
i : ι
⊢ f i < ⨆ (i : ι), f i + 1
have rw : f i + 1 ≤ ⨆ (i : ι), f i + 1
Tactic: rw [← add_one_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
⊢ succ a < iSup f
have by_contra! : ∀ (hoa : iSup f ≤ succ a), False
Tactic: by_contra! hoa
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
⊢ iSup f = 0 ↔ ∀ (i : ι), f i = 0
have h : ∀ (h : iSup f = 0) (i : ι), f i = 0
Tactic: refine
    ⟨fun h i => ?_, fun h =>
      le_antisymm (Ordinal.iSup_le fun i => nonpos_iff_eq_zero.2 (h i)) zero_le⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
ι : Type u_3
f : ι → Ordinal.{u}
inst : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i = 0
have rw : f i ≤ iSup f
Tactic: rw [← nonpos_iff_eq_zero, ← h]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Family (goal)
Goal:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst : Small.{u, u_3} α
inst_1 : Small.{u, u_4} β
⊢ iSup f = max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))
have apply : ∀ (i : α ⊕ β), f i ≤ max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))
Tactic: apply (Ordinal.iSup_le _).antisymm (max_le _ _)