awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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)
inr₂ : ∀ (c : Ordinal.{u_1}) (l : IsSuccLimit c) (IH : ∀ o' < c, a ^ (b * o') = (a ^ b) ^ o'), a ^ (b * c) = (a ^ b) ^ c
⊢ 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

Premises used: Ordinal.opow_add, Ordinal.zero, Ordinal.opow_add_one, mul_add_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b v : Ordinal.{u_1}
hb : b ≠ 0
u : Ordinal.{u_1}
hv : v ≠ 0
w : Ordinal.{u_1}
⊢ 0 < b ^ u * v + w

Tactic:
(opow_pos u <| pos_iff_ne_zero.2 hb).trans_le <|
    (le_mul_left _ <| pos_iff_ne_zero.2 hv).trans le_self_add

Premises used: Iff.mpr, LT.lt.trans_le, LE.le.trans, Ordinal.le_mul_left, le_self_add, pos_iff_ne_zero, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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)
hbc : b ^ u * (v + 1) ≤ b ^ u * x
⊢ b ^ u * v + w < b ^ u * x

Tactic:
apply lt_of_lt_of_le (b := b ^ u * (v + 1))

Premises used: lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
hab : b ^ u * v + w < b ^ u * v + b ^ u
hab₁ hab₂ hab₃ hab₄ : w < b ^ u
⊢ b ^ u * v + w < b ^ u * (v + 1)

Tactic:
rwa [mul_add_one, add_lt_add_iff_left]

Premises used: mul_add_one, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
hbc hbc₁ : b ^ u * x ≤ b ^ u * x
⊢ b ^ u * (v + 1) ≤ b ^ u * x

Tactic:
grw [add_one_le_of_lt hv]

Premises used: Order.add_one_le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
apply : b ^ u * b ≤ b ^ x
⊢ b ^ u * v + w < b ^ x

Tactic:
apply (opow_mul_add_lt_opow_mul hw hv).trans_le

Premises used: Ordinal.opow_mul_add_lt_opow_mul, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
rw : b ^ succ u ≤ b ^ x
⊢ b ^ u * b ≤ b ^ x

Tactic:
rw [← opow_succ]

Premises used: Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ succ u ≤ b ^ x

Tactic:
opow_le_opow_right hv.pos (succ_le_of_lt hu)

Premises used: Ordinal.opow_le_opow_right, LT.lt.pos, Order.succ_le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ succ u ≤ b ^ x

Tactic:
exact opow_le_opow_right hv.pos (succ_le_of_lt hu)

Premises used: Ordinal.opow_le_opow_right, LT.lt.pos, Order.succ_le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v x : Ordinal.{u_1}
hv : v < b
hu : u < x
⊢ b ^ u * v < b ^ x

Tactic:
simpa using opow_mul_add_lt_opow hv (opow_pos _ hv.pos) hu

Premises used: LT.lt.pos, Ordinal.opow_mul_add_lt_opow, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
inr : ∀ (h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1), log 1 x = 0
⊢ log b x = 0

Tactic:
obtain rfl | rfl := le_one_iff.1 h

Premises used: Iff.mp, Order.le_one_iff, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x : Ordinal.{u_1}
h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
apply : ¬BddAbove (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ HPow.hPow (α := Ordinal.{u_1}) 0 x) ⁻¹' Iic x)
⊢ log 0 x = 0

Tactic:
apply (csSup_of_not_bddAbove _).trans csSup_empty

Premises used: csSup_empty, csSup_of_not_bddAbove, Eq.trans
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x : Ordinal.{u_1}
h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
by_contra! :
  ∀ (hb : BddAbove (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ HPow.hPow (α := Ordinal.{u_1}) 0 x) ⁻¹' Iic x)),
    False
⊢ ¬BddAbove (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ HPow.hPow (α := Ordinal.{u_1}) 0 x) ⁻¹' Iic x)

Tactic:
by_contra! hb
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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

Tactic:
not_bddAbove_Ici 1 (hb.mono fun a ↦ ?_)

Premises used: not_bddAbove_Ici, OfNat.ofNat, BddAbove.mono
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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)
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
⊢ False

Tactic:
refine not_bddAbove_Ici 1 (hb.mono fun a ↦ ?_)

Premises used: not_bddAbove_Ici, OfNat.ofNat, BddAbove.mono
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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)
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:
simp +contextual [one_le_iff_ne_zero]

Premises used: Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x : Ordinal.{u_1}
h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
inr : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup (if 1 ∈ Iic x then univ else ∅)) 0
⊢ log 1 x = 0

Tactic:
simp_rw [log, one_opow, preimage_const]

Premises used: Set.preimage_const, Ordinal.one_opow, Ordinal.log
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
neg : 1 ∉ Iic x → Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup ∅) 0
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup (if 1 ∈ Iic x then univ else ∅)) 0

