case intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
⊢ FG (↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
⊢ FG (↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
rcases fg_def.1 h1 with ⟨p, hp, hp'⟩
case intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ FG (↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
case intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
⊢ FG (↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
rcases fg_def.1 h2 with ⟨q, hq, hq'⟩
case intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ span R (p * q) ≤ ↑Subalgebra.toSubmodule (adjoin R (s ∪ t))

case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ ↑Subalgebra.toSubmodule (adjoin R (s ∪ t)) ≤ span R (p * q)
case intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ FG (↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
refine' fg_def.2 ⟨p * q, hp.mul hq, le_antisymm _ _⟩
case intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ p * q ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
case intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ span R (p * q) ≤ ↑Subalgebra.toSubmodule (adjoin R (s ∪ t))
rw [span_le]
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ (fun x x_1 => x * x_1) x y ∈ ↑(↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
case intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ p * q ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
rintro _ ⟨x, y, hx, hy, rfl⟩
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x * y ∈ adjoin R (s ∪ t)
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ (fun x x_1 => x * x_1) x y ∈ ↑(↑Subalgebra.toSubmodule (adjoin R (s ∪ t)))
change x * y ∈ adjoin R (s ∪ t)
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x ∈ adjoin R (s ∪ t)

case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ y ∈ adjoin R (s ∪ t)
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x * y ∈ adjoin R (s ∪ t)
refine' Subalgebra.mul_mem _ _ _
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
this : y ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ y ∈ adjoin R (s ∪ t)
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ y ∈ adjoin R (s ∪ t)
have : y ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) := by
  rw [← hq']
  exact subset_span hy
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
this : y ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ y ∈ adjoin R (s ∪ t)
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
this : y ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ y ∈ adjoin R (s ∪ t)
change y ∈ adjoin R (s ∪ t)
no goals
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
this : y ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ y ∈ adjoin R (s ∪ t)
rwa [adjoin_union_eq_adjoin_adjoin]
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
this : x ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ x ∈ adjoin R (s ∪ t)
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x ∈ adjoin R (s ∪ t)
have : x ∈ Subalgebra.toSubmodule (adjoin R s) := by
  rw [← hp']
  exact subset_span hx
no goals
case intro.intro.intro.intro.refine'_1.intro.intro.intro.intro.refine'_1
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
this : x ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ x ∈ adjoin R (s ∪ t)
exact adjoin_mono (Set.subset_union_left _ _) this
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x ∈ span R p
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x ∈ ↑Subalgebra.toSubmodule (adjoin R s)
rw [← hp']
no goals
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ x ∈ span R p
exact subset_span hx
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ y ∈ span { x // x ∈ adjoin R s } q
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ y ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
rw [← hq']
no goals
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
x y : A
hx : x ∈ p
hy : y ∈ q
⊢ y ∈ span { x // x ∈ adjoin R s } q
exact subset_span hy
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (adjoin R (s ∪ t))
⊢ r ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ ↑Subalgebra.toSubmodule (adjoin R (s ∪ t)) ≤ span R (p * q)
intro r hr
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ adjoin R (s ∪ t)
⊢ r ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (adjoin R (s ∪ t))
⊢ r ∈ span R (p * q)
change r ∈ adjoin R (s ∪ t) at hr
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ Subalgebra.restrictScalars R (adjoin { x // x ∈ adjoin R s } t)
⊢ r ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ adjoin R (s ∪ t)
⊢ r ∈ span R (p * q)
rw [adjoin_union_eq_adjoin_adjoin] at hr
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ r ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ Subalgebra.restrictScalars R (adjoin { x // x ∈ adjoin R s } t)
⊢ r ∈ span R (p * q)
change r ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) at hr
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr :
  ∃ l,
    l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q ∧
      ↑(Finsupp.total A A { x // x ∈ adjoin R s } _root_.id) l = r
⊢ r ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
⊢ r ∈ span R (p * q)
rw [← hq', ← Set.image_id q, Finsupp.mem_span_image_iff_total (adjoin R s)] at hr
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
⊢ ↑(Finsupp.total A A { x // x ∈ adjoin R s } _root_.id) l ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
r : A
hr :
  ∃ l,
    l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q ∧
      ↑(Finsupp.total A A { x // x ∈ adjoin R s } _root_.id) l = r
⊢ r ∈ span R (p * q)
rcases hr with ⟨l, hlq, rfl⟩
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
⊢ ↑(Finsupp.total A A { x // x ∈ adjoin R s } _root_.id) l ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
⊢ ↑(Finsupp.total A A { x // x ∈ adjoin R s } _root_.id) l ∈ span R (p * q)
have := @Finsupp.total_apply A A (adjoin R s)
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
⊢ (Finset.sum l.support fun a => ↑l a • _root_.id a) ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
⊢ ↑(Finsupp.total A A { x // x ∈ adjoin R s } _root_.id) l ∈ span R (p * q)
rw [this, Finsupp.sum]
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
⊢ ∀ (c : A), c ∈ l.support → ↑l c • _root_.id c ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
⊢ (Finset.sum l.support fun a => ↑l a • _root_.id a) ∈ span R (p * q)
refine' sum_mem _
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
⊢ ↑l z • _root_.id z ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
⊢ ∀ (c : A), c ∈ l.support → ↑l c • _root_.id c ∈ span R (p * q)
intro z hz
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
⊢ ↑l z • _root_.id z ∈ span R (p * q)
change (l z).1 * _ ∈ _
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
this : ↑(↑l z) ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
have : (l z).1 ∈ Subalgebra.toSubmodule (adjoin R s) := (l z).2
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
this : ∃ l_1, l_1 ∈ Finsupp.supported R R p ∧ ↑(Finsupp.total A A R _root_.id) l_1 = ↑(↑l z)
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
this : ↑(↑l z) ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
rw [← hp', ← Set.image_id p, Finsupp.mem_span_image_iff_total R] at this
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : ↑(Finsupp.total A A R _root_.id) l2 = ↑(↑l z)
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
this : ∃ l_1, l_1 ∈ Finsupp.supported R R p ∧ ↑(Finsupp.total A A R _root_.id) l_1 = ↑(↑l z)
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
rcases this with ⟨l2, hlp, hl⟩
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : ↑(Finsupp.total A A R _root_.id) l2 = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : ↑(Finsupp.total A A R _root_.id) l2 = ↑(↑l z)
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
have := @Finsupp.total_apply A A R
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : ↑(Finsupp.total A A R _root_.id) l2 = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
rw [this] at hl
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ (Finsupp.sum l2 fun a c => c • _root_.id a * _root_.id z) ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ ↑(↑l z) * _root_.id z ∈ span R (p * q)
rw [← hl, Finsupp.sum_mul]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ ∀ (c : A), c ∈ l2.support → (fun a c => c • _root_.id a * _root_.id z) c (↑l2 c) ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ (Finsupp.sum l2 fun a c => c • _root_.id a * _root_.id z) ∈ span R (p * q)
refine' sum_mem _
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ (fun a c => c • _root_.id a * _root_.id z) t (↑l2 t) ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
⊢ ∀ (c : A), c ∈ l2.support → (fun a c => c • _root_.id a * _root_.id z) c (↑l2 c) ∈ span R (p * q)
intro t ht
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ ↑l2 t • _root_.id t * _root_.id z ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ (fun a c => c • _root_.id a * _root_.id z) t (↑l2 t) ∈ span R (p * q)
change _ * _ ∈ _
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ ↑l2 t • (_root_.id t * _root_.id z) ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ ↑l2 t • _root_.id t * _root_.id z ∈ span R (p * q)
rw [smul_mul_assoc]
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ _root_.id t * _root_.id z ∈ span R (p * q)
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ ↑l2 t • (_root_.id t * _root_.id z) ∈ span R (p * q)
refine' smul_mem _ _ _
no goals
case intro.intro.intro.intro.refine'_2.intro.intro.intro.intro
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : FG (↑Subalgebra.toSubmodule (adjoin R s))
h2 : FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝))
p : Set A
hp : Set.Finite p
hp' : span R p = ↑Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : Set.Finite q
hq' : span { x // x ∈ adjoin R s } q = ↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R s } t✝)
l : A →₀ { x // x ∈ adjoin R s }
hlq : l ∈ Finsupp.supported { x // x ∈ adjoin R s } { x // x ∈ adjoin R s } q
this✝ :
  ∀ [inst : Semiring { x // x ∈ adjoin R s }] [inst_1 : AddCommMonoid A] [inst_2 : Module { x // x ∈ adjoin R s } A]
    {v : A → A} (l : A →₀ { x // x ∈ adjoin R s }),
    ↑(Finsupp.total A A { x // x ∈ adjoin R s } v) l = Finsupp.sum l fun i a => a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.sum l2 fun i a => a • _root_.id i) = ↑(↑l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    ↑(Finsupp.total A A R v) l = Finsupp.sum l fun i a => a • v i
t : A
ht : t ∈ l2.support
⊢ _root_.id t * _root_.id z ∈ span R (p * q)
exact subset_span ⟨t, z, hlp ht, hlq hz, rfl⟩