awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
this : Nonempty.{u + 2} (↑(Iio o) : Type (u + 1))
c : (↑(Iio o) : Type (u + 1))
⊢ (fun (b : (↑(Iio o) : Type (u + 1))) ↦ enumOrd s (↑b : Ordinal.{u})) c ∈ s

Tactic:
exact enumOrd_mem hs c

Premises used: Ordinal.enumOrd_mem, Subtype.val
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
b : Ordinal.{u}
hb : b < o
⊢ enumOrd s (succ b) ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})

Tactic:
Ordinal.le_iSup _ (⟨_, ho.succ_lt hb⟩ : Iio o)

Premises used: Order.succ, Order.IsSuccLimit.succ_lt, Subtype.mk, Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
b : Ordinal.{u}
hb : b < o
⊢ enumOrd s (succ b) ≤ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u})

Tactic:
exact Ordinal.le_iSup _ (⟨_, ho.succ_lt hb⟩ : Iio o)

Premises used: Order.IsSuccLimit.succ_lt, Subtype.mk, Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u}) ≤ a

Tactic:
Ordinal.iSup_le fun x ↦ ha _ x.2

Premises used: Ordinal.iSup_le, Subtype.val, Subtype.property
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ ⨆ (b : (↑(Iio o) : Type (u + 1))), enumOrd s (↑b : Ordinal.{u}) ≤ a

Tactic:
exact Ordinal.iSup_le fun x ↦ ha _ x.2

Premises used: Ordinal.iSup_le
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
rw : enumOrd (range id) = id
⊢ enumOrd univ = id

Tactic:
rw [← range_id]

Premises used: Set.range_id
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
⊢ enumOrd (range id) = id

Tactic:
enumOrd_range strictMono_id

Premises used: Ordinal.enumOrd_range, strictMono_id
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
⊢ enumOrd (range id) = id

Tactic:
exact enumOrd_range strictMono_id

Premises used: Ordinal.enumOrd_range, strictMono_id
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
rw : sInf (s ∩ {b : Ordinal.{u} | ∀ c < 0, enumOrd s c < b}) = sInf s
⊢ enumOrd s 0 = sInf s

Tactic:
rw [enumOrd]

Premises used: Ordinal.enumOrd
-- Module: Mathlib.SetTheory.Ordinal.Enum
Goal:
s : Set Ordinal.{u}
⊢ sInf (s ∩ {b : Ordinal.{u} | ∀ c < 0, enumOrd s c < b}) = sInf s

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ b =
    limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) b 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
      fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
      ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯

Tactic:
if_neg h

Premises used: if_neg
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 a = 1 - a

Tactic:
if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
rw : 1 - a ≤ 1
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 a ≤ 1

Tactic:
rw [zero_opow']

Premises used: Ordinal.zero_opow'
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
⊢ 1 - a ≤ 1

Tactic:
sub_le_self 1 a

Premises used: Ordinal.sub_le_self, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
⊢ 1 - a ≤ 1

Tactic:
exact sub_le_self 1 a

Premises used: Ordinal.sub_le_self, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
a0 : a ≠ 0
rwa : 1 - a = 0
rwa₁ : 1 ≤ a
rwa₂ rwa₃ rwa₄ rwa₅ : a ≠ 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 a = 0

Tactic:
rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero]

Premises used: Ordinal.sub_eq_zero_iff_le, Ordinal.zero_opow', Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
inl : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0 = 1
inr : ∀ (h : a ≠ 0), HPow.hPow (β := Ordinal.{u_1}) a 0 = 1
⊢ HPow.hPow (β := Ordinal.{u_1}) a 0 = 1

Tactic:
obtain rfl | h := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
inl : HSub.hSub (α := Ordinal.{u_1}) 1 0 = 1
inl₁ inl₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 1 1
⊢ HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0 = 1

Tactic:
rw [zero_opow', Ordinal.sub_zero]

Premises used: Ordinal.sub_zero, Ordinal.zero_opow'
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
h : a ≠ 0
inr :
  Eq.{u_1 + 2} (α := Ordinal.{u_1})
    (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) 0 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
        fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
        ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯ :
      Ordinal.{u_1})
    1
inr₁ inr₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 1 1
⊢ HPow.hPow (β := Ordinal.{u_1}) a 0 = 1

Tactic:
rw [opow_of_ne_zero h, limitRecOn_zero]

