-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
inst_1 : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
intro :
  ∀ (val : Fintype ι),
    Surjective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
      (⇑(quotientInfToPiQuotient I) : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
intro₁ :
  ∀ (val : Fintype ι) (g : (i : ι) → R ⧸ I i),
    ∃ (a : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)),
      (quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i) a = g
intro₂ :
  ∀ (val : Fintype ι) (g : (i : ι) → R ⧸ I i) (f : (i : ι) → R)
    (hf : ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i) = g i),
    ∃ (a : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)),
      (quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i) a = g
intro₃ :
  ∀ (val : Fintype ι) (g : (i : ι) → R ⧸ I i) (f : (i : ι) → R)
    (hf : ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i) = g i)
    (key :
      ∀ (i : ι),
        ∃ (e : R),
          Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) e : R ⧸ I i) (1 : R ⧸ I i) ∧
            ∀ (j : ι), j ≠ i → Eq (α := R ⧸ I j) ((Quotient.mk (I j) : (a : R) → R ⧸ I j) e : R ⧸ I j) (0 : R ⧸ I j)),
    ∃ (a : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)),
      (quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i) a = g
intro₄ :
  ∀ (val : Fintype ι) (g : (i : ι) → R ⧸ I i) (f : (i : ι) → R)
    (hf : ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i) = g i) (e : (i : ι) → R)
    (he :
      ∀ (i : ι),
        Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) (e i) : R ⧸ I i) (1 : R ⧸ I i) ∧
          ∀ (j : ι), j ≠ i → Eq (α := R ⧸ I j) ((Quotient.mk (I j) : (a : R) → R ⧸ I j) (e i) : R ⧸ I j) (0 : R ⧸ I j)),
    ∃ (a : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)),
      (quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i) a = g
h :
  ∀ (val : Fintype ι) (g : (i : ι) → R ⧸ I i) (f : (i : ι) → R)
    (hf : ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i) = g i) (e : (i : ι) → R)
    (he :
      ∀ (i : ι),
        Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) (e i) : R ⧸ I i) (1 : R ⧸ I i) ∧
          ∀ (j : ι), j ≠ i → Eq (α := R ⧸ I j) ((Quotient.mk (I j) : (a : R) → R ⧸ I j) (e i) : R ⧸ I j) (0 : R ⧸ I j)),
    (quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
        ((Quotient.mk (⨅ (i : ι), I i) : (a : R) → R ⧸ ⨅ (i : ι), I i) (∑ i : ι, f i * e i)) =
      g
h₁ :
  ∀ (val : Fintype ι) (g : (i : ι) → R ⧸ I i) (f : (i : ι) → R)
    (hf : ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i) = g i) (e : (i : ι) → R)
    (he :
      ∀ (i : ι),
        Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) (e i) : R ⧸ I i) (1 : R ⧸ I i) ∧
          ∀ (j : ι), j ≠ i → Eq (α := R ⧸ I j) ((Quotient.mk (I j) : (a : R) → R ⧸ I j) (e i) : R ⧸ I j) (0 : R ⧸ I j))
    (i : ι),
    (quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
        ((Quotient.mk (⨅ (i : ι), I i) : (a : R) → R ⧸ ⨅ (i : ι), I i) (∑ i : ι, f i * e i)) i =
      g i
⊢ Surjective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
    (⇑(quotientInfToPiQuotient I) : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
have h₂ : ∀ (val : Fintype ι) (g : (i : ι) → R ⧸ I i) (f : (i : ι) → R)
  (hf : ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i) = g i) (e : (i : ι) → R)
  (he :
    ∀ (i : ι),
      Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) (e i) : R ⧸ I i) (1 : R ⧸ I i) ∧
        ∀ (j : ι), j ≠ i → Eq (α := R ⧸ I j) ((Quotient.mk (I j) : (a : R) → R ⧸ I j) (e i) : R ⧸ I j) (0 : R ⧸ I j))
  (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i * e i) = g i
Tactic: classical
  cases nonempty_fintype ι
  intro g
  choose f hf using fun i ↦ mk_surjective (g i)
  have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
    intro i
    have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
      intro j hj
      exact hI (by simpa [ne_comm, isCoprime_iff_add] using hj)
    rcases isCoprime_iff_exists.mp (isCoprime_biInf hI') with ⟨u, hu, e, he, hue⟩
    replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he
    refine ⟨e, ?_, ?_⟩
    · simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]
    · exact fun j hj ↦ eq_zero_iff_mem.mpr (he j hj)
  choose e he using key
  use mk _ (∑ i, f i * e i)
  ext i
  rw [quotientInfToPiQuotient_mk', map_sum, Fintype.sum_eq_single i]
  · simp [(he i).1, hf]
  · intro j hj
    simp [(he j).2 i hj.symm]