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

Proof state:
case a.mul
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 ∈ span R ↑(Subsemigroup.closure s)

Tactic:
apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy

Result:
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)

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 ∈ span R ↑(Subsemigroup.closure s), x * 0 ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simp

Result:
no goals

Proof state:
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 Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy

Result:
no goals

Proof state:
case a.smul
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✝ : A
r : R
x : A
hx✝ : x ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
⊢ r • x ∈ span R ↑(Subsemigroup.closure s)

Tactic:
exact smul_mem _ _ hpx

Result:
no goals