α : Type ?u.249186
G : Type ?u.249189
M : Type ?u.249192
R : Type u_1
A : Type ?u.249198
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : R
hn : n = 0
⊢ m * n = 0
α : Type ?u.249186
G : Type ?u.249189
M : Type ?u.249192
R : Type u_1
A : Type ?u.249198
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : R
hn : n ∈ ⊥
⊢ m * n ∈ ⊥
rw [AddSubmonoid.mem_bot] at hn ⊢
no goals
α : Type ?u.249186
G : Type ?u.249189
M : Type ?u.249192
R : Type u_1
A : Type ?u.249198
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : R
hn : n = 0
⊢ m * n = 0
rw [hn, mul_zero]