awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
refine_2₁ : 0 < b
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : b ≠ 0
⊢ 1 < a ^ b

Tactic:
rwa [← opow_zero a, opow_lt_opow_iff_right ha, pos_iff_ne_zero]

Premises used: Ordinal.opow_zero, Ordinal.opow_lt_opow_iff_right, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
⊢ a = 1 ∨ b = 0 → a ^ b = 1

Tactic:
simp +contextual [or_imp]

Premises used: or_imp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
refine : ∀ (h : a ^ b = 1), a = 1 ∨ b = 0
⊢ a ^ b = 1 ↔ a = 1 ∨ b = 0

Tactic:
refine ⟨fun h ↦ ?_, by simp +contextual [or_imp]⟩
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a ^ b = 1
contrapose! : ∀ (h : a ≠ 1 ∧ b ≠ 0), a ^ b ≠ 1
⊢ a = 1 ∨ b = 0

Tactic:
contrapose! h
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
inl : ∀ (ha : a ≤ 1), a ^ b ≠ 1
inr : ∀ (ha : 1 < a), a ^ b ≠ 1
⊢ a ^ b ≠ 1

Tactic:
obtain ha | ha := le_or_gt a 1

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : a ≤ 1
⊢ a ^ b ≠ 1

Tactic:
simp_all [le_one_iff]

Premises used: Order.le_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : 1 < a
⊢ a ^ b ≠ 1

Tactic:
simpa using ((opow_lt_opow_iff_right ha).2 h.2.pos).ne'

Premises used: Iff.mpr, Ne.pos, LT.lt.ne', And.right, Ordinal.opow_lt_opow_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
a1 : 1 < a
⊢ IsSuccLimit b → IsSuccLimit (a ^ b)

Tactic:
(isNormal_opow a1).map_isSuccLimit