Tactic:
split_ifs
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x : Ordinal.{u_1}
h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
h_1 : 1 ∈ Iic x
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup univ) 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x : Ordinal.{u_1}
h : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
h_1 : 1 ∉ Iic x
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup ∅) 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x : Ordinal.{u_1}
⊢ log 0 x = 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x : Ordinal.{u_1}
⊢ log 1 x = 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
inl : log 0 0 = 0
inr : ∀ (hb : b ≠ 0), log b 0 = 0
⊢ log b 0 = 0

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
⊢ log 0 0 = 0

Tactic:
log_zero_left 0

Premises used: Ordinal.log_zero_left, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
⊢ log 0 0 = 0

Tactic:
exact log_zero_left 0

Premises used: Ordinal.log_zero_left, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup ∅) ⊥

Tactic:
csSup_empty

Premises used: csSup_empty
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : b ≠ 0
h : Eq.{u_1 + 2} (α := Set Ordinal.{u_1}) (preimage (β := Ordinal.{u_1}) (fun (x : Ordinal.{u_1}) ↦ b ^ x) (Iic 0)) ∅
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (sSup (preimage (β := Ordinal.{u_1}) (fun (x : Ordinal.{u_1}) ↦ b ^ x) (Iic 0))) 0

Tactic:
convert! csSup_empty

Premises used: csSup_empty
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ Eq.{u_1 + 2} (α := Set Ordinal.{u_1}) (preimage (β := Ordinal.{u_1}) (fun (x : Ordinal.{u_1}) ↦ b ^ x) (Iic 0)) ∅

Tactic:
aesop
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ Membership.mem (γ := Set Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ b ^ x) ⁻¹' Iic x) 0

Tactic:
simpa [one_le_iff_ne_zero]

Premises used: Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
inl : b ^ c ≤ 0 ↔ c ≤ log b 0
inr : ∀ (hx : x ≠ 0), b ^ c ≤ x ↔ c ≤ log b x
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ 0 ↔ c ≤ log b 0

Tactic:
simpa [hc] using hb.ne_bot

Premises used: LT.lt.ne_bot
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
hx : x ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
opow_le_iff_le_log hb hx

Premises used: Ordinal.opow_le_iff_le_log
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
hx : x ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
exact opow_le_iff_le_log hb hx

Premises used: Ordinal.opow_le_iff_le_log
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
inl : ∀ (h : b ^ c ≤ 0), c ≤ log b 0
inr : ∀ (hx : x ≠ 0), c ≤ log b x
⊢ c ≤ log b x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ 0
⊢ b = 0 ∧ c ≠ 0

Tactic:
rw [nonpos_iff_eq_zero, opow_eq_zero] at h

Premises used: nonpos_iff_eq_zero, Ordinal.opow_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hb : 1 < b
h : b = 0 ∧ c ≠ 0
⊢ c ≤ log b 0

Tactic:
(zero_lt_one.asymm <| h.1 ▸ hb).elim

Premises used: False.elim, LT.lt.asymm, zero_lt_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hb : 1 < b
h : b = 0 ∧ c ≠ 0
⊢ c ≤ log b 0

Tactic:
exact (zero_lt_one.asymm <| h.1 ▸ hb).elim

Premises used: False.elim, LT.lt.asymm, zero_lt_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
hx : x ≠ 0
⊢ c ≤ log b x

Tactic:
(opow_le_iff_le_log hb hx).1 h

Premises used: Iff.mp, Ordinal.opow_le_iff_le_log
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
hx : x ≠ 0
⊢ c ≤ log b x

Tactic:
exact (opow_le_iff_le_log hb hx).1 h

Premises used: Iff.mp, Ordinal.opow_le_iff_le_log
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
inl : ∀ (hb : b ≤ 1), b ^ c ≤ x
inr : ∀ (hb : 1 < b), b ^ c ≤ x
⊢ b ^ c ≤ x

Tactic:
obtain hb | hb := le_or_gt b 1

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : b ≤ 1
⊢ c ≤ 0

Tactic:
rw [log_of_left_le_one hb] at h

Premises used: Ordinal.log_of_left_le_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : b ≤ 1
h₁ : c ≤ 0
⊢ b ≤ 1

Tactic:
rw [log_of_left_le_one hb] at h

Premises used: Ordinal.log_of_left_le_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ 0
hb : b ≤ 1
⊢ b ^ c ≤ x

Tactic:
(h.not_gt (pos_iff_ne_zero.2 hc)).elim

Premises used: Iff.mpr, False.elim, LE.le.not_gt, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ 0
hb : b ≤ 1
⊢ b ^ c ≤ x

Tactic:
exact (h.not_gt (pos_iff_ne_zero.2 hc)).elim

Premises used: Iff.mpr, False.elim, LE.le.not_gt, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
inr inr₁ inr₂ inr₃ : c ≤ log b x
⊢ b ^ c ≤ x

