a b : Ordinal
ha : a < 2
hb : b < 2
h₂ : succ 1 = 2
⊢ (fun x x_1 => x * x_1) a b < 2
a b : Ordinal
ha : a < 2
hb : b < 2
⊢ (fun x x_1 => x * x_1) a b < 2
have h₂ : succ (1 : Ordinal) = 2 := by simp
a b : Ordinal
ha : a < 2
hb : b < 2
h₂ : succ 1 = 2
⊢ a * b < 2
a b : Ordinal
ha : a < 2
hb : b < 2
h₂ : succ 1 = 2
⊢ (fun x x_1 => x * x_1) a b < 2
dsimp only
a b : Ordinal
ha : a ≤ 1
hb : b ≤ 1
h₂ : succ 1 = 2
⊢ a * b ≤ 1
a b : Ordinal
ha : a < 2
hb : b < 2
h₂ : succ 1 = 2
⊢ a * b < 2
rw [← h₂, lt_succ_iff] at ha hb ⊢
case h.e'_4
a b : Ordinal
ha : a ≤ 1
hb : b ≤ 1
h₂ : succ 1 = 2
⊢ 1 = 1 * 1
a b : Ordinal
ha : a ≤ 1
hb : b ≤ 1
h₂ : succ 1 = 2
⊢ a * b ≤ 1
convert mul_le_mul' ha hb
no goals
case h.e'_4
a b : Ordinal
ha : a ≤ 1
hb : b ≤ 1
h₂ : succ 1 = 2
⊢ 1 = 1 * 1
exact (mul_one 1).symm
no goals
a b : Ordinal
ha : a < 2
hb : b < 2
⊢ succ 1 = 2
simp