-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem addSubmonoid_smul_sup : M • (N ⊔ P) = M • N ⊔ M • P :=
  le_antisymm (smul_le.mpr fun m hm np hnp ↦ by
    refine closure_induction (p := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)
    · rintro x (hx | hx)
      exacts [le_sup_left (a := M • N) (smul_mem_smul hm hx),
        le_sup_right (a := M • N) (smul_mem_smul hm hx)]
    · apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem
    · intros _ _ _ _ h1 h2; rw [smul_add]; exact add_mem h1 h2)
  (sup_le (smul_le_smul_right le_sup_left) <| smul_le_smul_right le_sup_right)

Proof state:
case refine_3
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
hy✝ : y✝ ∈ closure (↑N ∪ ↑P)
h1 : m • x✝ ∈ M • N ⊔ M • P
h2 : m • y✝ ∈ M • N ⊔ M • P
⊢ m • (x✝ + y✝) ∈ M • N ⊔ M • P

Tactic:
rw [smul_add]

Result:
case refine_3
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
hy✝ : y✝ ∈ closure (↑N ∪ ↑P)
h1 : m • x✝ ∈ M • N ⊔ M • P
h2 : m • y✝ ∈ M • N ⊔ M • P
⊢ m • x✝ + m • y✝ ∈ M • N ⊔ M • P

Proof state:
case refine_3
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
hy✝ : y✝ ∈ closure (↑N ∪ ↑P)
h1 : m • x✝ ∈ M • N ⊔ M • P
h2 : m • y✝ ∈ M • N ⊔ M • P
⊢ m • x✝ + m • y✝ ∈ M • N ⊔ M • P

Tactic:
exact add_mem h1 h2

Result:
no goals

Proof state:
case refine_2
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ (fun x x_1 => m • x ∈ M • N ⊔ M • P) 0 ⋯

Tactic:
apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem

Result:
no goals

Proof state:
case refine_1
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ ∀ (x : A) (h : x ∈ ↑N ∪ ↑P), (fun x x_1 => m • x ∈ M • N ⊔ M • P) x ⋯

Tactic:
rintro x (hx | hx)

Result:
case refine_1.inl
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x : A
hx : x ∈ ↑N
⊢ m • x ∈ M • N ⊔ M • P

case refine_1.inr
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x : A
hx : x ∈ ↑P
⊢ m • x ∈ M • N ⊔ M • P

Proof state:
case refine_3
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
⊢ ∀ (x y : A) (hx : x ∈ closure (↑N ∪ ↑P)) (hy : y ∈ closure (↑N ∪ ↑P)),
    (fun x x_1 => m • x ∈ M • N ⊔ M • P) x hx →
      (fun x x_1 => m • x ∈ M • N ⊔ M • P) y hy → (fun x x_1 => m • x ∈ M • N ⊔ M • P) (x + y) ⋯

Tactic:
intros _ _ _ _ h1 h2

Result:
case refine_3
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
hy✝ : y✝ ∈ closure (↑N ∪ ↑P)
h1 : m • x✝ ∈ M • N ⊔ M • P
h2 : m • y✝ ∈ M • N ⊔ M • P
⊢ m • (x✝ + y✝) ∈ M • N ⊔ M • P

Proof state:
case refine_1.inl
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x : A
hx : x ∈ ↑N
⊢ m • x ∈ M • N ⊔ M • P

case refine_1.inr
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x : A
hx : x ∈ ↑P
⊢ m • x ∈ M • N ⊔ M • P

Tactic:
exacts [le_sup_left (a := M • N) (smul_mem_smul hm hx),
  le_sup_right (a := M • N) (smul_mem_smul hm hx)]

Result:
no goals