no goals
α : Type ?u.242292
G : Type ?u.242295
M✝ : Type ?u.242298
R : Type u_1
A : Type ?u.242304
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
C : R → Prop
r : R
hr : r ∈ M * N
hm : ∀ (m : R), m ∈ M → ∀ (n : R), n ∈ N → C (m * n)
ha : ∀ (x y : R), C x → C y → C (x + y)
⊢ 0 ∈ { carrier := setOf C, add_mem' := (_ : ∀ {a b : R}, C a → C b → C (a + b)) }.carrier
simpa only [zero_mul] using hm _ (zero_mem _) _ (zero_mem _)