simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]
case intro.intro.intro.intro.refine_1
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ (mk (I i)) e = 1
no goals