-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_eq_span : Subalgebra.toSubmodule (adjoin R s) = span R (Submonoid.closure s)

Proof state:
case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Submonoid.closure s ≤ (adjoin R s).toSubmonoid

Tactic:
exact Submonoid.closure_le.2 subset_adjoin

Result:
no goals

Proof state:
case a.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
L : List (List A)
HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
hr : (List.map List.prod L).sum ∈ Subalgebra.toSubmodule (adjoin R s)
⊢ (List.map List.prod L).sum ∈ span R ↑(Submonoid.closure s)

Tactic:
clear hr

Result:
case a.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
L : List (List A)
HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod L).sum ∈ span R ↑(Submonoid.closure s)

Proof state:
case intro.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
z : ?m.39683
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = hd.prod
⊢ z • r ∈ span R ↑(Submonoid.closure s)

Tactic:
exact smul_mem _ _ (subset_span hr)

Result:
no goals

Proof state:
case a.intro.intro.nil
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
HL : ∀ t ∈ [], ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod []).sum ∈ span R ↑(Submonoid.closure s)

Tactic:
exact zero_mem _

Result:
no goals

Proof state:
case a.intro.intro.cons.cons.intro.intro.intro.inr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hs : hd ∈ s
⊢ ∃ z_1 r_1, ∃ (_ : r_1 ∈ Submonoid.closure s), z_1 • r_1 = hd * z • r

Tactic:
exact
  ⟨z, hd * r, Submonoid.mul_mem _ (Submonoid.subset_closure hs) hr,
    (mul_smul_comm _ _ _).symm⟩

Result:
no goals

Proof state:
case a.intro.intro.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : (∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod (hd :: tl)).sum ∈ span R ↑(Submonoid.closure s)

Tactic:
rw [List.map_cons, List.sum_cons]

Result:
case a.intro.intro.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : (∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ hd.prod + (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)

Proof state:
case intro.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
z : ?m.39683
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = hd.prod
⊢ hd.prod ∈ span R ↑(Submonoid.closure s)

Tactic:
rw [← hzr]

Result:
case intro.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
z : ?m.39683
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = hd.prod
⊢ z • r ∈ span R ↑(Submonoid.closure s)

Proof state:
case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Subalgebra.toSubmodule (adjoin R s) ≤ span R ↑(Submonoid.closure s)

Tactic:
intro r hr

Result:
case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
r : A
hr : r ∈ Subalgebra.toSubmodule (adjoin R s)
⊢ r ∈ span R ↑(Submonoid.closure s)

Proof state:
case a.intro.intro.cons.cons.intro.intro.intro.inl.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hd : R
HL : (algebraMap R A) hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (hd * z) • r = (algebraMap R A) hd * z • r

Tactic:
rw [Algebra.smul_def, Algebra.smul_def, (algebraMap _ _).map_mul, _root_.mul_assoc]

Result:
no goals

Proof state:
case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
r : A
hr : r ∈ Subalgebra.toSubmodule (adjoin R s)
⊢ r ∈ span R ↑(Submonoid.closure s)

Tactic:
rcases Subsemiring.mem_closure_iff_exists_list.1 hr with ⟨L, HL, rfl⟩

Result:
case a.intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
L : List (List A)
HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
hr : (List.map List.prod L).sum ∈ Subalgebra.toSubmodule (adjoin R s)
⊢ (List.map List.prod L).sum ∈ span R ↑(Submonoid.closure s)

Proof state:
case a.intro.intro.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : (∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ hd.prod ∈ span R ↑(Submonoid.closure s)

Tactic:
replace HL := HL.1

Result:
case a.intro.intro.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ hd.prod ∈ span R ↑(Submonoid.closure s)

Proof state:
case a.intro.intro.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod (hd :: tl)).sum ∈ span R ↑(Submonoid.closure s)

Tactic:
rw [List.forall_mem_cons] at HL

Result:
case a.intro.intro.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : (∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod (hd :: tl)).sum ∈ span R ↑(Submonoid.closure s)