awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b c : Ordinal.{u}
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
rw : a + (b + (c - b)) = b + (c - b)
rw₁ : a + b + (c - b) = b + (c - b)
rw₂ : b + (c - b) = b + (c - b)
rw₃ rw₄ : c = c
⊢ a + c = c

Tactic:
rw [← Ordinal.add_sub_cancel_of_le hbc, ← add_assoc, hb.add_eq_right hab,
    Ordinal.add_sub_cancel_of_le hbc]

Premises used: add_assoc, Ordinal.IsPrincipal.add_eq_right, Ordinal.add_sub_cancel_of_le
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
ha : ¬IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a
⊢ ∃ a_1 < a, ∃ b < a, a ≤ a_1 + b

Tactic:
rw [not_isPrincipal_iff] at ha

Premises used: Ordinal.not_isPrincipal_iff
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
ha : ∃ a_1 < a, ∃ b < a, a ≤ a_1 + b
rcases : ∀ (b : Ordinal.{u}) (hb : b < a) (c : Ordinal.{u}) (hc : c < a) (H : a ≤ b + c), ∃ b < a, ∃ c < a, b + c = a
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
rcases ha with ⟨b, hb, c, hc, H⟩
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
⟨b, hb, _, lt_of_le_of_ne (sub_le_self a b) fun hab => ?_, Ordinal.add_sub_cancel_of_le hb.le⟩

Premises used: LT.lt.le, Ordinal.sub_le_self, And.intro, Exists.intro, Ordinal.add_sub_cancel_of_le, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
lt_of_le_of_ne : ∀ (hab : a - b = a), False
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
refine
    ⟨b, hb, _, lt_of_le_of_ne (sub_le_self a b) fun hab => ?_, Ordinal.add_sub_cancel_of_le hb.le⟩
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
hab : a - b = a
⊢ a ≤ c

Tactic:
rw [← sub_le, hab] at H

Premises used: Ordinal.sub_le
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
hab : a - b = a
H₁ : a ≤ c
⊢ a - b = a

Tactic:
rw [← sub_le, hab] at H

Premises used: Ordinal.sub_le
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False

Tactic:
H.not_gt hc

Premises used: LE.le.not_gt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ c
hab : a - b = a
⊢ False

Tactic:
exact H.not_gt hc

Premises used: LE.le.not_gt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
by_contra : ∀ (ha : ¬IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a), False
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a

Tactic:
by_contra ha
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
ha : ¬IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a
rcases :
  ∀ (b c : Ordinal.{u}) (H : ∀ b_1 < b + c, ∀ c_1 < b + c, b_1 + c_1 ≠ b + c)
    (ha : ¬IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (b + c)) (hb : b < b + c) (hc : c < b + c), False
⊢ False

Tactic:
rcases exists_lt_add_of_not_isPrincipal_add ha with ⟨b, hb, c, hc, rfl⟩

Premises used: Ordinal.exists_lt_add_of_not_isPrincipal_add, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b c : Ordinal.{u}
H : ∀ b_1 < b + c, ∀ c_1 < b + c, b_1 + c_1 ≠ b + c
ha : ¬IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (b + c)
hb : b < b + c
hc : c < b + c
⊢ False

Tactic:
(H b hb c hc).irrefl

Premises used: Ne.irrefl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b c : Ordinal.{u}
H : ∀ b_1 < b + c, ∀ c_1 < b + c, b_1 + c_1 ≠ b + c
ha : ¬IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (b + c)
hb : b < b + c
hc : c < b + c
⊢ False

Tactic:
exact (H b hb c hc).irrefl

Premises used: Ne.irrefl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) ω

Tactic:
isPrincipal_add_iff_add_left_eq_self.2 fun _ => add_omega0

Premises used: Iff.mpr, Ordinal.isPrincipal_add_iff_add_left_eq_self, Ordinal.add_omega0
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
⊢ a < ω → ω ≤ b → a + b = b

Tactic:
isPrincipal_add_omega0.add_eq_right_of_le

Premises used: Ordinal.IsPrincipal.add_eq_right_of_le, Ordinal.isPrincipal_add_omega0
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u_1}
inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (β := Ordinal.{u_1}) ω 0)
inr : ∀ (ha' : o ≠ 0), IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ o)
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ o)

Tactic:
obtain rfl | ha' := eq_or_ne o 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 1
inl₁ : HAdd.hAdd (α := Ordinal.{u_1}) 0 0 = 0
inl₂ inl₃ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (β := Ordinal.{u_1}) ω 0)

