-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
lemma adjoin_eq_span (s : Set A) : (adjoin R s).toSubmodule = span R (Subsemigroup.closure s)

Proof state:
case Hs
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (x y : A), x ∈ ↑(Subsemigroup.closure s) → y ∈ ↑(Subsemigroup.closure s) → x * y ∈ span R ↑(Subsemigroup.closure s)

case Hadd_l
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (x y z : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        z ∈ span R ↑(Subsemigroup.closure s) →
          x * z ∈ span R ↑(Subsemigroup.closure s) →
            y * z ∈ span R ↑(Subsemigroup.closure s) → (x + y) * z ∈ span R ↑(Subsemigroup.closure s)

case Hadd_r
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (x y z : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        z ∈ span R ↑(Subsemigroup.closure s) →
          x * y ∈ span R ↑(Subsemigroup.closure s) →
            x * z ∈ span R ↑(Subsemigroup.closure s) → x * (y + z) ∈ span R ↑(Subsemigroup.closure s)

case Hsmul_l
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (r : R) (x y : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        x * y ∈ span R ↑(Subsemigroup.closure s) → r • x * y ∈ span R ↑(Subsemigroup.closure s)

case Hsmul_r
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (r : R) (x y : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        x * y ∈ span R ↑(Subsemigroup.closure s) → x * r • y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
case Hs => exact fun x y hx hy ↦ subset_span <| mul_mem hx hy

Result:
case Hadd_l
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (x y z : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        z ∈ span R ↑(Subsemigroup.closure s) →
          x * z ∈ span R ↑(Subsemigroup.closure s) →
            y * z ∈ span R ↑(Subsemigroup.closure s) → (x + y) * z ∈ span R ↑(Subsemigroup.closure s)

case Hadd_r
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (x y z : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        z ∈ span R ↑(Subsemigroup.closure s) →
          x * y ∈ span R ↑(Subsemigroup.closure s) →
            x * z ∈ span R ↑(Subsemigroup.closure s) → x * (y + z) ∈ span R ↑(Subsemigroup.closure s)

case Hsmul_l
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (r : R) (x y : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        x * y ∈ span R ↑(Subsemigroup.closure s) → r • x * y ∈ span R ↑(Subsemigroup.closure s)

case Hsmul_r
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (r : R) (x y : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        x * y ∈ span R ↑(Subsemigroup.closure s) → x * r • y ∈ span R ↑(Subsemigroup.closure s)

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝³ x✝² y✝ : A
hx✝ : x✝² ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝² ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
r : R
x y : A
x✝¹ : x ∈ span R ↑(Subsemigroup.closure s)
x✝ : y ∈ span R ↑(Subsemigroup.closure s)
hxy : x * y ∈ span R ↑(Subsemigroup.closure s)
⊢ r • x * y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simpa [smul_mul_assoc] using smul_mem _ _ hxy

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝⁴ x✝³ y✝ : A
hx✝ : x✝³ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝³ ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
x y z : A
x✝² : x ∈ span R ↑(Subsemigroup.closure s)
x✝¹ : y ∈ span R ↑(Subsemigroup.closure s)
x✝ : z ∈ span R ↑(Subsemigroup.closure s)
hxz : x * z ∈ span R ↑(Subsemigroup.closure s)
hyz : y * z ∈ span R ↑(Subsemigroup.closure s)
⊢ (x + y) * z ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simpa [add_mul] using add_mem hxz hyz

Result:
no goals