Premises used: _private.0.Ordinal.opow_of_ne_zero, Ordinal.limitRecOn_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
inl : HPow.hPow (α := Ordinal.{u_1}) 0 (b + 1) = HPow.hPow (α := Ordinal.{u_1}) 0 b * 0
inr : ∀ (h : a ≠ 0), a ^ (b + 1) = a ^ b * a
⊢ a ^ (b + 1) = a ^ b * a

Tactic:
obtain rfl | h := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
inl : 0 = HPow.hPow (α := Ordinal.{u_1}) 0 b * 0
inl₁ inl₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 (b + 1) = HPow.hPow (α := Ordinal.{u_1}) 0 b * 0

Tactic:
rw [zero_opow (add_pos_of_right zero_lt_one b).ne', mul_zero]

Premises used: MulZeroClass.mul_zero, add_pos_of_right, LT.lt.ne', zero_lt_one, Ordinal.zero_opow
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a ≠ 0
inr :
  (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (b + 1) 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
      fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
      ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯) =
    HMul.hMul (α := Ordinal.{u_1})
      (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) b 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
          fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
          ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯ :
        Ordinal.{u_1})
      a
⊢ a ^ (b + 1) = a ^ b * a

Tactic:
rw [opow_of_ne_zero h, opow_of_ne_zero h]

Premises used: _private.0.Ordinal.opow_of_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (b + 1) 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
      fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
      ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯) =
    HMul.hMul (α := Ordinal.{u_1})
      (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) b 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
          fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
          ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯ :
        Ordinal.{u_1})
      a

Tactic:
limitRecOn_add_one ..

Premises used: Ordinal.limitRecOn_add_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (b + 1) 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
      fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
      ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯) =
    HMul.hMul (α := Ordinal.{u_1})
      (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) b 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
          fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
          ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯ :
        Ordinal.{u_1})
      a

Tactic:
exact limitRecOn_add_one ..

Premises used: Ordinal.limitRecOn_add_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
⊢ a ^ succ b = a ^ b * a

Tactic:
opow_add_one a b

Premises used: Order.succ, Ordinal.opow_add_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccLimit b
simp_rw :
  Eq (α := Ordinal.{u_1})
    (limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) b 1 (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
        fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
        ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯ :
      Ordinal.{u_1})
    (⨆ (x : (↑(Iio b) : Type (u_1 + 1))),
      limitRecOn (motive := fun (x : Ordinal.{u_1}) ↦ Ordinal.{u_1}) (↑x : Ordinal.{u_1}) 1
        (fun (x x_1 : Ordinal.{u_1}) ↦ x_1 * a)
        fun (o : Ordinal.{u_1}) (x : IsSuccLimit o) (f : (o' : Ordinal.{u_1}) → o' < o → Ordinal.{u_1}) ↦
        ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), f (↑x : Ordinal.{u_1}) ⋯)
⊢ a ^ b = ⨆ (x : (↑(Iio b) : Type (u_1 + 1))), a ^ (↑x : Ordinal.{u_1})

Tactic:
simp_rw [opow_of_ne_zero ha, limitRecOn_limit _ _ _ _ hb]

Premises used: _private.0.Ordinal.opow_of_ne_zero, Ordinal.limitRecOn_limit
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
rw :
  (∀ (a_1 : Ordinal.{u_1}) (b_1 : a_1 ∈ Iio b),
      a ^ (↑(Subtype.mk (p := fun (a : Ordinal.{u_1}) ↦ a ∈ Iio b) a_1 b_1) : Ordinal.{u_1}) ≤ c) ↔
    ∀ b' < b, a ^ b' ≤ c
⊢ a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c

Tactic:
rw [opow_limit a0 h, Ordinal.iSup_le_iff, Subtype.forall]

Premises used: Subtype.forall, Ordinal.opow_limit, Ordinal.iSup_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ (∀ (a_1 : Ordinal.{u_1}) (b_1 : a_1 ∈ Iio b),
      a ^ (↑(Subtype.mk (p := fun (a : Ordinal.{u_1}) ↦ a ∈ Iio b) a_1 b_1) : Ordinal.{u_1}) ≤ c) ↔
    ∀ b' < b, a ^ b' ≤ c

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : IsSuccLimit c
⊢ a < b ^ c ↔ ∃ c' < c, a < b ^ c'

