case a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
⊢ ↑Subalgebra.toSubmodule (adjoin R s) ≤ span R ↑(Submonoid.closure s)

case a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
⊢ span R ↑(Submonoid.closure s) ≤ ↑Subalgebra.toSubmodule (adjoin R s)
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
⊢ ↑Subalgebra.toSubmodule (adjoin R s) = span R ↑(Submonoid.closure s)
apply le_antisymm
case a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
⊢ ↑(Submonoid.closure s) ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R s))
case a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
⊢ span R ↑(Submonoid.closure s) ≤ ↑Subalgebra.toSubmodule (adjoin R s)
refine' span_le.2 _
case a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
⊢ Submonoid.closure s ≤ (adjoin R s).toSubsemiring.toSubmonoid
case a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
⊢ ↑(Submonoid.closure s) ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R s))
change Submonoid.closure s ≤ (adjoin R s).toSubsemiring.toSubmonoid
no goals
case a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
⊢ Submonoid.closure s ≤ (adjoin R s).toSubsemiring.toSubmonoid
exact Submonoid.closure_le.2 subset_adjoin
case a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ r ∈ span R ↑(Submonoid.closure s)
case a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
⊢ ↑Subalgebra.toSubmodule (adjoin R s) ≤ span R ↑(Submonoid.closure s)
intro r hr
case a.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hr : List.sum (List.map List.prod L) ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ List.sum (List.map List.prod L) ∈ span R ↑(Submonoid.closure s)
case a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ r ∈ span R ↑(Submonoid.closure s)
rcases Subsemiring.mem_closure_iff_exists_list.1 hr with ⟨L, HL, rfl⟩
case a.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod L) ∈ span R ↑(Submonoid.closure s)
case a.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hr : List.sum (List.map List.prod L) ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ List.sum (List.map List.prod L) ∈ span R ↑(Submonoid.closure s)
clear hr
case a.intro.intro.nil
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
HL : ∀ (t : List A), t ∈ [] → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod []) ∈ span R ↑(Submonoid.closure s)

case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL : ∀ (t : List A), t ∈ hd :: tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod (hd :: tl)) ∈ span R ↑(Submonoid.closure s)
case a.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod L) ∈ span R ↑(Submonoid.closure s)
induction' L with hd tl ih
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL :
  (∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s) ∧
    ∀ (x : List A), x ∈ tl → ∀ (y : A), y ∈ x → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod (hd :: tl)) ∈ span R ↑(Submonoid.closure s)
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL : ∀ (t : List A), t ∈ hd :: tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod (hd :: tl)) ∈ span R ↑(Submonoid.closure s)
rw [List.forall_mem_cons] at HL
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL :
  (∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s) ∧
    ∀ (x : List A), x ∈ tl → ∀ (y : A), y ∈ x → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd + List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL :
  (∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s) ∧
    ∀ (x : List A), x ∈ tl → ∀ (y : A), y ∈ x → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod (hd :: tl)) ∈ span R ↑(Submonoid.closure s)
rw [List.map_cons, List.sum_cons]
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL :
  (∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s) ∧
    ∀ (x : List A), x ∈ tl → ∀ (y : A), y ∈ x → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL :
  (∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s) ∧
    ∀ (x : List A), x ∈ tl → ∀ (y : A), y ∈ x → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd + List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
refine' Submodule.add_mem _ _ (ih HL.2)
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL :
  (∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s) ∧
    ∀ (x : List A), x ∈ tl → ∀ (y : A), y ∈ x → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
replace HL := HL.1
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
clear ih tl
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod hd
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
suffices ∃ (z r : _) (_hr : r ∈ Submonoid.closure s), z • r = List.prod hd by
  rcases this with ⟨z, r, hr, hzr⟩
  rw [← hzr]
  exact smul_mem _ _ (subset_span hr)
case a.intro.intro.cons.nil
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL✝ : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
HL : ∀ (y : A), y ∈ [] → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod []

