ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
h : ∀ (i : κ), ∃ S, f i = span (Subtype.val '' S)
⊢ ∃ S, (⨆ (i : κ), f i) = span (Subtype.val '' S)
ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)
⊢ IsHomogeneous 𝒜 (⨆ (i : κ), f i)
simp_rw [iff_exists] at h⊢
ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ ∃ S, (⨆ (i : κ), f i) = span (Subtype.val '' S)
ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
h : ∀ (i : κ), ∃ S, f i = span (Subtype.val '' S)
⊢ ∃ S, (⨆ (i : κ), f i) = span (Subtype.val '' S)
choose s hs using h
ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ (⨆ (i : κ), f i) = span (Subtype.val '' ⋃ (i : κ), s i)
ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ ∃ S, (⨆ (i : κ), f i) = span (Subtype.val '' S)
refine' ⟨⋃ i, s i, _⟩
ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ (⨆ (i : κ), f i) = ⨆ (i : κ), span (Subtype.val '' s i)
ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ (⨆ (i : κ), f i) = span (Subtype.val '' ⋃ (i : κ), s i)
simp_rw [Set.image_iUnion, Ideal.span_iUnion]
case e_s
ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ (fun i => f i) = fun i => span (Subtype.val '' s i)
ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ (⨆ (i : κ), f i) = ⨆ (i : κ), span (Subtype.val '' s i)
congr
no goals
case e_s
ι : Type u_3
σ : Type u_4
R : Type ?u.122146
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
f : κ → Ideal A
s : κ → Set { x // x ∈ homogeneousSubmonoid 𝒜 }
hs : ∀ (i : κ), f i = span (Subtype.val '' s i)
⊢ (fun i => f i) = fun i => span (Subtype.val '' s i)
exact funext hs