Tactic:
simpa using (opow_le_of_isSuccLimit b0 h).not

Premises used: Iff.not, Ordinal.opow_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
⊢ HPow.hPow (β := Ordinal.{u_1}) a 1 = a

Tactic:
simpa using opow_add_one a 0

Premises used: Ordinal.opow_add_one, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
⊢ HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 1 0 = 1

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
IH : HPow.hPow (α := Ordinal.{u_1}) 1 o = 1
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 (o + 1) = 1

Tactic:
simp [IH, mul_one]

Premises used: mul_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, HPow.hPow (α := Ordinal.{u_1}) 1 o' = 1
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 b = 1

Tactic:
eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, HPow.hPow (α := Ordinal.{u_1}) 1 o' = 1
limit : ∀ (c : Ordinal.{u_1}), HPow.hPow (α := Ordinal.{u_1}) 1 b ≤ c ↔ 1 ≤ c
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 b = 1

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, HPow.hPow (α := Ordinal.{u_1}) 1 o' = 1
c : Ordinal.{u_1}
limit : (∀ b' < b, HPow.hPow (α := Ordinal.{u_1}) 1 b' ≤ c) ↔ 1 ≤ c
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 b ≤ c ↔ 1 ≤ c

Tactic:
rw [opow_le_of_isSuccLimit one_ne_zero l]

Premises used: one_ne_zero, Ordinal.opow_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, HPow.hPow (α := Ordinal.{u_1}) 1 o' = 1
c : Ordinal.{u_1}
H : ∀ b' < b, HPow.hPow (α := Ordinal.{u_1}) 1 b' ≤ c
⊢ 1 ≤ c

Tactic:
simpa only [opow_zero] using H 0 l.bot_lt

Premises used: Ordinal.opow_zero, Order.IsSuccLimit.bot_lt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, HPow.hPow (α := Ordinal.{u_1}) 1 o' = 1
c : Ordinal.{u_1}
H : 1 ≤ c
b' : Ordinal.{u_1}
h : b' < b
rwa rwa₁ rwa₂ rwa₃ : 1 ≤ c
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 b' ≤ c

Tactic:
rwa [IH _ h]
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, HPow.hPow (α := Ordinal.{u_1}) 1 o' = 1
c : Ordinal.{u_1}
⊢ (∀ b' < b, HPow.hPow (α := Ordinal.{u_1}) 1 b' ≤ c) ↔ 1 ≤ c

Tactic:
exact ⟨fun H => by simpa only [opow_zero] using H 0 l.bot_lt, fun H b' h => by rwa [IH _ h]⟩
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
zero : HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 1 0 = 1
add_one :
  ∀ (o : Ordinal.{u_1}) (IH : HPow.hPow (α := Ordinal.{u_1}) 1 o = 1), HPow.hPow (α := Ordinal.{u_1}) 1 (o + 1) = 1
limit :
  ∀ (b : Ordinal.{u_1}) (l : IsSuccLimit b) (IH : ∀ o' < b, HPow.hPow (α := Ordinal.{u_1}) 1 o' = 1),
    HPow.hPow (α := Ordinal.{u_1}) 1 b = 1
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 a = 1

Tactic:
induction a using limitRecOn with
  | zero => simp
  | add_one _ IH => simp [IH, mul_one]
  | limit b l IH =>
    refine eq_of_forall_ge_iff fun c => ?_
    rw [opow_le_of_isSuccLimit one_ne_zero l]
    exact ⟨fun H => by simpa only [opow_zero] using H 0 l.bot_lt, fun H b' h => by rwa [IH _ h]⟩

Premises used: eq_of_forall_ge_iff, Ordinal.zero, mul_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < HPow.hPow (β := Ordinal.{u_1}) a 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < HPow.hPow (β := Ordinal.{u_1}) a 0

Tactic:
have h0 : 0 < a ^ (0 : Ordinal) := by simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
⊢ 0 < HPow.hPow (β := Ordinal.{u_1}) a 0

Tactic:
h0
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
⊢ 0 < HPow.hPow (β := Ordinal.{u_1}) a 0

Tactic:
exact h0
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ (b + 1)

Tactic:
simpa using mul_pos IH a0

Premises used: mul_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
b : Ordinal.{u_1}
l : IsSuccLimit b
h : ∀ o' < b, 0 < a ^ o'
⊢ 0 < a ^ b

