awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
inst_1 : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
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
i : ι
hI' : ∀ (j : ι), Membership.mem (γ := Finset ι) {i}ᶜ j → IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
he : Membership.mem (γ := Ideal R) (⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {i}ᶜ j), I j) e
hue : u + e = 1
⊢ ∃ (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)
have he₁ : ∀ (j : ι), j ≠ i → e ∈ I j
Tactic: replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he
Cleared hypotheses: he
-- 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)
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
i : ι
hI' : ∀ (j : ι), Membership.mem (γ := Finset ι) {i}ᶜ j → IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∃ (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)
have refine_1 : Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) e : R ⧸ I i) (1 : R ⧸ I i)
Tactic: refine ⟨e, ?_, ?_⟩
-- 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)
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
i : ι
hI' : ∀ (j : ι), Membership.mem (γ := Finset ι) {i}ᶜ j → IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
refine_1 : Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) e : R ⧸ I i) (1 : R ⧸ I 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)
have refine_2 : ∀ (j : ι), j ≠ i → Eq (α := R ⧸ I j) ((Quotient.mk (I j) : (a : R) → R ⧸ I j) e : R ⧸ I j) (0 : R ⧸ I j)
Tactic: refine ⟨e, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
inst_1 : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
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
have 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)
Tactic: 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)
-- 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)
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
have intro : ∀ (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
Tactic: choose e he using key
Cleared hypotheses: key
-- 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)
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
have h : (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
Tactic: use mk _ (∑ i, f i * e i)
-- 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)
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
have h : ∀ (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
Tactic: ext i
-- 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)
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
have h : (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i * e i) = g i
Tactic: rw [quotientInfToPiQuotient_mk', map_sum, Fintype.sum_eq_single i]
-- 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)
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 : ι
h : (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i * e i) = g 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
have h₁ : ∀ (x : ι), x ≠ i → Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) (f x * e x) : R ⧸ I i) (0 : R ⧸ I i)
Tactic: rw [quotientInfToPiQuotient_mk', map_sum, Fintype.sum_eq_single i]
-- 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)
⊢ 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 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)
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]
-- 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)
⊢ 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 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
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]
-- 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
⊢ 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 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
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]
-- 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
⊢ 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 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
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]
-- 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
⊢ 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 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
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]
-- 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
hf : Pairwise (IsCoprime on I)
x : (i : ι) → R ⧸ I i
⊢ ∃ (r : R), ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) r = x i
have obtain : ∀ (y : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)),
  ∃ (r : R),
    ∀ (i : ι),
      Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) r : R ⧸ I i)
        ((quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i) y i : R ⧸ I i)
Tactic: obtain ⟨y, rfl⟩ := Ideal.quotientInfToPiQuotient_surj hf x
Cleared hypotheses: x
-- 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
hf : Pairwise (IsCoprime on I)
y : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)
⊢ ∃ (r : R),
    ∀ (i : ι),
      Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) r : R ⧸ I i)
        ((quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i) y i : R ⧸ I i)
have obtain : ∀ (r : R),
  ∃ (r_1 : R),
    ∀ (i : ι),
      Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) r_1 : R ⧸ I i)
        ((quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
            ((Quotient.mk (⨅ (i : ι), I i) : (a : R) → R ⧸ ⨅ (i : ι), I i) r :
              HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i))
            i :
          R ⧸ I i)
Tactic: obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective y
Cleared hypotheses: y
-- 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)
x : ι → R
⊢ ∃ (r : R), ∀ (i : ι), r - x i ∈ I i
have obtain : ∀ (y : R)
  (hy :
    ∀ (i : ι),
      Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) y : R ⧸ I i)
        ((Quotient.mk (I i) : (a : R) → R ⧸ I i) (x i) : R ⧸ I i)),
  ∃ (r : R), ∀ (i : ι), r - x i ∈ I i
Tactic: obtain ⟨y, hy⟩ := Ideal.pi_quotient_surjective hI (fun i ↦ x i)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
ι_1 : Type u_1
R : Type u_2
inst_2 : CommRing R
ι : Type u_3
inst_3 : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
i j : Fin 2
h : i ≠ j
⊢ (IsCoprime on f) i j
have 0 : ∀ (h : (fun (i : Fin 2) ↦ i) ⟨0, sorry⟩ ≠ j), (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
ι_1 : Type u_1
R : Type u_2
inst_2 : CommRing R
ι : Type u_3
inst_3 : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
i j : Fin 2
h : i ≠ j
0 : ∀ (h : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j), (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
⊢ (IsCoprime on f) i j
have 1 : ∀ (h : (fun (i : Fin 2) ↦ i) ⟨1, sorry⟩ ≠ j), (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
ι_1 : Type u_1
R : Type u_2
inst_2 : CommRing R
ι : Type u_3
inst_3 : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
j : Fin 2
h : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have 0 : ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)),
  (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
ι_1 : Type u_1
R : Type u_2
inst_2 : CommRing R
ι : Type u_3
inst_3 : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
j : Fin 2
h : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
0 :
  ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have 0₁ : ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)),
  (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, h