Premises used: Ordinal.isNormal_opow, Order.IsNormal.map_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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)
inr₁ : ∀ (l' : IsSuccLimit b), IsSuccLimit (a ^ b)
⊢ IsSuccLimit (a ^ b)

Tactic:
rcases zero_or_succ_or_isSuccLimit b with (e | ⟨b, rfl⟩ | l')

Premises used: Ordinal.zero_or_succ_or_isSuccLimit, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
e : b = 0
⊢ IsSuccLimit (a ^ b)

Tactic:
absurd e hb

Premises used: absurd
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
e : b = 0
⊢ IsSuccLimit (a ^ b)

Tactic:
exact absurd e hb

Premises used: absurd
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
l : IsSuccLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
inr : IsSuccLimit (a ^ b * a)
⊢ IsSuccLimit (a ^ succ b)

Tactic:
rw [opow_succ]

Premises used: Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
l : IsSuccLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsSuccLimit (a ^ b * a)

Tactic:
isSuccLimit_mul_right (opow_pos _ l.bot_lt) l

Premises used: Ordinal.isSuccLimit_mul_right, Order.IsSuccLimit.bot_lt, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
l : IsSuccLimit a
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ IsSuccLimit (a ^ b * a)

Tactic:
exact isSuccLimit_mul_right (opow_pos _ l.bot_lt) l

Premises used: Ordinal.isSuccLimit_mul_right, Order.IsSuccLimit.bot_lt, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
l' : IsSuccLimit b
⊢ IsSuccLimit (a ^ b)

Tactic:
isSuccLimit_opow (one_lt_of_isSuccLimit l) l'

Premises used: Ordinal.isSuccLimit_opow, Ordinal.one_lt_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
l' : IsSuccLimit b
⊢ IsSuccLimit (a ^ b)

Tactic:
exact isSuccLimit_opow (one_lt_of_isSuccLimit l) l'

Premises used: Ordinal.isSuccLimit_opow, Ordinal.one_lt_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
h₁ : 0 < a
h₂ : b ≤ c
inl : ∀ (h₁ : a = 1), a ^ b ≤ a ^ c
inr : ∀ (h₁ : 1 < a), a ^ b ≤ a ^ c
⊢ a ^ b ≤ a ^ c

Tactic:
rcases (one_le_iff_pos.2 h₁).eq_or_lt' with h₁ | h₁

Premises used: Iff.mpr, LE.le.eq_or_lt', Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
h₁_1 : 0 < a
h₂ : b ≤ c
h₁ : a = 1
⊢ a ^ b ≤ a ^ c

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
h₁_1 : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c

Tactic:
(opow_le_opow_iff_right h₁).2 h₂

Premises used: Iff.mpr, Ordinal.opow_le_opow_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
h₁_1 : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c

Tactic:
exact (opow_le_opow_iff_right h₁).2 h₂

Premises used: Iff.mpr, Ordinal.opow_le_opow_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
pos : ∀ (ha : a = 0), a ^ c ≤ b ^ c
neg : ∀ (ha : ¬a = 0), a ^ c ≤ b ^ c
⊢ a ^ c ≤ b ^ c

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
pos : c = 0 → a ^ c ≤ b ^ c
neg : ¬c = 0 → a ^ c ≤ b ^ c
⊢ a ^ c ≤ b ^ c

Tactic:
by_cases c = 0
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
h : c = 0
⊢ a ^ c ≤ b ^ c

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
h : ¬c = 0
⊢ a ^ c ≤ b ^ c

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
⊢ HPow.hPow (β := Ordinal.{u_1}) a 0 ≤ HPow.hPow (β := Ordinal.{u_1}) b 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
c : Ordinal.{u_1}
IH : a ^ c ≤ b ^ c
⊢ a ^ (c + 1) ≤ b ^ (c + 1)

Tactic:
simpa using mul_le_mul' IH ab

Premises used: mul_le_mul'
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ o' ≤ b ^ o'
⊢ a ^ c ≤ b ^ c

Tactic:
(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)

Premises used: Ordinal.opow_le_opow_right, Iff.mpr, LT.lt.le, LT.lt.trans_le, LE.le.trans, pos_iff_ne_zero, Ordinal.opow_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ o' ≤ b ^ o'
⊢ a ^ c ≤ b ^ c

Tactic:
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)

Premises used: Ordinal.opow_le_opow_right, Iff.mpr, LT.lt.le, LT.lt.trans_le, LE.le.trans, pos_iff_ne_zero, Ordinal.opow_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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)
neg₂ : ∀ (c : Ordinal.{u_1}) (l : IsSuccLimit c) (IH : ∀ o' < c, a ^ o' ≤ b ^ o'), a ^ c ≤ b ^ c
⊢ 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)

Premises used: Ordinal.zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c d : Ordinal.{u_1}
hac : a ≤ c
hbd : b ≤ d
hc : 0 < c
⊢ a ^ b ≤ c ^ d

Tactic:
(opow_le_opow_left b hac).trans (opow_le_opow_right hc hbd)

Premises used: Ordinal.opow_le_opow_right, LE.le.trans, Ordinal.opow_le_opow_left
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
nth_rw : HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
⊢ a ≤ a ^ b

Tactic:
nth_rw 1 [← opow_one a]

Premises used: Ordinal.opow_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
inl : ∀ (a1 : a ≤ 1), HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
inr : ∀ (a1 : 1 < a), HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b

Tactic:
rcases le_or_gt a 1 with a1 | a1

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
inl₁ : ∀ (a1 : a = 1), HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b

Tactic:
rcases lt_or_eq_of_le a1 with a0 | a1

Premises used: lt_or_eq_of_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ a = 0

Tactic:
rw [lt_one_iff] at a0

Premises used: Order.lt_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
inl : 0 ≤ HPow.hPow (α := Ordinal.{u_1}) 0 b
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b

Tactic:
rw [a0, zero_opow one_ne_zero]

Premises used: one_ne_zero, Ordinal.zero_opow
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ HPow.hPow (α := Ordinal.{u_1}) 0 b

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ HPow.hPow (α := Ordinal.{u_1}) 0 b

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
inl₂ inl₃ : LE.le.{u_1 + 1} (α := Ordinal.{u_1}) 1 1
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b

Tactic:
rw [a1, one_opow, one_opow]

Premises used: Ordinal.one_opow
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : 1 < a
inr : 1 ≤ b
inr₁ inr₂ inr₃ inr₄ : 0 < b
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 ≤ a ^ b

