ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i in s, span R (M i) = span R (∏ i in s, M i)
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
⊢ ∏ i in s, span R (M i) = span R (∏ i in s, M i)
letI := Classical.decEq ι
case refine'_1
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i in ∅, span R (M i) = span R (∏ i in ∅, M i)

case refine'_2
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ∏ i in s, span R (M i) = span R (∏ i in s, M i) →
        ∏ i in insert a s, span R (M i) = span R (∏ i in insert a s, M i)
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i in s, span R (M i) = span R (∏ i in s, M i)
refine' Finset.induction_on s _ _
no goals
case refine'_1
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i in ∅, span R (M i) = span R (∏ i in ∅, M i)
simp [one_eq_span, Set.singleton_one]
case refine'_2
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : ¬a✝ ∈ s✝
ih : ∏ i in s✝, span R (M i) = span R (∏ i in s✝, M i)
⊢ ∏ i in insert a✝ s✝, span R (M i) = span R (∏ i in insert a✝ s✝, M i)
case refine'_2
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ∏ i in s, span R (M i) = span R (∏ i in s, M i) →
        ∏ i in insert a s, span R (M i) = span R (∏ i in insert a s, M i)
intro _ _ H ih
no goals
case refine'_2
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : ¬a✝ ∈ s✝
ih : ∏ i in s✝, span R (M i) = span R (∏ i in s✝, M i)
⊢ ∏ i in insert a✝ s✝, span R (M i) = span R (∏ i in insert a✝ s✝, M i)
rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]