case h.e'_3
α : Type u
β : Type ?u.63411
inst✝ : StrictOrderedSemiring α
a b c d : α
hn : 0 < a
hm : 1 < b
⊢ a = a * 1
α : Type u
β : Type ?u.63411
inst✝ : StrictOrderedSemiring α
a b c d : α
hn : 0 < a
hm : 1 < b
⊢ a < a * b
convert mul_lt_mul_of_pos_left hm hn
no goals
case h.e'_3
α : Type u
β : Type ?u.63411
inst✝ : StrictOrderedSemiring α
a b c d : α
hn : 0 < a
hm : 1 < b
⊢ a = a * 1
rw [mul_one]