awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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)
⊢ a + c = c
have rw₂ : b + (c - b) = b + (c - b)
Tactic: rw [← Ordinal.add_sub_cancel_of_le hbc, ← add_assoc, hb.add_eq_right hab,
    Ordinal.add_sub_cancel_of_le hbc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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)
⊢ a + c = c
have rw₃ : 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]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
a : Ordinal.{u}
ha : ¬IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a
⊢ ∃ b < a, ∃ c < a, b + c = a
have ha₁ : ∃ a_1 < a, ∃ b < a, a ≤ a_1 + b
Tactic: rw [not_isPrincipal_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a : Ordinal.{u}
ha : ∃ a_1 < a, ∃ b < a, a ≤ a_1 + b
⊢ ∃ b < a, ∃ c < a, b + c = a
have rcases : ∀ (b : Ordinal.{u}) (hb : b < a) (c : Ordinal.{u}) (hc : c < a) (H : a ≤ b + c), ∃ b < a, ∃ c < a, b + c = a
Tactic: rcases ha with ⟨b, hb, c, hc, H⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
have lt_of_le_of_ne : ∀ (hab : a - b = a), False
Tactic: refine
    ⟨b, hb, _, lt_of_le_of_ne (sub_le_self a b) fun hab => ?_, Ordinal.add_sub_cancel_of_le hb.le⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
hab : a - b = a
⊢ False
have H₁ : a ≤ c
Tactic: rw [← sub_le, hab] at H
Cleared hypotheses: H, hab
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a
have by_contra : ∀ (ha : ¬IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a), False
Tactic: by_contra ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
ha : ¬IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a
⊢ False
have 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
Tactic: rcases exists_lt_add_of_not_isPrincipal_add ha with ⟨b, hb, c, hc, rfl⟩
Cleared hypotheses: a, H, ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ o)
have inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (β := Ordinal.{u_1}) ω 0)
Tactic: obtain rfl | ha' := eq_or_ne o 0
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u_1}
inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (β := Ordinal.{u_1}) ω 0)
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ o)
have inr : ∀ (ha' : o ≠ 0), IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ o)
Tactic: obtain rfl | ha' := eq_or_ne o 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (β := Ordinal.{u_1}) ω 0)
have inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 1
Tactic: rw [opow_zero, isPrincipal_one_iff, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
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}) ω 0)
have inl₁ : HAdd.hAdd (α := Ordinal.{u_1}) 0 0 = 0
Tactic: rw [opow_zero, isPrincipal_one_iff, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 1
inl₁ : HAdd.hAdd (α := Ordinal.{u_1}) 0 0 = 0
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (β := Ordinal.{u_1}) ω 0)
have inl₂ : Eq.{u_1 + 2} (α := Ordinal.{u_1}) 0 0
Tactic: rw [opow_zero, isPrincipal_one_iff, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ o)
have inr : ∀ b < ω ^ o, b + b < ω ^ o
Tactic: rw [isPrincipal_add_iff_add_self_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
⊢ a + a < ω ^ o
have inr : ∀ (c : Ordinal.{u_1}) (hc : c < o) (m : ℕ) (hm : a < ω ^ c * (↑m : Ordinal.{u_1})), a + a < ω ^ o
Tactic: obtain ⟨c, hc, m, hm⟩ := (lt_omega0_opow ha').1 ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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})
⊢ a + a < ω ^ o
have inr : ω ^ c * (↑m : Ordinal.{u_1}) + ω ^ c * (↑m : Ordinal.{u_1}) ≤ ω ^ o
Tactic: apply (add_lt_add_of_le_of_lt hm.le hm).trans_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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 : Ordinal.{u_1}) + ω ^ c * (↑m : Ordinal.{u_1}) ≤ ω ^ o
have inr : ω ^ c * (↑(m + m) : Ordinal.{u_1}) ≤ ω ^ o
Tactic: rw [← mul_add, ← Nat.cast_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
have 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
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
have mp : ∀ (H : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o) (ho : ¬o = 0), ¬ω ^ log ω o < o
Tactic: refine fun H ho ↦ ⟨log ω o, (opow_log_le_self ω ho).eq_of_not_lt ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
H : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
ho : ¬o = 0
⊢ ¬ω ^ log ω o < o
have mp : ∀ (n : ℕ) (hn : o < ω ^ log ω o * (↑n : Ordinal.{u})), ¬ω ^ log ω o < o
Tactic: obtain ⟨n, hn⟩ := lt_omega0_opow_succ.1 (lt_opow_succ_log_self one_lt_omega0 o)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a : Ordinal.{u_1}
ha : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) a
b : Ordinal.{u_1}
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (a ^ b)
have 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)
Tactic: rcases isPrincipal_add_iff_zero_or_omega0_opow.1 ha with (rfl | ⟨c, rfl⟩)
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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)
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (a ^ b)
have 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)
Tactic: rcases isPrincipal_add_iff_zero_or_omega0_opow.1 ha with (rfl | ⟨c, rfl⟩)
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
b : Ordinal.{u_1}
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)
have inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0)
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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)
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (HPow.hPow (α := Ordinal.{u_1}) 0 b)
have inl₁ : ∀ (hb : b ≠ 0), 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)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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) (HPow.hPow (α := Ordinal.{u_1}) (β := Ordinal.{u_1}) 0 0)
have inl : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 1
Tactic: rw [opow_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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)
    (HPow.hPow (α := Ordinal.{u_1}) ((fun (x : Ordinal.{u_1}) ↦ ω ^ x) c) b)