Tactic:
rw [opow_zero, isPrincipal_one_iff, add_zero]

Premises used: Ordinal.isPrincipal_one_iff, Ordinal.opow_zero, add_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u_1}
ha' : o ≠ 0
inr : ∀ b < ω ^ o, b + b < ω ^ o
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ o)

Tactic:
rw [isPrincipal_add_iff_add_self_lt]

Premises used: Ordinal.isPrincipal_add_iff_add_self_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
inr : ∀ (c : Ordinal.{u_1}) (hc : c < o) (m : ℕ) (hm : a < ω ^ c * (↑m : Ordinal.{u_1})), a + a < ω ^ o
⊢ a + a < ω ^ o

Tactic:
obtain ⟨c, hc, m, hm⟩ := (lt_omega0_opow ha').1 ha

Premises used: Ordinal.lt_omega0_opow, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * (↑m : Ordinal.{u_1})
inr : ω ^ c * (↑m : Ordinal.{u_1}) + ω ^ c * (↑m : Ordinal.{u_1}) ≤ ω ^ o
⊢ a + a < ω ^ o

Tactic:
apply (add_lt_add_of_le_of_lt hm.le hm).trans_le

Premises used: add_lt_add_of_le_of_lt, LT.lt.le, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * (↑m : Ordinal.{u_1})
inr : ω ^ c * (↑(m + m) : Ordinal.{u_1}) ≤ ω ^ o
⊢ ω ^ c * (↑m : Ordinal.{u_1}) + ω ^ c * (↑m : Ordinal.{u_1}) ≤ ω ^ o

Tactic:
rw [← mul_add, ← Nat.cast_add]

Premises used: Nat.cast_add, mul_add
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * (↑m : Ordinal.{u_1})
⊢ ω ^ c * (↑(m + m) : Ordinal.{u_1}) ≤ ω ^ o

Tactic:
(omega0_opow_mul_nat_lt hc _).le

Premises used: LT.lt.le, Ordinal.omega0_opow_mul_nat_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * (↑m : Ordinal.{u_1})
⊢ ω ^ c * (↑(m + m) : Ordinal.{u_1}) ≤ ω ^ o

Tactic:
exact (omega0_opow_mul_nat_lt hc _).le

Premises used: LT.lt.le, Ordinal.omega0_opow_mul_nat_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
h : a < ω ^ b
⊢ a + ω ^ b = ω ^ b

Tactic:
(isPrincipal_add_omega0_opow b).add_eq_right h

Premises used: Ordinal.IsPrincipal.add_eq_right, Ordinal.isPrincipal_add_omega0_opow
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b c : Ordinal.{u}
h₁ : a < ω ^ b
h₂ : ω ^ b ≤ c
⊢ a + c = c

Tactic:
(isPrincipal_add_omega0_opow b).add_eq_right_of_le h₁ h₂

Premises used: Ordinal.IsPrincipal.add_eq_right_of_le, Ordinal.isPrincipal_add_omega0_opow
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
mp :
  IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o →
    o = 0 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ x) o
mpr :
  o = 0 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ x) o →
    IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o ↔
    o = 0 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ x) o

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
mp :
  IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o →
    ¬o = 0 → Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ x) o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o →
    o = 0 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ x) o

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o →
    ¬o = 0 → Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ x) o

Tactic:
fun H ho ↦ ⟨log ω o, (opow_log_le_self ω ho).eq_of_not_lt ?_⟩

Premises used: Ordinal.omega0, Set.Mem, setOf, Ordinal.opow_log_le_self, LE.le.eq_of_not_lt, Ordinal.log, Exists.intro, Set.range
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
mp : ∀ (H : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o) (ho : ¬o = 0), ¬ω ^ log ω o < o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o →
    ¬o = 0 → Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ x) o

Tactic:
refine fun H ho ↦ ⟨log ω o, (opow_log_le_self ω ho).eq_of_not_lt ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
H : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
ho : ¬o = 0
mp : ∀ (n : ℕ) (hn : o < ω ^ log ω o * (↑n : Ordinal.{u})), ¬ω ^ log ω o < o
⊢ ¬ω ^ log ω o < o

Tactic:
obtain ⟨n, hn⟩ := lt_omega0_opow_succ.1 (lt_opow_succ_log_self one_lt_omega0 o)

