R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
⊢ (⨅ (i : ι) (_ : i ∈ J), ker (proj i)) ≤ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
⊢ (⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)) = ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
refine' le_antisymm (iSup_range_stdBasis_le_iInf_ker_proj _ _ _ _ hd) _
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
this : Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
⊢ (⨅ (i : ι) (_ : i ∈ J), ker (proj i)) ≤ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
⊢ (⨅ (i : ι) (_ : i ∈ J), ker (proj i)) ≤ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
have : Set.univ ⊆ ↑hI.toFinset ∪ J := by rwa [hI.coe_toFinset]
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
this : Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
i : ι
⊢ (⨆ (_ : i ∈ Set.Finite.toFinset hI), range (stdBasis R φ i)) ≤ ⨆ (_ : i ∈ I), range (stdBasis R φ i)
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
this : Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
⊢ (⨅ (i : ι) (_ : i ∈ J), ker (proj i)) ≤ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
refine' le_trans (iInf_ker_proj_le_iSup_range_stdBasis R φ this) (iSup_mono fun i => _)
no goals
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
this : Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
i : ι
⊢ (⨆ (_ : i ∈ Set.Finite.toFinset hI), range (stdBasis R φ i)) ≤ ⨆ (_ : i ∈ I), range (stdBasis R φ i)
rw [Set.Finite.mem_toFinset]
no goals
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
⊢ Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
rwa [hI.coe_toFinset]