simp at he
case intro.intro.intro.intro.refine_2
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 : ι
hI' : ∀ j ∈ {i}ᶜ, I i + I j = 1
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ (j : ι) (_ : j ∈ {i}ᶜ), I j
hue : u + e = 1
j : ι
hj : j ≠ i
⊢ e ∈ I j
case intro.intro.intro.intro.refine_2
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 : ι
hI' : ∀ j ∈ {i}ᶜ, I i + I j = 1
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
j : ι
hj : j ≠ i
he : ∀ (i_1 : ι), ¬i_1 = i → e ∈ I i_1
⊢ e ∈ I j