-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_mul_iff_mul_left_eq : Principal (· * ·) o ↔ ∀ a, 0 < a → a < o → a * o = o

Proof state:
case h.e'_2.h.e'_5.a
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 2

Tactic:
exact hao.trans_le ho

Result:
no goals

Proof state:
case refine_2.inr
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 => x1 * x2) a b < a * o

Tactic:
exact (isNormal_mul_right ha).strictMono hbo

Result:
no goals

Proof state:
case refine_1
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
⊢ a * o = o

Tactic:
rcases le_or_gt o 2 with ho | ho

Result:
case refine_1.inl
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a * o = o

case refine_1.inr
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o > 2
⊢ a * o = o

Proof state:
case refine_1.inr
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o > 2
⊢ a * o = o

Tactic:
exact op_eq_self_of_principal hao (isNormal_mul_right ha₀) h (isLimit_of_principal_mul ho h)

Result:
no goals

Proof state:
case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ 0 * b < o

Tactic:
rwa [zero_mul]

Result:
no goals

Proof state:
case h.e'_2.h.e'_5
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a = 1

Tactic:
apply le_antisymm

Result:
case h.e'_2.h.e'_5.a
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a ≤ 1

case h.e'_2.h.e'_5.a
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 1 ≤ a

Proof state:
case refine_2.inr
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 => x1 * x2) a b < o

Tactic:
rw [← Ordinal.pos_iff_ne_zero] at ha

Result:
case refine_2.inr
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 => x1 * x2) a b < o

Proof state:
o : Ordinal.{u}
⊢ Principal (fun x1 x2 => x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o

Tactic:
refine ⟨fun h a ha₀ hao => ?_, fun h a b hao hbo => ?_⟩

Result:
case refine_1
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
⊢ a * o = o

case refine_2
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 => x1 * x2) a b < o

Proof state:
case refine_2
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 => x1 * x2) a b < o

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ (fun x1 x2 => x1 * x2) 0 b < o

case refine_2.inr
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 => x1 * x2) a b < o

Proof state:
case h.e'_2.h.e'_5.a
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a ≤ 1

Tactic:
rw [← lt_succ_iff, succ_one]

Result:
case h.e'_2.h.e'_5.a
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 2

Proof state:
case h.e'_2.h.e'_5.a
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 1 ≤ a

Tactic:
rwa [← succ_le_iff, succ_zero] at ha₀

Result:
no goals

Proof state:
case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ (fun x1 x2 => x1 * x2) 0 b < o

Tactic:
dsimp only

Result:
case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ 0 * b < o

Proof state:
case refine_2.inr
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 => x1 * x2) a b < o

Tactic:
rw [← h a ha hao]

Result:
case refine_2.inr
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 => x1 * x2) a b < a * o

Proof state:
case refine_1.inl
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a * o = o

Tactic:
convert one_mul o

Result:
case h.e'_2.h.e'_5
o : Ordinal.{u}
h : Principal (fun x1 x2 => x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a = 1