R : Type u_2
S : Type ?u.133565
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_1
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
R : Type u_2
S : Type ?u.133565
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_1
s : Finset ι
p : ι → Submodule R M
⊢ ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
letI := Classical.decEq ι
case refine'_1
R : Type u_2
S : Type ?u.133565
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_1
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Finset.inf ∅ p) = ⋂ (i : ι) (_ : i ∈ ∅), ↑(p i)

case refine'_2
R : Type u_2
S : Type ?u.133565
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_1
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
ih : ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
⊢ ↑(Finset.inf (insert i s) p) = ⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), ↑(p i_1)
R : Type u_2
S : Type ?u.133565
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_1
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
refine' s.induction_on _ fun i s _ ih ↦ _
no goals
case refine'_1
R : Type u_2
S : Type ?u.133565
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_1
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Finset.inf ∅ p) = ⋂ (i : ι) (_ : i ∈ ∅), ↑(p i)
simp
case refine'_2
R : Type u_2
S : Type ?u.133565
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_1
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
ih : ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
⊢ (↑(p i) ∩ ⋂ (i : ι) (_ : i ∈ s), ↑(p i)) = ⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), ↑(p i_1)
case refine'_2
R : Type u_2
S : Type ?u.133565
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_1
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
ih : ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
⊢ ↑(Finset.inf (insert i s) p) = ⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), ↑(p i_1)
rw [Finset.inf_insert, inf_coe, ih]
no goals
case refine'_2
R : Type u_2
S : Type ?u.133565
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_1
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
ih : ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
⊢ (↑(p i) ∩ ⋂ (i : ι) (_ : i ∈ s), ↑(p i)) = ⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), ↑(p i_1)
simp