simp [(he j).2 i hj.symm]
case h.h
ι : 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
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
i j : ι
hj : j ≠ i
⊢ (mk (I i)) (f j * e j) = 0
no goals