Tactic:
(lt_opow_of_isSuccLimit (pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Iff.mp, Ordinal.lt_opow_of_isSuccLimit, OfNat.ofNat, Order.IsSuccLimit.pos, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
b : Ordinal.{u_1}
l : IsSuccLimit b
h : ∀ o' < b, 0 < a ^ o'
⊢ 0 < a ^ b

Tactic:
exact (lt_opow_of_isSuccLimit (pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Iff.mp, Ordinal.lt_opow_of_isSuccLimit, OfNat.ofNat, Order.IsSuccLimit.pos, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
zero : 0 < HPow.hPow (β := Ordinal.{u_1}) a 0
add_one : ∀ (b : Ordinal.{u_1}) (IH : 0 < a ^ b), 0 < a ^ (b + 1)
limit : ∀ (b : Ordinal.{u_1}) (l : IsSuccLimit b), (∀ o' < b, 0 < a ^ o') → 0 < a ^ b
⊢ 0 < a ^ b

Tactic:
induction b using limitRecOn with
  | zero => exact h0
  | add_one b IH => simpa using mul_pos IH a0
  | limit b l _ => exact (lt_opow_of_isSuccLimit (pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩

Premises used: Ordinal.zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
a0 : a ≠ 0
⊢ a ^ b ≠ 0

Tactic:
pos_iff_ne_zero.1 <| opow_pos b <| pos_iff_ne_zero.2 a0

Premises used: Iff.mpr, Iff.mp, pos_iff_ne_zero, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
pos : a = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
neg : ¬a = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
by_cases a = 0
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a = 0
pos : b = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
neg : ¬b = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
by_cases b = 0
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : ¬a = 0
pos : b = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
neg : ¬b = 0 → (a ^ b = 0 ↔ a = 0 ∧ b ≠ 0)
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
by_cases b = 0
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a = 0
h_1 : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
simp_all [opow_ne_zero]

Premises used: Ordinal.opow_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a = 0
h_1 : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
simp_all [opow_ne_zero]

Premises used: Ordinal.opow_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : ¬a = 0
h_1 : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
simp_all [opow_ne_zero]

Premises used: Ordinal.opow_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : ¬a = 0
h_1 : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
simp_all [opow_ne_zero]

Premises used: Ordinal.opow_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
zero : HPow.hPow (β := Ordinal.{u_1}) a 0 = HPow.hPow (β := ℕ) a 0
zero₁ : 1 = HPow.hPow (β := ℕ) a 0
zero₂ zero₃ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 1 1
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑0 : Ordinal.{u_1}) = HPow.hPow (β := ℕ) a 0

Tactic:
rw [Nat.cast_zero, opow_zero, pow_zero]

Premises used: pow_zero, Ordinal.opow_zero, Nat.cast_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
n : ℕ
IH : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) = a ^ n
succ : a ^ HAdd.hAdd (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) 1 = a ^ (n + 1)
succ₁ : HPow.hPow (β := Ordinal.{u_1}) a (Order.succ (↑n : Ordinal.{u_1})) = a ^ (n + 1)
succ₂ : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) * a = a ^ (n + 1)
succ₃ : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) * a = a ^ n * a
succ₄ succ₅ : a ^ n * a = a ^ n * a
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑(n + 1) : Ordinal.{u_1}) = a ^ (n + 1)

Tactic:
rw [Nat.cast_succ, ← succ_eq_add_one, opow_succ, pow_succ, IH]

Premises used: Nat.cast_succ, Order.succ_eq_add_one, pow_succ, Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
n : ℕ
zero : HPow.hPow (β := Ordinal.{u_1}) a (↑0 : Ordinal.{u_1}) = HPow.hPow (β := ℕ) a 0
succ :
  ∀ (n : ℕ) (IH : HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) = a ^ n),
    HPow.hPow (β := Ordinal.{u_1}) a (↑(n + 1) : Ordinal.{u_1}) = a ^ (n + 1)
⊢ HPow.hPow (β := Ordinal.{u_1}) a (↑n : Ordinal.{u_1}) = a ^ n

Tactic:
induction n with
  | zero => rw [Nat.cast_zero, opow_zero, pow_zero]
  | succ n IH => rw [Nat.cast_succ, ← succ_eq_add_one, opow_succ, pow_succ, IH]

