α : Type ?u.252332
β : Type ?u.252335
γ : Type ?u.252338
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : a * b ≠ 0
⊢ a ≤ a * b
α : Type ?u.252332
β : Type ?u.252335
γ : Type ?u.252338
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a x✝ : Ordinal
b0 : x✝ ≠ 0
b : Ordinal
e : x✝ = a * b
⊢ a ≤ x✝
subst e
no goals
α : Type ?u.252332
β : Type ?u.252335
γ : Type ?u.252338
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : a * b ≠ 0
⊢ a ≤ a * b
simpa only [mul_one] using
  mul_le_mul_left'
    (one_le_iff_ne_zero.2 fun h : b = 0 => by simp only [h, mul_zero, Ne] at b0) a
no goals
α : Type ?u.252332
β : Type ?u.252335
γ : Type ?u.252338
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : a * b ≠ 0
h : b = 0
⊢ False
simp only [h, mul_zero, Ne] at b0