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

Proof state:
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 Hadd_l => exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz

Result:
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:
case a
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
hx : x ∈ (adjoin R s).toSubmodule
⊢ x ∈ span R ↑(Subsemigroup.closure s)

Tactic:
induction hx using adjoin_induction with
| mem x hx => exact subset_span <| Subsemigroup.subset_closure hx
| add x y _ _ hpx hpy => exact add_mem hpx hpy
| zero => exact zero_mem _
| mul x y _ _ hpx hpy =>
  apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
  case Hs => exact fun x y hx hy ↦ subset_span <| mul_mem hx hy
  case Hadd_l => exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
  case Hadd_r => exact fun x y z _ _ _ hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
  case Hsmul_l => exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
  case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
| smul r x _ hpx => exact smul_mem _ _ hpx

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 * y ∈ span R ↑(Subsemigroup.closure s)
hyz : x * z ∈ span R ↑(Subsemigroup.closure s)
⊢ x * (y + z) ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simpa [mul_add] using add_mem hxz hyz

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
⊢ Subsemigroup.closure s ≤ (adjoin R s).toSubsemigroup

Tactic:
exact Subsemigroup.closure_le.2 (subset_adjoin R)

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
⊢ (adjoin R s).toSubmodule = span R ↑(Subsemigroup.closure s)

Tactic:
apply le_antisymm

Result:
case a
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
⊢ (adjoin R s).toSubmodule ≤ span R ↑(Subsemigroup.closure s)

case a
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
⊢ span R ↑(Subsemigroup.closure s) ≤ (adjoin R s).toSubmodule