case inl
o : Ordinal
ho✝ : o ≤ 2
ho : o < 2
⊢ Principal (fun x x_1 => x * x_1) o

case inr
ho : 2 ≤ 2
⊢ Principal (fun x x_1 => x * x_1) 2
o : Ordinal
ho : o ≤ 2
⊢ Principal (fun x x_1 => x * x_1) o
rcases lt_or_eq_of_le ho with (ho | rfl)
case inl
o : Ordinal
ho✝ : o ≤ 2
ho : o < 2
h₂ : succ 1 = 2
⊢ Principal (fun x x_1 => x * x_1) o
case inl
o : Ordinal
ho✝ : o ≤ 2
ho : o < 2
⊢ Principal (fun x x_1 => x * x_1) o
have h₂ : succ (1 : Ordinal) = 2 := by simp
case inl
o : Ordinal
ho✝ : o ≤ 2
ho : o ≤ 1
h₂ : succ 1 = 2
⊢ Principal (fun x x_1 => x * x_1) o
case inl
o : Ordinal
ho✝ : o ≤ 2
ho : o < 2
h₂ : succ 1 = 2
⊢ Principal (fun x x_1 => x * x_1) o
rw [← h₂, lt_succ_iff] at ho
case inl.inl
o : Ordinal
ho✝¹ : o ≤ 2
ho✝ : o ≤ 1
h₂ : succ 1 = 2
ho : o < 1
⊢ Principal (fun x x_1 => x * x_1) o

case inl.inr
h₂ : succ 1 = 2
ho✝ : 1 ≤ 2
ho : 1 ≤ 1
⊢ Principal (fun x x_1 => x * x_1) 1
case inl
o : Ordinal
ho✝ : o ≤ 2
ho : o ≤ 1
h₂ : succ 1 = 2
⊢ Principal (fun x x_1 => x * x_1) o
rcases lt_or_eq_of_le ho with (ho | rfl)
no goals
o : Ordinal
ho✝ : o ≤ 2
ho : o < 2
⊢ succ 1 = 2
simp
case inl.inl
o : Ordinal
ho✝¹ : o ≤ 2
ho✝ : o ≤ 1
h₂ : succ 1 = 2
ho : o < 1
⊢ Principal (fun x x_1 => x * x_1) 0
case inl.inl
o : Ordinal
ho✝¹ : o ≤ 2
ho✝ : o ≤ 1
h₂ : succ 1 = 2
ho : o < 1
⊢ Principal (fun x x_1 => x * x_1) o
rw [lt_one_iff_zero.1 ho]
no goals
case inl.inl
o : Ordinal
ho✝¹ : o ≤ 2
ho✝ : o ≤ 1
h₂ : succ 1 = 2
ho : o < 1
⊢ Principal (fun x x_1 => x * x_1) 0
exact principal_zero
no goals
case inl.inr
h₂ : succ 1 = 2
ho✝ : 1 ≤ 2
ho : 1 ≤ 1
⊢ Principal (fun x x_1 => x * x_1) 1
exact principal_mul_one
no goals
case inr
ho : 2 ≤ 2
⊢ Principal (fun x x_1 => x * x_1) 2
exact principal_mul_two