case inl
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ Principal (fun x x_1 => x + x_1) o

case inr
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
⊢ Principal (fun x x_1 => x + x_1) o
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
⊢ Principal (fun x x_1 => x + x_1) o
cases' lt_or_gt_of_ne ho₂ with ho₁ ho₂
case inl
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o < succ 1
⊢ Principal (fun x x_1 => x + x_1) o
case inl
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ Principal (fun x x_1 => x + x_1) o
replace ho₁ : o < succ 1 := by simpa using ho₁
case inl
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o ≤ 1
⊢ Principal (fun x x_1 => x + x_1) o
case inl
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o < succ 1
⊢ Principal (fun x x_1 => x + x_1) o
rw [lt_succ_iff] at ho₁
no goals
case inl
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o ≤ 1
⊢ Principal (fun x x_1 => x + x_1) o
exact principal_add_of_le_one ho₁
no goals
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ o < succ 1
simpa using ho₁
case inr
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x + x_1) a b ≤ (fun x x_1 => x * x_1) (max a b) 2
case inr
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
⊢ Principal (fun x x_1 => x + x_1) o
refine' fun a b hao hbo => lt_of_le_of_lt _ (ho (max_lt hao hbo) ho₂)
case inr
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal
hao : a < o
hbo : b < o
⊢ a + b ≤ max a b * 2
case inr
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x + x_1) a b ≤ (fun x x_1 => x * x_1) (max a b) 2
dsimp only
case inr
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal
hao : a < o
hbo : b < o
⊢ a + b ≤ max a b + max a b
case inr
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal
hao : a < o
hbo : b < o
⊢ a + b ≤ max a b * 2
rw [← one_add_one_eq_two, mul_add, mul_one]
no goals
case inr
o : Ordinal
ho : Principal (fun x x_1 => x * x_1) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal
hao : a < o
hbo : b < o
⊢ a + b ≤ max a b + max a b
exact add_le_add (le_max_left a b) (le_max_right a b)