Tactic:
rwa [opow_le_opow_iff_right a1, one_le_iff_pos]

Premises used: Ordinal.opow_le_opow_iff_right, Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
rw : HPow.hPow (β := Ordinal.{u_1}) a 1
| a

Tactic:
rw [← opow_one a]

Premises used: Ordinal.opow_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
conv_lhs : HPow.hPow (β := Ordinal.{u_1}) a 1 < a ^ b
⊢ a < a ^ b

Tactic:
conv_lhs => rw [← opow_one a]

Premises used: Ordinal.opow_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : 1 < a
hb rwa rwa₁ rwa₂ rwa₃ : 1 < b
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 < a ^ b

Tactic:
rwa [opow_lt_opow_iff_right ha]

Premises used: Ordinal.opow_lt_opow_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
a1 : 1 < a
⊢ b ≤ a ^ b

Tactic:
(isNormal_opow a1).strictMono.le_apply

Premises used: StrictMono.le_apply, Ordinal.isNormal_opow, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
ab : a < b
rw : a ^ c * a < b ^ c * b
⊢ a ^ succ c < b ^ succ c

Tactic:
rw [opow_succ, opow_succ]

Premises used: Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c ≤ b ^ c

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c * a < b ^ c * b

Tactic:
exact mul_lt_mul_of_le_of_lt_of_nonneg_of_pos (by gcongr) ab zero_le (opow_pos _ ab.bot_lt)

Premises used: zero_le, mul_lt_mul_of_le_of_lt_of_nonneg_of_pos, LT.lt.bot_lt, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
inr : ∀ (ha : 0 < a), a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
obtain rfl | ha := eq_zero_or_pos a

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
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
⊢ 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

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
⊢ 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:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hc : 0 < c
⊢ b + c ≠ 0

Tactic:
have : b + c ≠ 0 := (hc.trans_le le_add_self).ne'
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hc : 0 < c
this inl : b + c ≠ 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b + c) = HPow.hPow (α := Ordinal.{u_1}) 0 b * HPow.hPow (α := Ordinal.{u_1}) 0 c

Tactic:
rw [zero_opow hc.ne', zero_opow, mul_zero]

Premises used: MulZeroClass.mul_zero, LT.lt.ne', Ordinal.zero_opow
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ b + c ≠ 0

Tactic:
(hc.trans_le le_add_self).ne'

Premises used: LT.lt.ne', LT.lt.trans_le, le_add_self
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ b + c ≠ 0

Tactic:
exact (hc.trans_le le_add_self).ne'

Premises used: LT.lt.ne', LT.lt.trans_le, le_add_self
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
inr₁ : ∀ (ha' : 1 < a), a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
obtain rfl | ha' := (one_le_iff_ne_zero.2 ha.ne').eq_or_lt

Premises used: Iff.mpr, LE.le.eq_or_lt, Order.one_le_iff_ne_zero, LT.lt.ne', rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
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:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
⊢ a ^ (b + 0) = a ^ b * HPow.hPow (β := Ordinal.{u_1}) a 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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)
inr₄ inr₅ : a ^ b * (a ^ c * a) = a ^ b * (a ^ c * a)
⊢ a ^ (b + (c + 1)) = a ^ b * a ^ (c + 1)

Tactic:
rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]

Premises used: add_assoc, mul_assoc, Ordinal.opow_add_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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

Tactic:
eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_

Premises used: eq_of_forall_ge_iff, Order.IsNormal.le_iff_forall_le, Ordinal.isNormal_opow, Iff.trans, Order.IsNormal.comp, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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'
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
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_

Premises used: eq_of_forall_ge_iff, Order.IsNormal.le_iff_forall_le, Ordinal.isNormal_opow, Iff.trans, Order.IsNormal.comp, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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'
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:
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

Premises used: Iff.mpr, Ordinal.isNormal_mul_right, Order.IsNormal.le_iff_forall_le, Ordinal.isNormal_opow, LT.lt.ne', Order.IsNormal.comp, pos_iff_ne_zero, Ordinal.opow_pos, Iff.symm
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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)
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
⊢ 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

