apply hI
R : Type u_1
inst✝² : CommRing R
ι : Type
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → I i + I j = 1
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ I i + I j = 1
case a
R : Type u_1
inst✝² : CommRing R
ι : Type
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → I i + I j = 1
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ i ≠ j