Tactic:
rwa [opow_le_iff_le_log' hb hc]

Premises used: Ordinal.opow_le_iff_le_log'
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ x < b ^ c ↔ log b x < c

Tactic:
lt_iff_lt_of_le_iff_le (opow_le_iff_le_log hb hx)

Premises used: Ordinal.opow_le_iff_le_log, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ x < b ^ c ↔ log b x < c

Tactic:
lt_iff_lt_of_le_iff_le (opow_le_iff_le_log' hb hc)

Premises used: lt_iff_lt_of_le_iff_le, Ordinal.opow_le_iff_le_log'
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hb : 1 < b
⊢ log b x < c → x < b ^ c

Tactic:
lt_imp_lt_of_le_imp_le <| le_log_of_opow_le hb

Premises used: Ordinal.le_log_of_opow_le, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x c : Ordinal.{u_1}
hc : c ≠ 0
⊢ x < b ^ c → log b x < c

Tactic:
lt_imp_lt_of_le_imp_le <| opow_le_of_le_log hc

Premises used: lt_imp_lt_of_le_imp_le, Ordinal.opow_le_of_le_log
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
inl : 0 < b ^ succ (log b 0)
inr : ∀ (hx : x ≠ 0), x < b ^ succ (log b x)
⊢ x < b ^ succ (log b x)

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)

Tactic:
simpa using hb.pos

Premises used: LT.lt.pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
inr : log b x < succ (log b x)
inr₁ inr₂ : log b x ≤ log b x
⊢ x < b ^ succ (log b x)

Tactic:
rw [lt_opow_iff_log_lt hb hx, lt_succ_iff]

Premises used: Order.lt_succ_iff, Ordinal.lt_opow_iff_log_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
inl : ∀ (hb : b ≤ 1), b ^ log b x ≤ x
inr : ∀ (hb : 1 < b), b ^ log b x ≤ x
⊢ b ^ log b x ≤ x

Tactic:
obtain hb | hb := le_or_gt b 1

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ 1 ≤ x

Tactic:
rw [← one_le_iff_ne_zero] at hx

Premises used: Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
hx₁ : 1 ≤ x
⊢ b ≤ 1

Tactic:
rw [← one_le_iff_ne_zero] at hx

Premises used: Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
inl₁ : ∀ (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1), HPow.hPow (α := Ordinal.{u_1}) 1 (log 1 x) ≤ x
⊢ b ^ log b x ≤ x

Tactic:
obtain rfl | rfl := le_one_iff.1 hb

Premises used: Iff.mp, Order.le_one_iff, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x : Ordinal.{u_1}
hx : 1 ≤ x
hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 x) ≤ x

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x : Ordinal.{u_1}
hx : 1 ≤ x
hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 (log 1 x) ≤ x

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
inr inr₁ : log b x ≤ log b x
⊢ b ^ log b x ≤ x

Tactic:
rw [opow_le_iff_le_log hb hx]

Premises used: Ordinal.opow_le_iff_le_log
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
rwa₂ : HPow.hPow (β := Ordinal.{u_1}) b 1 ≤ o
rwa₃ rwa₄ rwa₅ rwa₆ : b ≤ o
⊢ 0 < log b o

Tactic:
rwa [← add_one_le_iff, zero_add, ← opow_le_iff_le_log hb ho, opow_one]

Premises used: Ordinal.opow_one, zero_add, Order.add_one_le_iff, Ordinal.opow_le_iff_le_log
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hbo : o < b
inl : ∀ (hbo : 0 < b), log b 0 = 0
inr : ∀ (ho : o ≠ 0), log b o = 0
⊢ log b o = 0

Tactic:
rcases eq_or_ne o 0 with (rfl | ho)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hbo : 0 < b
⊢ log b 0 = 0

Tactic:
log_zero_right b

Premises used: Ordinal.log_zero_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hbo : 0 < b
⊢ log b 0 = 0

Tactic:
exact log_zero_right b

Premises used: Ordinal.log_zero_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
inr : ∀ (hb : b ≤ 1), log b o = 0
inr₁ : ∀ (hb : 1 < b), log b o = 0
⊢ log b o = 0

Tactic:
rcases le_or_gt b 1 with hb | hb

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
inr₁ : ∀ (hbo : o < 1) (hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1), log 1 o = 0
⊢ log b o = 0

Tactic:
rcases le_one_iff.1 hb with (rfl | rfl)

Premises used: Iff.mp, Order.le_one_iff, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 0
hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
⊢ log 0 o = 0

Tactic:
log_zero_left o

Premises used: Ordinal.log_zero_left
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 0
hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
⊢ log 0 o = 0

Tactic:
exact log_zero_left o

Premises used: Ordinal.log_zero_left
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 1
hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
⊢ log 1 o = 0

