case refine'_1
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
⊢ a * o = o

case refine'_2
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
a b : Ordinal
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x * x_1) a b < o
o : Ordinal
⊢ Principal (fun x x_1 => x * x_1) o ↔ ∀ (a : Ordinal), 0 < a → a < o → a * o = o
refine' ⟨fun h a ha₀ hao => _, fun h a b hao hbo => _⟩
case refine'_1.inl
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a * o = o

case refine'_1.inr
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o > 2
⊢ a * o = o
case refine'_1
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
⊢ a * o = o
cases' le_or_gt o 2 with ho ho
case h.e'_2.h.e'_5
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a = 1
case refine'_1.inl
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a * o = o
convert one_mul o
case h.e'_2.h.e'_5.a
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a ≤ 1

case h.e'_2.h.e'_5.a
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 1 ≤ a
case h.e'_2.h.e'_5
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a = 1
apply le_antisymm
case h.e'_2.h.e'_5.a
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
this : a < succ 1
⊢ a ≤ 1
case h.e'_2.h.e'_5.a
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a ≤ 1
have : a < succ 1 := hao.trans_le (by simpa using ho)
no goals
case h.e'_2.h.e'_5.a
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
this : a < succ 1
⊢ a ≤ 1
rwa [lt_succ_iff] at this
no goals
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ o ≤ succ 1
simpa using ho
no goals
case h.e'_2.h.e'_5.a
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 1 ≤ a
rwa [← succ_le_iff, succ_zero] at ha₀
no goals
case refine'_1.inr
o : Ordinal
h : Principal (fun x x_1 => x * x_1) o
a : Ordinal
ha₀ : 0 < a
hao : a < o
ho : o > 2
⊢ a * o = o
exact op_eq_self_of_principal hao (mul_isNormal ha₀) h (principal_mul_isLimit ho h)
case refine'_2.inl
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
b : Ordinal
hbo : b < o
hao : 0 < o
⊢ (fun x x_1 => x * x_1) 0 b < o

case refine'_2.inr
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
a b : Ordinal
hao : a < o
hbo : b < o
ha : a ≠ 0
⊢ (fun x x_1 => x * x_1) a b < o
case refine'_2
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
a b : Ordinal
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x * x_1) a b < o
rcases eq_or_ne a 0 with (rfl | ha)
case refine'_2.inr
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
a b : Ordinal
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x x_1 => x * x_1) a b < o
case refine'_2.inr
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
a b : Ordinal
hao : a < o
hbo : b < o
ha : a ≠ 0
⊢ (fun x x_1 => x * x_1) a b < o
rw [← Ordinal.pos_iff_ne_zero] at ha
case refine'_2.inr
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
a b : Ordinal
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x x_1 => x * x_1) a b < a * o
case refine'_2.inr
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
a b : Ordinal
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x x_1 => x * x_1) a b < o
rw [← h a ha hao]
no goals
case refine'_2.inr
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
a b : Ordinal
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x x_1 => x * x_1) a b < a * o
exact (mul_isNormal ha).strictMono hbo
case refine'_2.inl
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
b : Ordinal
hbo : b < o
hao : 0 < o
⊢ 0 * b < o
case refine'_2.inl
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
b : Ordinal
hbo : b < o
hao : 0 < o
⊢ (fun x x_1 => x * x_1) 0 b < o
dsimp only
no goals
case refine'_2.inl
o : Ordinal
h : ∀ (a : Ordinal), 0 < a → a < o → a * o = o
b : Ordinal
hbo : b < o
hao : 0 < o
⊢ 0 * b < o
rwa [zero_mul]