awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
⊢ a ^ (b * c) = (a ^ b) ^ c
have inr : ∀ (ha : Ne.{u_1 + 2} (α := Ordinal.{u_1}) 1 0),
  HPow.hPow (α := Ordinal.{u_1}) 1 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 1 b ^ c
Tactic: obtain rfl | ha' := (one_le_iff_ne_zero.2 ha).eq_or_lt
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
inr :
  ∀ (ha : Ne.{u_1 + 2} (α := Ordinal.{u_1}) 1 0),
    HPow.hPow (α := Ordinal.{u_1}) 1 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 1 b ^ c
⊢ a ^ (b * c) = (a ^ b) ^ c
have inr₁ : ∀ (ha' : 1 < a), a ^ (b * c) = (a ^ b) ^ c
Tactic: obtain rfl | ha' := (one_le_iff_ne_zero.2 ha).eq_or_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b * c) = (a ^ b) ^ c
⊢ a ^ (b * (c + 1)) = (a ^ b) ^ (c + 1)
have inr : a ^ (b * c + b) = (a ^ b) ^ (c + 1)
Tactic: rw [mul_add_one, opow_add, IH, opow_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b * c) = (a ^ b) ^ c
inr : a ^ (b * c + b) = (a ^ b) ^ (c + 1)
⊢ a ^ (b * (c + 1)) = (a ^ b) ^ (c + 1)
have inr₁ : a ^ (b * c) * a ^ b = (a ^ b) ^ (c + 1)
Tactic: rw [mul_add_one, opow_add, IH, opow_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b * c) = (a ^ b) ^ c
inr : a ^ (b * c + b) = (a ^ b) ^ (c + 1)
inr₁ : a ^ (b * c) * a ^ b = (a ^ b) ^ (c + 1)
⊢ a ^ (b * (c + 1)) = (a ^ b) ^ (c + 1)
have inr₂ : (a ^ b) ^ c * a ^ b = (a ^ b) ^ (c + 1)
Tactic: rw [mul_add_one, opow_add, IH, opow_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b * c) = (a ^ b) ^ c
inr : a ^ (b * c + b) = (a ^ b) ^ (c + 1)
inr₁ : a ^ (b * c) * a ^ b = (a ^ b) ^ (c + 1)
inr₂ : (a ^ b) ^ c * a ^ b = (a ^ b) ^ (c + 1)
⊢ a ^ (b * (c + 1)) = (a ^ b) ^ (c + 1)
have inr₃ : (a ^ b) ^ c * a ^ b = (a ^ b) ^ c * a ^ b
Tactic: rw [mul_add_one, opow_add, IH, opow_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b * o') = (a ^ b) ^ o'
⊢ a ^ (b * c) = (a ^ b) ^ 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) ^ c ≤ d
Tactic: refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_mul_right hb)).le_iff_forall_le l).trans ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c
have inr : a ^ (b * 0) = HPow.hPow (β := Ordinal.{u_1}) (a ^ b) 0
Tactic: induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [mul_add_one, opow_add, IH, opow_add_one]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_mul_right hb)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using (opow_le_of_isSuccLimit (opow_ne_zero _ ha) l).symm
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
inr : a ^ (b * 0) = HPow.hPow (β := Ordinal.{u_1}) (a ^ b) 0
⊢ a ^ (b * c) = (a ^ b) ^ c
have inr₁ : ∀ (c : Ordinal.{u_1}) (IH : a ^ (b * c) = (a ^ b) ^ c), a ^ (b * (c + 1)) = (a ^ b) ^ (c + 1)
Tactic: induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [mul_add_one, opow_add, IH, opow_add_one]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_mul_right hb)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using (opow_le_of_isSuccLimit (opow_ne_zero _ ha) l).symm
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
inr : a ^ (b * 0) = HPow.hPow (β := Ordinal.{u_1}) (a ^ b) 0
inr₁ : ∀ (c : Ordinal.{u_1}) (IH : a ^ (b * c) = (a ^ b) ^ c), a ^ (b * (c + 1)) = (a ^ b) ^ (c + 1)
⊢ a ^ (b * c) = (a ^ b) ^ c
have inr₂ : ∀ (c : Ordinal.{u_1}) (l : IsSuccLimit c) (IH : ∀ o' < c, a ^ (b * o') = (a ^ b) ^ o'), a ^ (b * c) = (a ^ b) ^ c
Tactic: induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [mul_add_one, opow_add, IH, opow_add_one]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_mul_right hb)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using (opow_le_of_isSuccLimit (opow_ne_zero _ ha) l).symm
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * x
have hab : b ^ u * v + w < b ^ u * (v + 1)
Tactic: apply lt_of_lt_of_le (b := b ^ u * (v + 1))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
hab : b ^ u * v + w < b ^ u * (v + 1)
⊢ b ^ u * v + w < b ^ u * x
have hbc : b ^ u * (v + 1) ≤ b ^ u * x
Tactic: apply lt_of_lt_of_le (b := b ^ u * (v + 1))
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * (v + 1)
have hab : b ^ u * v + w < b ^ u * v + b ^ u
Tactic: rwa [mul_add_one, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * (v + 1) ≤ b ^ u * x
have hbc : b ^ u * x ≤ b ^ u * x
Tactic: grw [add_one_le_of_lt hv]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ u * v + w < b ^ x
have apply : b ^ u * b ≤ b ^ x
Tactic: apply (opow_mul_add_lt_opow_mul hw hv).trans_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ u * b ≤ b ^ x
have rw : b ^ succ u ≤ b ^ x
Tactic: rw [← opow_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
h : b ≤ 1
x : Ordinal.{u_1}
⊢ log b x = 0
have inl : ∀ (h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1), log 0 x = 0
Tactic: obtain rfl | rfl := le_one_iff.1 h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
h : b ≤ 1
x : Ordinal.{u_1}
inl : ∀ (h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1), log 0 x = 0
⊢ log b x = 0
have inr : ∀ (h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1), log 1 x = 0
Tactic: obtain rfl | rfl := le_one_iff.1 h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
x : Ordinal.{u_1}
h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
⊢ log 0 x = 0
have apply : ¬BddAbove (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ HPow.hPow (α := Ordinal.{u_1}) 0 x) ⁻¹' Iic x)
Tactic: apply (csSup_of_not_bddAbove _).trans csSup_empty
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
x : Ordinal.{u_1}
h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
hb : BddAbove (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ HPow.hPow (α := Ordinal.{u_1}) 0 x) ⁻¹' Iic x)
⊢ False
have refine : ∀ (a : Ordinal.{u_1}),
  Membership.mem (γ := Set Ordinal.{u_1}) (Ici 1) a →
    Membership.mem (γ := Set Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ HPow.hPow (α := Ordinal.{u_1}) 0 x) ⁻¹' Iic x) a
Tactic: refine not_bddAbove_Ici 1 (hb.mono fun a ↦ ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
x : Ordinal.{u_1}
h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
⊢ log 1 x = 0
have inr : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup (if 1 ∈ Iic x then univ else ∅)) 0
Tactic: simp_rw [log, one_opow, preimage_const]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
x : Ordinal.{u_1}
h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup (if 1 ∈ Iic x then univ else ∅)) 0
have pos : 1 ∈ Iic x → Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup univ) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
x : Ordinal.{u_1}
h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
pos : 1 ∈ Iic x → Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup univ) 0
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup (if 1 ∈ Iic x then univ else ∅)) 0
have neg : 1 ∉ Iic x → Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup ∅) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
⊢ log b 0 = 0
have inl : log 0 0 = 0
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
inl : log 0 0 = 0
⊢ log b 0 = 0
have inr : ∀ (hb : b ≠ 0), log b 0 = 0
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup (preimage (β := Ordinal.{u_1}) (fun (x : Ordinal.{u_1}) ↦ b ^ x) (Iic 0))) 0
have h : Eq.{u_1 + 2} (α := Set Ordinal.{u_1}) (preimage (β := Ordinal.{u_1}) (fun (x : Ordinal.{u_1}) ↦ b ^ x) (Iic 0)) ∅
Tactic: convert! csSup_empty
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x
have inl : b ^ c ≤ 0 ↔ c ≤ log b 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
inl : b ^ c ≤ 0 ↔ c ≤ log b 0
⊢ b ^ c ≤ x ↔ c ≤ log b x
have inr : ∀ (hx : x ≠ 0), b ^ c ≤ x ↔ c ≤ log b x
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
⊢ c ≤ log b x
have inl : ∀ (h : b ^ c ≤ 0), c ≤ log b 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
inl : ∀ (h : b ^ c ≤ 0), c ≤ log b 0
⊢ c ≤ log b x
have inr : ∀ (hx : x ≠ 0), c ≤ log b x
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (hypothesis)
Goal:
b c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ 0
⊢ c ≤ log b 0
have h₁ : b = 0 ∧ c ≠ 0
Tactic: rw [nonpos_iff_eq_zero, opow_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
⊢ b ^ c ≤ x
have inl : ∀ (hb : b ≤ 1), b ^ c ≤ x
Tactic: obtain hb | hb := le_or_gt b 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
inl : ∀ (hb : b ≤ 1), b ^ c ≤ x
⊢ b ^ c ≤ x
have inr : ∀ (hb : 1 < b), b ^ c ≤ x
Tactic: obtain hb | hb := le_or_gt b 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (hypothesis)
Goal:
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : b ≤ 1
⊢ b ^ c ≤ x
have h₁ : c ≤ 0
Tactic: rw [log_of_left_le_one hb] at h
Cleared hypotheses: h, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x < b ^ succ (log b x)
have inl : 0 < b ^ succ (log b 0)
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
inl : 0 < b ^ succ (log b 0)
⊢ x < b ^ succ (log b x)
have inr : ∀ (hx : x ≠ 0), x < b ^ succ (log b x)
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)
have inr : log b x < succ (log b x)
Tactic: rw [lt_opow_iff_log_lt hb hx, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
inr : log b x < succ (log b x)
⊢ x < b ^ succ (log b x)
have inr₁ : log b x ≤ log b x
Tactic: rw [lt_opow_iff_log_lt hb hx, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ b ^ log b x ≤ x
have inl : ∀ (hb : b ≤ 1), b ^ log b x ≤ x
Tactic: obtain hb | hb := le_or_gt b 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
inl : ∀ (hb : b ≤ 1), b ^ log b x ≤ x
⊢ b ^ log b x ≤ x
have inr : ∀ (hb : 1 < b), b ^ log b x ≤ x
Tactic: obtain hb | hb := le_or_gt b 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (hypothesis)
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ b ^ log b x ≤ x
have hx₁ : 1 ≤ x
Tactic: rw [← one_le_iff_ne_zero] at hx
Cleared hypotheses: hx, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hx : 1 ≤ x
hb : b ≤ 1
⊢ b ^ log b x ≤ x
have inl : ∀ (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1), HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 x) ≤ x
Tactic: obtain rfl | rfl := le_one_iff.1 hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hx : 1 ≤ x
hb : b ≤ 1
inl : ∀ (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1), HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 x) ≤ x
⊢ b ^ log b x ≤ x
have inl₁ : ∀ (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1), HPow.hPow (α := Ordinal.{u_1}) 1 (log 1 x) ≤ x
Tactic: obtain rfl | rfl := le_one_iff.1 hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x
have inr : log b x ≤ log b x
Tactic: rw [opow_le_iff_le_log hb hx]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ 0 < log b o
have rwa : HAdd.hAdd (α := Ordinal.{u_1}) 0 1 ≤ log b o
Tactic: rwa [← add_one_le_iff, zero_add, ← opow_le_iff_le_log hb ho, opow_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
rwa : HAdd.hAdd (α := Ordinal.{u_1}) 0 1 ≤ log b o
⊢ 0 < log b o
have rwa₁ : 1 ≤ log b o
Tactic: rwa [← add_one_le_iff, zero_add, ← opow_le_iff_le_log hb ho, opow_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
rwa : HAdd.hAdd (α := Ordinal.{u_1}) 0 1 ≤ log b o
rwa₁ : 1 ≤ log b o
⊢ 0 < log b o
have rwa₂ : HPow.hPow (β := Ordinal.{u_1}) b 1 ≤ o
Tactic: rwa [← add_one_le_iff, zero_add, ← opow_le_iff_le_log hb ho, opow_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hbo : o < b
⊢ log b o = 0
have inl : ∀ (hbo : 0 < b), log b 0 = 0
Tactic: rcases eq_or_ne o 0 with (rfl | ho)
Cleared hypotheses: o, hbo
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hbo : o < b
inl : ∀ (hbo : 0 < b), log b 0 = 0
⊢ log b o = 0
have inr : ∀ (ho : o ≠ 0), log b o = 0
Tactic: rcases eq_or_ne o 0 with (rfl | ho)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
⊢ log b o = 0
have inr : ∀ (hb : b ≤ 1), log b o = 0
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
inr : ∀ (hb : b ≤ 1), log b o = 0
⊢ log b o = 0
have inr₁ : ∀ (hb : 1 < b), log b o = 0
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : b ≤ 1
⊢ log b o = 0
have inr : ∀ (hbo : o < 0) (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1), log 0 o = 0
Tactic: rcases le_one_iff.1 hb with (rfl | rfl)
Cleared hypotheses: b, hbo, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : b ≤ 1
inr : ∀ (hbo : o < 0) (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1), log 0 o = 0
⊢ log b o = 0
have inr₁ : ∀ (hbo : o < 1) (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1), log 1 o = 0
Tactic: rcases le_one_iff.1 hb with (rfl | rfl)
Cleared hypotheses: b, hbo, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o = 0
have inr : log b o ≤ 0
Tactic: rwa [← nonpos_iff_eq_zero, ← lt_add_one_iff, zero_add, ← lt_opow_iff_log_lt hb ho, opow_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
inr : log b o ≤ 0
⊢ log b o = 0
have inr₁ : log b o < HAdd.hAdd (α := Ordinal.{u_1}) 0 1
Tactic: rwa [← nonpos_iff_eq_zero, ← lt_add_one_iff, zero_add, ← lt_opow_iff_log_lt hb ho, opow_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
inr : log b o ≤ 0
inr₁ : log b o < HAdd.hAdd (α := Ordinal.{u_1}) 0 1
⊢ log b o = 0
have inr₂ : log b o < 1
Tactic: rwa [← nonpos_iff_eq_zero, ← lt_add_one_iff, zero_add, ← lt_opow_iff_log_lt hb ho, opow_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
inr : log b o ≤ 0
inr₁ : log b o < HAdd.hAdd (α := Ordinal.{u_1}) 0 1
inr₂ : log b o < 1
⊢ log b o = 0
have inr₃ : o < HPow.hPow (β := Ordinal.{u_1}) b 1
Tactic: rwa [← nonpos_iff_eq_zero, ← lt_add_one_iff, zero_add, ← lt_opow_iff_log_lt hb ho, opow_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
⊢ log b x ≤ log b y
have inl : ∀ (xy : 0 ≤ y), log b 0 ≤ log b y
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x, xy
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
inl : ∀ (xy : 0 ≤ y), log b 0 ≤ log b y
⊢ log b x ≤ log b y
have inr : ∀ (hx : x ≠ 0), log b x ≤ log b y
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b y : Ordinal.{u_1}
xy : 0 ≤ y
⊢ log b 0 ≤ log b y
have inl : 0 ≤ log b y
Tactic: simp_rw [log_zero_right, zero_le]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
⊢ log b x ≤ log b y
have inr : ∀ (hb : 1 < b), log b x ≤ log b y
Tactic: obtain hb | hb := lt_or_ge 1 b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
inr : ∀ (hb : 1 < b), log b x ≤ log b y
⊢ log b x ≤ log b y
have inr₁ : ∀ (hb : b ≤ 1), log b x ≤ log b y
Tactic: obtain hb | hb := lt_or_ge 1 b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ log b y
have inr : 0 ≤ log b y
Tactic: rw [log_of_left_le_one hb, log_of_left_le_one hb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : b ≤ 1
inr : 0 ≤ log b y
⊢ log b x ≤ log b y
have inr₁ : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 0
Tactic: rw [log_of_left_le_one hb, log_of_left_le_one hb]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
⊢ log b x ≤ x
have inl : log b 0 ≤ 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
inl : log b 0 ≤ 0
⊢ log b x ≤ x
have inr : ∀ (hx : x ≠ 0), log b x ≤ x
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
⊢ log b 0 ≤ 0
have inl : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 0
Tactic: rw [log_zero_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ log b x ≤ x
have inr : ∀ (hb : 1 < b), log b x ≤ x
Tactic: obtain hb | hb := lt_or_ge 1 b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
inr : ∀ (hb : 1 < b), log b x ≤ x
⊢ log b x ≤ x
have inr₁ : ∀ (hb : b ≤ 1), log b x ≤ x
Tactic: obtain hb | hb := lt_or_ge 1 b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ x
have inr : 0 ≤ x
Tactic: simp_rw [log_of_left_le_one hb, zero_le]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
⊢ log b 1 = 0
have inl : ∀ (hb : 1 < b), log b 1 = 0
Tactic: obtain hb | hb := lt_or_ge 1 b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b : Ordinal.{u_1}
inl : ∀ (hb : 1 < b), log b 1 = 0
⊢ log b 1 = 0
have inr : ∀ (hb : b ≤ 1), log b 1 = 0
Tactic: obtain hb | hb := lt_or_ge 1 b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % b ^ log b o < o
have inl : o % HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 o) < o
Tactic: rcases eq_or_ne b 0 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 : o % HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 o) < o
⊢ o % b ^ log b o < o
have inr : ∀ (hb : b ≠ 0), o % b ^ log b o < o
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
⊢ log b (o % b ^ log b o) < log b o
have inl : ∀ (h : o % b ^ log b o = 0), log b (o % b ^ log b o) < log b o
Tactic: rcases eq_or_ne (o % (b ^ log b o)) 0 with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
inl : ∀ (h : o % b ^ log b o = 0), log b (o % b ^ log b o) < log b o
⊢ log b (o % b ^ log b o) < log b o
have inr : ∀ (h : o % b ^ log b o ≠ 0), log b (o % b ^ log b o) < log b o
Tactic: rcases eq_or_ne (o % (b ^ log b o)) 0 with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ log b (o % b ^ log b o) < log b o
have inl : 0 < log b o
Tactic: rw [h, log_zero_right]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b (o % b ^ log b o) < log b o
have inr : o % b ^ log b o < b ^ log b o
Tactic: rw [← lt_opow_iff_log_lt hb h]
-- 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}
⊢ log b x = y ↔ b ^ y ≤ x ∧ x < b ^ (y + 1)
have mp : log b x = y → b ^ y ≤ x ∧ x < b ^ (y + 1)
Tactic: constructor
-- 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}
mp : log b x = y → b ^ y ≤ x ∧ x < b ^ (y + 1)
⊢ log b x = y ↔ b ^ y ≤ x ∧ x < b ^ (y + 1)
have mpr : b ^ y ≤ x ∧ x < b ^ (y + 1) → log b x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ b ^ log b x ≤ x ∧ x < b ^ (log b x + 1)
have left : b ^ log b x ≤ x
Tactic: use opow_log_le_self b hx, lt_opow_succ_log_self hb x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Exponential (goal)
Goal:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
left : b ^ log b x ≤ x
⊢ b ^ log b x ≤ x ∧ x < b ^ (log b x + 1)
have right : x < b ^ (log b x + 1)
Tactic: use opow_log_le_self b hx, lt_opow_succ_log_self hb x