α : Type ?u.250853
G : Type ?u.250856
M : Type ?u.250859
R : Type u_1
A : Type ?u.250865
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
hn : n ∈ S
⊢ m * n = 0
α : Type ?u.250853
G : Type ?u.250856
M : Type ?u.250859
R : Type u_1
A : Type ?u.250865
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m ∈ ⊥
n : R
hn : n ∈ S
⊢ m * n ∈ ⊥
rw [AddSubmonoid.mem_bot] at hm ⊢
no goals
α : Type ?u.250853
G : Type ?u.250856
M : Type ?u.250859
R : Type u_1
A : Type ?u.250865
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
hn : n ∈ S
⊢ m * n = 0
rw [hm, zero_mul]