Premises used: add_assoc, mul_assoc, Ordinal.zero, Ordinal.opow_add_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
rw : HPow.hPow (β := Ordinal.{u_1}) a 1 * a ^ b = a * a ^ b
rw₁ rw₂ : a * a ^ b = a * a ^ b
⊢ a ^ (1 + b) = a * a ^ b

Tactic:
rw [opow_add, opow_one]

Premises used: Ordinal.opow_one, Ordinal.opow_add
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
h : b ≤ c
rw : a ^ c = a ^ (b + (c - b))
rw₁ rw₂ : a ^ c = a ^ c
⊢ a ^ c = a ^ b * a ^ (c - b)

Tactic:
rw [← opow_add, Ordinal.add_sub_cancel_of_le h]

Premises used: Ordinal.opow_add, Ordinal.add_sub_cancel_of_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
a1 : 1 < a
⊢ a ^ b ∣ a ^ c ↔ b ≤ c

Tactic:
⟨fun h =>
    le_of_not_gt fun hn =>
      not_le_of_gt ((opow_lt_opow_iff_right a1).2 hn) <|
        le_of_dvd (opow_ne_zero _ <| one_le_iff_ne_zero.1 <| a1.le) h,
    opow_dvd_opow _⟩

Premises used: Iff.mpr, Ordinal.opow_dvd_opow, le_of_not_gt, Ordinal.opow_ne_zero, LT.lt.le, Order.one_le_iff_ne_zero, Iff.intro, Iff.mp, Ordinal.opow_lt_opow_iff_right, not_le_of_gt, Ordinal.le_of_dvd
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
inl : a ^ (0 * c) = HPow.hPow (β := Ordinal.{u_1}) a 0 ^ c
inr : ∀ (hb : 0 < b), a ^ (b * c) = (a ^ b) ^ c
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
obtain rfl | hb := eq_zero_or_pos b

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a c : Ordinal.{u_1}
⊢ a ^ (0 * c) = HPow.hPow (β := Ordinal.{u_1}) a 0 ^ c

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
inr₁ : ∀ (ha : a ≠ 0), a ^ (b * c) = (a ^ b) ^ c
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
obtain rfl | ha := eq_or_ne a 0

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

Tactic:
have := hb.ne'
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
neg : ¬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

Tactic:
by_cases c = 0
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
h : c = 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 0 b ^ c

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
h : ¬c = 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b * c) = HPow.hPow (α := Ordinal.{u_1}) 0 b ^ c

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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
inr₁ : ∀ (ha' : 1 < a), a ^ (b * c) = (a ^ b) ^ c
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
obtain rfl | ha' := (one_le_iff_ne_zero.2 ha).eq_or_lt

Premises used: Iff.mpr, LE.le.eq_or_lt, Order.one_le_iff_ne_zero, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b c : Ordinal.{u_1}
hb : 0 < b
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:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
⊢ a ^ (b * 0) = HPow.hPow (β := Ordinal.{u_1}) (a ^ b) 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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)
inr₃ inr₄ : (a ^ b) ^ c * a ^ b = (a ^ b) ^ c * a ^ b
⊢ a ^ (b * (c + 1)) = (a ^ b) ^ (c + 1)

Tactic:
rw [mul_add_one, opow_add, IH, opow_add_one]

Premises used: Ordinal.opow_add, Ordinal.opow_add_one, mul_add_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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

Tactic:
eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_mul_right hb)).le_iff_forall_le l).trans ?_

Premises used: Ordinal.isNormal_mul_right, eq_of_forall_ge_iff, Order.IsNormal.le_iff_forall_le, Ordinal.isNormal_opow, Iff.trans, Order.IsNormal.comp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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'
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
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_mul_right hb)).le_iff_forall_le l).trans ?_

Premises used: Ordinal.isNormal_mul_right, eq_of_forall_ge_iff, Order.IsNormal.le_iff_forall_le, Ordinal.isNormal_opow, Iff.trans, Order.IsNormal.comp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
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'
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:
simpa +contextual [IH] using (opow_le_of_isSuccLimit (opow_ne_zero _ ha) l).symm

Premises used: Ordinal.opow_ne_zero, Iff.symm, Ordinal.opow_le_of_isSuccLimit