have inr : IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) (ω ^ (c * b))
Tactic: rw [← opow_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a 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) (a * b)
have inl : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (0 * b)
Tactic: rcases eq_zero_or_pos a with (rfl | _)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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)
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * b)
have inr : 0 < a → IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * b)
Tactic: rcases eq_zero_or_pos a with (rfl | _)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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 * b)
have inl : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * b)
have 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)
Tactic: rcases eq_zero_or_pos b with (rfl | hb₁')
Cleared hypotheses: b, hb₁, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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)
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * b)
have inr₁ : ∀ (hb₁' : 0 < b), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * b)
Tactic: rcases eq_zero_or_pos b with (rfl | hb₁')
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
h : 0 < a
hb₁' : 0 < b
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) (a * b)
have hb₁'₁ : 1 ≤ b
Tactic: rw [← one_le_iff_pos] at hb₁'
Cleared hypotheses: hb₁'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * b
have 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'
Tactic: rw [lt_mul_iff_of_isSuccLimit
        (isSuccLimit_of_isPrincipal_add (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *
Cleared hypotheses: hc, hd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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'
⊢ ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'
have inr : ∀ (x : Ordinal.{u}) (hx : x < b) (hx' : c < a * x), ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'
Tactic: rcases hc with ⟨x, hx, hx'⟩
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
⊢ ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'
have inr : ∀ (y : Ordinal.{u}) (hy : y < b) (hy' : d < a * y), ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'
Tactic: rcases hd with ⟨y, hy, hy'⟩
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
⊢ ∃ c' < b, (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * c'
have right : (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * (x + y)
Tactic: use x + y, hb hx hy
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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 + y)
have right : (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) c d < a * x + a * y
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u_1}
ha : a < 2
hb : b < 2
⊢ LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) ((fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) a b) 2
have 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
Tactic: rw [lt_two_iff] at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : o ≤ 2
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
have inl : ∀ (ho : LE.le.{u + 1} (α := Ordinal.{u}) 0 2), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0
Tactic: obtain rfl | rfl | rfl := le_two_iff.1 ho
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
have inr : ∀ (ho : LE.le.{u + 1} (α := Ordinal.{u}) 1 2), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 1
Tactic: obtain rfl | rfl | rfl := le_two_iff.1 ho
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
have inr₁ : ∀ (ho : LE.le.{u + 1} (α := Ordinal.{u}) 2 2), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 2
Tactic: obtain rfl | rfl | rfl := le_two_iff.1 ho
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂ : o ≠ 2
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
have inl : ∀ (ho₁ : o < 2), IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
Tactic: rcases lt_or_gt_of_ne ho₂ with ho₁ | ho₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
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
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
have inr : ∀ (ho₂ : 2 < o), IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
Tactic: rcases lt_or_gt_of_ne ho₂ with ho₁ | ho₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂_1 : o ≠ 2
ho₂ : 2 < o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
have inr : ∀ b < o, b * 2 < o
Tactic: simp_rw [isPrincipal_add_iff_add_self_lt, ← Ordinal.mul_two]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
have refine_1 : ∀ (h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o) (a : Ordinal.{u}) (ha₀ : 0 < a) (hao : a < o), a * o = o
Tactic: refine ⟨fun h a ha₀ hao => ?_, fun h a b hao hbo => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
refine_1 :
  ∀ (h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o) (a : Ordinal.{u}) (ha₀ : 0 < a) (hao : a < o), a * o = o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
have refine_2 : ∀ (h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o) (a b : Ordinal.{u}) (hao : a < o) (hbo : b < o),
  (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < o
Tactic: refine ⟨fun h a ha₀ hao => ?_, fun h a b hao hbo => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
⊢ a * o = o
have refine_1 : ∀ (ho : o ≤ 2), a * o = o
Tactic: rcases le_or_gt o 2 with ho | ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
refine_1 : ∀ (ho : o ≤ 2), a * o = o
⊢ a * o = o
have refine_1₁ : ∀ (ho : 2 < o), a * o = o
Tactic: rcases le_or_gt o 2 with ho | ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a * o = o
have h₁ : a = 1
Tactic: convert! one_mul o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a = 1
have h₁ : a ≤ 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
h₁ : a ≤ 1
⊢ a = 1
have h₂ : 1 ≤ a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a ≤ 1
have h₁ : a < 2
Tactic: rw [← lt_add_one_iff, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < o
have refine_2 : ∀ (hao : 0 < o), (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0 b < o
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a, hao
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
refine_2 : ∀ (hao : 0 < o), (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0 b < o
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < o
have refine_2₁ : ∀ (ha : a ≠ 0), (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < o
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (hypothesis)
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : a ≠ 0
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < o
have ha₁ : 0 < a
Tactic: rw [← pos_iff_ne_zero] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < o
have refine_2 : (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < a * o
Tactic: rw [← h a ha hao]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b : Ordinal.{u_1}
m n : ℕ
ha : (↑m : Ordinal.{u_1}) < ω
hb : (↑n : Ordinal.{u_1}) < ω
⊢ HMul.hMul (α := Ordinal.{u_1}) (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1}) < ω
have rw : (↑(m * n) : Ordinal.{u_1}) < ω
Tactic: rw [← natCast_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
⊢ a * b < ω ^ c
have inl : ∀ (c0 : LT.lt.{u + 1} (α := Ordinal.{u}) 0 0) (ha : a < HPow.hPow (β := Ordinal.{u}) ω 0),
  a * b < HPow.hPow (β := Ordinal.{u}) ω 0
Tactic: rcases zero_or_succ_or_isSuccLimit c with (rfl | ⟨c, rfl⟩ | l)
Cleared hypotheses: c, c0, ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
inl :
  ∀ (c0 : LT.lt.{u + 1} (α := Ordinal.{u}) 0 0) (ha : a < HPow.hPow (β := Ordinal.{u}) ω 0),
    a * b < HPow.hPow (β := Ordinal.{u}) ω 0
⊢ a * b < ω ^ c
have inr : ∀ (c : Ordinal.{u}) (c0 : 0 < succ c) (ha : a < ω ^ succ c), a * b < ω ^ succ c
Tactic: rcases zero_or_succ_or_isSuccLimit c with (rfl | ⟨c, rfl⟩ | l)
Cleared hypotheses: c, c0, ha