case a.intro.intro.cons.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : ∀ (y : A), y ∈ hd :: tl → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod (hd :: tl)
case a.intro.intro.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod hd
induction' hd with hd tl ih
case a.intro.intro.cons.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod (hd :: tl)
case a.intro.intro.cons.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : ∀ (y : A), y ∈ hd :: tl → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod (hd :: tl)
rw [List.forall_mem_cons] at HL
case a.intro.intro.cons.cons.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
⊢ ∃ z r _hr, z • r = List.prod (hd :: tl)
case a.intro.intro.cons.cons
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod (hd :: tl)
rcases ih HL.2 with ⟨z, r, hr, hzr⟩
case a.intro.intro.cons.cons.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
⊢ ∃ z_1 r_1 _hr, z_1 • r_1 = hd * z • r
case a.intro.intro.cons.cons.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
⊢ ∃ z r _hr, z • r = List.prod (hd :: tl)
rw [List.prod_cons, ← hzr]
case a.intro.intro.cons.cons.intro.intro.intro.inl.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
hd : R
HL : ↑(algebraMap R A) hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z_1 r_1 _hr, z_1 • r_1 = ↑(algebraMap R A) hd * z • r

case a.intro.intro.cons.cons.intro.intro.intro.inr
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
hs : hd ∈ s
⊢ ∃ z_1 r_1 _hr, z_1 • r_1 = hd * z • r
case a.intro.intro.cons.cons.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
⊢ ∃ z_1 r_1 _hr, z_1 • r_1 = hd * z • r
rcases HL.1 with (⟨hd, rfl⟩ | hs)
no goals
case a.intro.intro.nil
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
HL : ∀ (t : List A), t ∈ [] → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod []) ∈ span R ↑(Submonoid.closure s)
exact zero_mem _
case intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
z : ?m.199348
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod hd
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
this : ∃ z r _hr, z • r = List.prod hd
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
rcases this with ⟨z, r, hr, hzr⟩
case intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
z : ?m.199348
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod hd
⊢ z • r ∈ span R ↑(Submonoid.closure s)

R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ Type ?u.199445

R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ?m.199348 → (r : A) → r ∈ Submonoid.closure s → HSMul ?m.199348 A A
case intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
z : ?m.199348
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod hd
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
rw [← hzr]
no goals
case intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
z : ?m.199348
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod hd
⊢ z • r ∈ span R ↑(Submonoid.closure s)

R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ Type ?u.199445

R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ?m.199348 → (r : A) → r ∈ Submonoid.closure s → HSMul ?m.199348 A A
exact smul_mem _ _ (subset_span hr)
no goals
case a.intro.intro.cons.nil
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL✝ : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
HL : ∀ (y : A), y ∈ [] → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod []
exact ⟨1, 1, (Submonoid.closure s).one_mem', one_smul _ _⟩
case a.intro.intro.cons.cons.intro.intro.intro.inl.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
hd : R
HL : ↑(algebraMap R A) hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ (hd * z) • r = ↑(algebraMap R A) hd * z • r
case a.intro.intro.cons.cons.intro.intro.intro.inl.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
hd : R
HL : ↑(algebraMap R A) hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z_1 r_1 _hr, z_1 • r_1 = ↑(algebraMap R A) hd * z • r
refine' ⟨hd * z, r, hr, _⟩
no goals
case a.intro.intro.cons.cons.intro.intro.intro.inl.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
hd : R
HL : ↑(algebraMap R A) hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ (hd * z) • r = ↑(algebraMap R A) hd * z • r
rw [Algebra.smul_def, Algebra.smul_def, (algebraMap _ _).map_mul, _root_.mul_assoc]
no goals
case a.intro.intro.cons.cons.intro.intro.intro.inr
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
hs : hd ∈ s
⊢ ∃ z_1 r_1 _hr, z_1 • r_1 = hd * z • r
exact
  ⟨z, hd * r, Submonoid.mul_mem _ (Submonoid.subset_closure hs) hr,
    (mul_smul_comm _ _ _).symm⟩