case h.e'_3
α : Type ?u.192331
β : Type ?u.192334
γ : Type ?u.192337
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
hb : 0 < b
⊢ a = a * 1
α : Type ?u.192331
β : Type ?u.192334
γ : Type ?u.192337
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
hb : 0 < b
⊢ a ≤ a * b
convert mul_le_mul_left' (one_le_iff_pos.2 hb) a
no goals
case h.e'_3
α : Type ?u.192331
β : Type ?u.192334
γ : Type ?u.192337
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
hb : 0 < b
⊢ a = a * 1
rw [mul_one a]