case h.e'_3
R : Type u_3
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
γ : Sort u_1
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ HomogeneousIdeal.toIdeal (⨅ (i : γ), vanishingIdeal (t i)) =
    ⨅ (i : γ), HomogeneousIdeal.toIdeal (vanishingIdeal (t i))
R : Type u_3
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
γ : Sort u_1
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ HomogeneousIdeal.toIdeal (vanishingIdeal (⋃ (i : γ), t i)) =
    HomogeneousIdeal.toIdeal (⨅ (i : γ), vanishingIdeal (t i))
convert(gc_ideal 𝒜).u_iInf
no goals
case h.e'_3
R : Type u_3
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
γ : Sort u_1
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ HomogeneousIdeal.toIdeal (⨅ (i : γ), vanishingIdeal (t i)) =
    ⨅ (i : γ), HomogeneousIdeal.toIdeal (vanishingIdeal (t i))
exact HomogeneousIdeal.toIdeal_iInf _