Premises used: Ordinal.lt_omega0_opow_succ, Ordinal.lt_opow_succ_log_self, Iff.mp, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
H : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
ho : ¬o = 0
n : ℕ
hn : o < ω ^ log ω o * (↑n : Ordinal.{u})
⊢ ¬ω ^ log ω o < o

Tactic:
fun h ↦ hn.not_gt <| H.mul_natCast_lt h n

Premises used: Ordinal.IsPrincipal.mul_natCast_lt, LT.lt.not_gt, Not
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
H : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
ho : ¬o = 0
n : ℕ
hn : o < ω ^ log ω o * (↑n : Ordinal.{u})
⊢ ¬ω ^ log ω o < o

Tactic:
exact fun h ↦ hn.not_gt <| H.mul_natCast_lt h n

Premises used: Ordinal.IsPrincipal.mul_natCast_lt, LT.lt.not_gt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0

Tactic:
isPrincipal_zero

Premises used: Ordinal.isPrincipal_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)

Tactic:
isPrincipal_add_omega0_opow a

Premises used: Ordinal.isPrincipal_add_omega0_opow
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0

Tactic:
exacts [isPrincipal_zero, isPrincipal_add_omega0_opow a]

Premises used: Ordinal.isPrincipal_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u_1}
ha : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) a
b : Ordinal.{u_1}
inl :
  ∀ (ha : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 0),
    IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (α := Ordinal.{u_1}) 0 b)
inr :
  ∀ (c : Ordinal.{u_1})
    (ha : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) ((fun (x : Ordinal.{u_1}) ↦ ω ^ x) c)),
    IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2)
      (HPow.hPow (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ ω ^ x) c) b)
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (a ^ b)

Tactic:
rcases isPrincipal_add_iff_zero_or_omega0_opow.1 ha with (rfl | ⟨c, rfl⟩)

Premises used: Ordinal.isPrincipal_add_iff_zero_or_omega0_opow, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b : Ordinal.{u_1}
ha : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 0
inl :
  IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0)
inl₁ : ∀ (hb : b ≠ 0), IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (α := Ordinal.{u_1}) 0 b)
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (α := Ordinal.{u_1}) 0 b)

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ha : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 0
inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 1
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0)

Tactic:
rw [opow_zero]

Premises used: Ordinal.opow_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ha : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 0
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 1

Tactic:
isPrincipal_add_one

Premises used: Ordinal.isPrincipal_add_one
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ha : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 0
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 1

Tactic:
exact isPrincipal_add_one

Premises used: Ordinal.isPrincipal_add_one
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b : Ordinal.{u_1}
ha : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 0
hb : b ≠ 0
inl inl₁ inl₂ inl₃ : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 0
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (α := Ordinal.{u_1}) 0 b)

Tactic:
rwa [zero_opow hb]

Premises used: Ordinal.zero_opow
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b c : Ordinal.{u_1}
ha : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) ((fun (x : Ordinal.{u_1}) ↦ ω ^ x) c)
inr : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ (c * b))
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2)
    (HPow.hPow (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ ω ^ x) c) b)

Tactic:
rw [← opow_mul]

Premises used: Ordinal.opow_mul
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b c : Ordinal.{u_1}
ha : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) ((fun (x : Ordinal.{u_1}) ↦ ω ^ x) c)
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ (c * b))

Tactic:
isPrincipal_add_omega0_opow _

Premises used: Ordinal.isPrincipal_add_omega0_opow
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b c : Ordinal.{u_1}
ha : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) ((fun (x : Ordinal.{u_1}) ↦ ω ^ x) c)
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ (c * b))

Tactic:
exact isPrincipal_add_omega0_opow _

Premises used: Ordinal.isPrincipal_add_omega0_opow
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
inl : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (0 * b)
inr : 0 < a → IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * b)
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * b)

Tactic:
rcases eq_zero_or_pos a with (rfl | _)

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
inl : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (0 * b)

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0

Tactic:
isPrincipal_zero

Premises used: Ordinal.isPrincipal_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0

Tactic:
exact isPrincipal_zero

Premises used: Ordinal.isPrincipal_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
inr :
  ∀ (hb₁ : Ne.{u + 2} (α := Ordinal.{u}) 0 1) (hb : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0),
    IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * 0)
inr₁ : ∀ (hb₁' : 0 < b), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * b)
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * b)

