M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a : R
ha : a ∈ AddSubmonoid.closure ↑S
⊢ ∀ {b : R}, b ∈ S → a * b ∈ AddSubmonoid.closure ↑S
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ AddSubmonoid.closure ↑S
hb : b ∈ S
⊢ a * b ∈ AddSubmonoid.closure ↑S
revert b
case refine'_1
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x : R), x ∈ ↑S → (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) x

case refine'_2
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) 0

case refine'_3
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x y : R),
    (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) x →
      (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) y →
        (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) (x + y)
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a : R
ha : a ∈ AddSubmonoid.closure ↑S
⊢ ∀ {b : R}, b ∈ S → a * b ∈ AddSubmonoid.closure ↑S
refine' @AddSubmonoid.closure_induction _ _ _
  (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure S) _ ha _ _ _ <;> clear ha a
no goals
case refine'_1
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x : R), x ∈ ↑S → (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) x
exact fun r hr b hb => AddSubmonoid.mem_closure.mpr fun y hy => hy (mul_mem hr hb)
no goals
case refine'_2
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) 0
exact fun b _ => by simp only [zero_mul, (AddSubmonoid.closure (S : Set R)).zero_mem]
no goals
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
b : R
x✝ : b ∈ S
⊢ 0 * b ∈ AddSubmonoid.closure ↑S
simp only [zero_mul, (AddSubmonoid.closure (S : Set R)).zero_mem]
case refine'_3
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x y : R),
    (∀ (b : R), b ∈ S → x * b ∈ AddSubmonoid.closure ↑S) →
      (∀ (b : R), b ∈ S → y * b ∈ AddSubmonoid.closure ↑S) → ∀ (b : R), b ∈ S → x * b + y * b ∈ AddSubmonoid.closure ↑S
case refine'_3
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x y : R),
    (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) x →
      (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) y →
        (fun z => ∀ (b : R), b ∈ S → z * b ∈ AddSubmonoid.closure ↑S) (x + y)
simp_rw [add_mul]
no goals
case refine'_3
M : Type u_2
A : Type ?u.256135
B : Type ?u.256138
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x y : R),
    (∀ (b : R), b ∈ S → x * b ∈ AddSubmonoid.closure ↑S) →
      (∀ (b : R), b ∈ S → y * b ∈ AddSubmonoid.closure ↑S) → ∀ (b : R), b ∈ S → x * b + y * b ∈ AddSubmonoid.closure ↑S
exact fun r s hr hs b hb => (AddSubmonoid.closure (S : Set R)).add_mem (hr _ hb) (hs _ hb)