M : Type u_2
A : Type ?u.259525
B : Type ?u.259528
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
b : R
hb : b ∈ AddSubmonoid.closure ↑S
⊢ ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * b ∈ AddSubmonoid.closure ↑S
M : Type u_2
A : Type ?u.259525
B : Type ?u.259528
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 ∈ AddSubmonoid.closure ↑S
⊢ a * b ∈ AddSubmonoid.closure ↑S
revert a
case refine'_1
M : Type u_2
A : Type ?u.259525
B : Type ?u.259528
R : Type u_1
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
⊢ ∀ (x : R), x ∈ ↑S → (fun z => ∀ {a : R}, a ∈ AddSubmonoid.closure ↑S → a * z ∈ AddSubmonoid.closure ↑S) x

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

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