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