Tactic:
log_one_left o

Premises used: Ordinal.log_one_left
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 1
hb : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
⊢ log 1 o = 0

Tactic:
exact log_one_left o

Premises used: Ordinal.log_one_left
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
inr₃ : o < HPow.hPow (β := Ordinal.{u_1}) b 1
inr₄ inr₅ inr₆ inr₇ : o < b
⊢ 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]

Premises used: Ordinal.opow_one, zero_add, Order.lt_add_one_iff, nonpos_iff_eq_zero, Ordinal.lt_opow_iff_log_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
inl : ∀ (xy : 0 ≤ y), log b 0 ≤ log b y
inr : ∀ (hx : x ≠ 0), log b x ≤ log b y
⊢ log b x ≤ log b y

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b y : Ordinal.{u_1}
xy : 0 ≤ y
inl : 0 ≤ log b y
⊢ log b 0 ≤ log b y

Tactic:
simp_rw [log_zero_right, zero_le]

Premises used: zero_le, Ordinal.log_zero_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
inr : ∀ (hb : 1 < b), log b x ≤ log b y
inr₁ : ∀ (hb : b ≤ 1), log b x ≤ log b y
⊢ log b x ≤ log b y

Tactic:
obtain hb | hb := lt_or_ge 1 b

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ log b y

Tactic:
(opow_le_iff_le_log hb (hx.bot_lt.trans_le xy).ne').1 <|
        (opow_log_le_self _ hx).trans xy

Premises used: Ordinal.opow_log_le_self, LT.lt.ne', LT.lt.trans_le, Iff.mp, LE.le.trans, Ordinal.opow_le_iff_le_log, Ne.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ log b y

Tactic:
exact (opow_le_iff_le_log hb (hx.bot_lt.trans_le xy).ne').1 <|
        (opow_log_le_self _ hx).trans xy

Premises used: Ordinal.opow_log_le_self, LT.lt.ne', LT.lt.trans_le, Iff.mp, LE.le.trans, Ordinal.opow_le_iff_le_log, Ne.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : b ≤ 1
inr : 0 ≤ log b y
inr₁ inr₂ : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 0
⊢ log b x ≤ log b y

Tactic:
rw [log_of_left_le_one hb, log_of_left_le_one hb]

Premises used: Ordinal.log_of_left_le_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
inl : log b 0 ≤ 0
inr : ∀ (hx : x ≠ 0), log b x ≤ x
⊢ log b x ≤ x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
inl inl₁ : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 0 0
⊢ log b 0 ≤ 0

Tactic:
rw [log_zero_right]

Premises used: Ordinal.log_zero_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
inr : ∀ (hb : 1 < b), log b x ≤ x
inr₁ : ∀ (hb : b ≤ 1), log b x ≤ x
⊢ log b x ≤ x

Tactic:
obtain hb | hb := lt_or_ge 1 b

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ x

Tactic:
(right_le_opow _ hb).trans (opow_log_le_self b hx)

Premises used: Ordinal.opow_log_le_self, Ordinal.right_le_opow, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ x

Tactic:
exact (right_le_opow _ hb).trans (opow_log_le_self b hx)

Premises used: Ordinal.opow_log_le_self, Ordinal.right_le_opow, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
inr : 0 ≤ x
⊢ log b x ≤ x

Tactic:
simp_rw [log_of_left_le_one hb, zero_le]

Premises used: zero_le, Ordinal.log_of_left_le_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
inl : ∀ (hb : 1 < b), log b 1 = 0
inr : ∀ (hb : b ≤ 1), log b 1 = 0
⊢ log b 1 = 0

Tactic:
obtain hb | hb := lt_or_ge 1 b

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : 1 < b
⊢ log b 1 = 0

Tactic:
log_eq_zero hb

Premises used: Ordinal.log_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : 1 < b
⊢ log b 1 = 0

Tactic:
exact log_eq_zero hb

Premises used: Ordinal.log_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 1 = 0

Tactic:
log_of_left_le_one hb 1

Premises used: Ordinal.log_of_left_le_one, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 1 = 0

Tactic:
exact log_of_left_le_one hb 1

Premises used: Ordinal.log_of_left_le_one, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
inl : o % HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 o) < o
inr : ∀ (hb : b ≠ 0), o % b ^ log b o < o
⊢ o % b ^ log b o < o

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 o) < o

Tactic:
simpa using pos_iff_ne_zero.2 ho

Premises used: Iff.mpr, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o

Tactic:
(mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)

Premises used: Ordinal.opow_log_le_self, Ordinal.opow_ne_zero, Ordinal.mod_lt, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o

Tactic:
exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)

Premises used: Ordinal.opow_log_le_self, Ordinal.opow_ne_zero, Ordinal.mod_lt, LT.lt.trans_le