Tactic:
rcases eq_zero_or_pos b with (rfl | hb₁')

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
h : 0 < a
hb₁ : Ne.{u + 2} (α := Ordinal.{u}) 0 1
hb : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0
inr : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * 0)

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
h : 0 < a
hb₁ : Ne.{u + 2} (α := Ordinal.{u}) 0 1
hb : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0

Tactic:
isPrincipal_zero

Premises used: Ordinal.isPrincipal_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
h : 0 < a
hb₁ : Ne.{u + 2} (α := Ordinal.{u}) 0 1
hb : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0

Tactic:
exact isPrincipal_zero

Premises used: Ordinal.isPrincipal_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
hb₁' : 0 < b
⊢ 1 ≤ b

Tactic:
rw [← one_le_iff_pos] at hb₁'

Premises used: Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : c < a * b
hd : d < a * b
inr :
  ∀ (hc : ∃ c' < b, c < a * c') (hd : ∃ c' < b, d < a * c'),
    ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * b

Tactic:
rw [lt_mul_iff_of_isSuccLimit
        (isSuccLimit_of_isPrincipal_add (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *

Premises used: Ne.symm, Ordinal.isSuccLimit_of_isPrincipal_add, Ordinal.lt_mul_iff_of_isSuccLimit, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : ∃ c' < b, c < a * c'
hd : ∃ c' < b, d < a * c'
inr : ∀ (x : Ordinal.{u}) (hx : x < b) (hx' : c < a * x), ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'
⊢ ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'

Tactic:
rcases hc with ⟨x, hx, hx'⟩
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hd : ∃ c' < b, d < a * c'
x : Ordinal.{u}
hx : x < b
hx' : c < a * x
inr : ∀ (y : Ordinal.{u}) (hy : y < b) (hy' : d < a * y), ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'
⊢ ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'

Tactic:
rcases hd with ⟨y, hy, hy'⟩
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
right : (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * (x + y)
⊢ ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'

Tactic:
use x + y, hb hx hy
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
right : (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * x + a * y
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * (x + y)

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * x + a * y

Tactic:
Left.add_lt_add hx' hy'

Premises used: Left.add_lt_add
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * x + a * y

Tactic:
exact Left.add_lt_add hx' hy'

Premises used: Left.add_lt_add
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) 1

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u_1}
ha : a < 2
hb : b < 2
rw : ∀ (ha : a ≤ 1) (hb : b ≤ 1), LE.le.{u_1 + 1} (α := Ordinal.{u_1}) ((fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) a b) 1
⊢ LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) ((fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) a b) 2

Tactic:
rw [lt_two_iff] at *

Premises used: Order.lt_two_iff
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
⊢ LE.le.{u_1 + 1} (α := Ordinal.{u_1}) ((fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) a b) 1

Tactic:
simpa using mul_le_mul' ha hb

Premises used: mul_le_mul'
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : o ≤ 2
inl : ∀ (ho : LE.le.{u + 1} (α := Ordinal.{u}) 0 2), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0
inr : ∀ (ho : LE.le.{u + 1} (α := Ordinal.{u}) 1 2), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 1
inr₁ : ∀ (ho : LE.le.{u + 1} (α := Ordinal.{u}) 2 2), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 2
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o

Tactic:
obtain rfl | rfl | rfl := le_two_iff.1 ho

Premises used: Order.le_two_iff, Iff.mp, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : LE.le.{u + 1} (α := Ordinal.{u}) 0 2
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0

Tactic:
isPrincipal_zero

Premises used: Ordinal.isPrincipal_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : LE.le.{u + 1} (α := Ordinal.{u}) 1 2
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 1

Tactic:
isPrincipal_mul_one

Premises used: Ordinal.isPrincipal_mul_one
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : LE.le.{u + 1} (α := Ordinal.{u}) 2 2
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 2

Tactic:
isPrincipal_mul_two

Premises used: Ordinal.isPrincipal_mul_two
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : LE.le.{u + 1} (α := Ordinal.{u}) 0 2
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0

Tactic:
exacts [isPrincipal_zero, isPrincipal_mul_one, isPrincipal_mul_two]

Premises used: Ordinal.isPrincipal_zero, Ordinal.isPrincipal_mul_one, Ordinal.isPrincipal_mul_two
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂ : o ≠ 2
inl : ∀ (ho₁ : o < 2), IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
inr : ∀ (ho₂ : 2 < o), IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o

Tactic:
rcases lt_or_gt_of_ne ho₂ with ho₁ | ho₂

Premises used: lt_or_gt_of_ne