Premises used: Nat.cast_succ, Order.succ, Order.succ_eq_add_one, pow_succ, pow_zero, Ordinal.opow_zero, Ordinal.zero, Nat.cast_zero, Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
h : 1 < a
⊢ 0 < a

Tactic:
have ha : 0 < a := zero_lt_one.trans h
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ IsNormal (β := Ordinal.{u_1}) fun (x : Ordinal.{u_1}) ↦ a ^ x

Tactic:
IsNormal.of_succ_lt ?_ fun hl ↦ ?_

Premises used: Order.IsNormal.of_succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
refine_1 : ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ succ a_1
refine_2 :
  ∀ {a_1 : Ordinal.{u_1}} (hl : IsSuccLimit a_1), IsLUB ((fun (x : Ordinal.{u_1}) ↦ a ^ x) '' Iio a_1) (a ^ a_1)
⊢ IsNormal (β := Ordinal.{u_1}) fun (x : Ordinal.{u_1}) ↦ a ^ x

Tactic:
refine IsNormal.of_succ_lt ?_ fun hl ↦ ?_

Premises used: Order.IsNormal.of_succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ succ a_1

Tactic:
simpa only [mul_one, opow_succ] using fun b ↦ mul_lt_mul_of_pos_left h (opow_pos b ha)

Premises used: mul_lt_mul_of_pos_left, Ordinal.opow_succ, mul_one, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
a_1 : Ordinal.{u_1}
hl : IsSuccLimit a_1
⊢ IsLUB ((fun (x : Ordinal.{u_1}) ↦ a ^ x) '' Iio a_1) (a ^ a_1)

Tactic:
simp [IsLUB, IsLeast, upperBounds, lowerBounds, ← opow_le_of_isSuccLimit ha.ne' hl]

Premises used: lowerBounds, upperBounds, IsLeast, LT.lt.ne', IsLUB, Ordinal.opow_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
a1 : 1 < a
⊢ a ^ b < a ^ c ↔ b < c

Tactic:
(isNormal_opow a1).strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Ordinal.isNormal_opow, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
a1 : 1 < a
⊢ a ^ b ≤ a ^ c ↔ b ≤ c

Tactic:
(isNormal_opow a1).strictMono.le_iff_le

Premises used: Ordinal.isNormal_opow, Order.IsNormal.strictMono, StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b c : Ordinal.{u_1}
a1 : 1 < a
⊢ a ^ b = a ^ c ↔ b = c

Tactic:
(isNormal_opow a1).strictMono.injective.eq_iff

Premises used: Function.Injective.eq_iff, Ordinal.isNormal_opow, StrictMono.injective, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
⊢ 1 < a ^ b ↔ 1 < a ∧ b ≠ 0

Tactic:
⟨?_, fun ⟨ha, hb⟩ ↦ ?_⟩

Premises used: _private.0.Ordinal.one_lt_opow.match_1, HPow.hPow, LT.lt, Iff.intro, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
refine_1 : 1 < a ^ b → 1 < a ∧ b ≠ 0
refine_2 : 1 < a ∧ b ≠ 0 → ∀ (ha : 1 < a) (hb : b ≠ 0), 1 < a ^ b
⊢ 1 < a ^ b ↔ 1 < a ∧ b ≠ 0

Tactic:
refine ⟨?_, fun ⟨ha, hb⟩ ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
refine_1 : a ≤ 1 ∨ b = 0 → a ^ b ≤ 1
⊢ 1 < a ^ b → 1 < a ∧ b ≠ 0

Tactic:
contrapose! +distrib
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
refine_1 : (a = 0 ∨ a = 1) ∨ b = 0 → a ^ b ≤ 1
⊢ a ≤ 1 ∨ b = 0 → a ^ b ≤ 1

Tactic:
rw [le_one_iff]

Premises used: Order.le_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 b ≤ 1

Tactic:
zero_opow_le b

Premises used: Ordinal.zero_opow_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
⊢ HPow.hPow (α := Ordinal.{u_1}) 0 b ≤ 1

Tactic:
exact zero_opow_le b

Premises used: Ordinal.zero_opow_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
⊢ HPow.hPow (α := Ordinal.{u_1}) 1 b ≤ 1

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a : Ordinal.{u_1}
⊢ HPow.hPow (β := Ordinal.{u_1}) a 0 ≤ 1

Tactic:
simp