awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
rw : ker f ≤ I ↔ ker f = I
⊢ Injective.{u + 1, v + 1} (α := R ⧸ I) (β := S) (⇑(Quotient.lift I f H) : (a : R ⧸ I) → S) ↔ ker f = I

Tactic:
rw [injective_iff_ker_eq_bot, ker_quotient_lift, map_eq_bot_iff_le_ker, mk_ker]

Premises used: Ideal.ker_quotient_lift, RingHom.injective_iff_ker_eq_bot, Ideal.mk_ker, Ideal.map_eq_bot_iff_le_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
mp : ker f ≤ I → ker f = I
mpr : ker f = I → ker f ≤ I
⊢ ker f ≤ I ↔ ker f = I

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
⊢ ker f ≤ I → ker f = I

Tactic:
fun h ↦ le_antisymm h H

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
⊢ ker f ≤ I → ker f = I

Tactic:
exact fun h ↦ le_antisymm h H

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
inst_2 : IsTwoSided (ker f)
H : ∀ (a : R), Membership.mem (γ := Ideal R) (ker f) a → Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
⊢ LE.le (α := Ideal R) (ker f) (ker f)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
ι : Type u_1
I : ι → Ideal R
inst_1 : ∀ (i : ι), (I i).IsTwoSided
⊢ Eq (α := Ideal R)
    (ker (F := R →+* (i : ι) → R ⧸ I i) (Pi.ringHom (f := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Quotient.mk (I i)))
    (⨅ (i : ι), I i)

Tactic:
simp [Pi.ker_ringHom, mk_ker]

Premises used: Pi.ker_ringHom, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
this : DivisionRing (R ⧸ I) := Quotient.divisionRing I
⊢ IsMaximal.{u} (α := R ⧸ I) ⊥

Tactic:
bot_isMaximal

Premises used: Ideal.bot_isMaximal
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
this : DivisionRing (R ⧸ I) := Quotient.divisionRing I
⊢ IsMaximal.{u} (α := R ⧸ I) ⊥

Tactic:
exact bot_isMaximal

Premises used: Ideal.bot_isMaximal
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
x : R
rw :
  Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      x ↔
    x ∈ J ⊔ I
rw₁ : x ∈ J ⊔ comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥ ↔ x ∈ J ⊔ I
rw₂ : x ∈ J ⊔ ker (F := R →+* R ⧸ I) (Quotient.mk I) ↔ x ∈ J ⊔ I
rw₃ rw₄ : x ∈ J ⊔ I ↔ x ∈ J ⊔ I
⊢ Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)
      ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
    x ∈ J ⊔ I

Tactic:
rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ←
    ker_eq_comap_bot, mk_ker]

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
hIJ : I ≤ J
x : R
rw : x ∈ J ⊔ I ↔ x ∈ J
rw₁ rw₂ : x ∈ J ↔ x ∈ J
⊢ Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)
      ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
    x ∈ J

Tactic:
rw [mem_quotient_iff_mem_sup, sup_eq_left.mpr hIJ]

Premises used: Iff.mpr, sup_eq_left, Ideal.mem_quotient_iff_mem_sup
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S
ι : Type u_1
I : ι → Ideal R
inst_2 : ∀ (i : ι), (I i).IsTwoSided
⊢ ∀ (a : R),
    Membership.mem (γ := Ideal R) (⨅ (i : ι), I i) a →
      Eq (α := (i : ι) → R ⧸ I i)
        (((Pi.ringHom (f := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Quotient.mk (I i) : R →+* (i : ι) → R ⧸ I i) :
              (a : R) → (i : ι) → R ⧸ I i)
            a :
          (i : ι) → R ⧸ I i)
        (0 : (i : ι) → R ⧸ I i)

Tactic:
simp [← RingHom.mem_ker, ker_Pi_Quotient_mk]

Premises used: Ideal.ker_Pi_Quotient_mk, RingHom.mem_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
ι : Type u_1
I : ι → Ideal R
inst_1 : ∀ (i : ι), (I i).IsTwoSided
x : R
⊢ Eq (α := (i : ι) → 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) x :
          HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) :
      (i : ι) → R ⧸ I i)
    fun (i : ι) ↦ ((Quotient.mk (I i) : (a : R) → R ⧸ I i) x : R ⧸ I i)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
ι : Type u_1
I : ι → Ideal R
inst_1 : ∀ (i : ι), (I i).IsTwoSided
x : R
i : ι
⊢ Eq.{u + 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) x :
          HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i))
        i :
      R ⧸ I i)
    ((Quotient.mk (I i) : (a : R) → R ⧸ I i) x : R ⧸ I i)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
inst : Ring R
ι : Type u_1
I : ι → Ideal R
inst_1 : ∀ (i : ι), (I i).IsTwoSided
rw :
  Injective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
    (⇑(lift (⨅ (i : ι), I i) (Pi.ringHom (f := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Quotient.mk (I i)) ⋯ :
          HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i) →+* (i : ι) → R ⧸ I i) :
      (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
rw₁ :
  Eq (α := Ideal R)
    (ker (F := R →+* (i : ι) → R ⧸ I i)
      (Pi.ringHom (f := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Quotient.mk (I i) : R →+* (i : ι) → R ⧸ I i))
    (⨅ (i : ι), I i)
rw₂ rw₃ : Eq.{u + 1} (α := Ideal R) (⨅ (i : ι), I i) (⨅ (i : ι), I i)
⊢ Injective (α := 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:
rw [quotientInfToPiQuotient, injective_lift_iff, ker_Pi_Quotient_mk]

Premises used: Ideal.ker_Pi_Quotient_mk, Ideal.quotientInfToPiQuotient, Ideal.injective_lift_iff
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
intro :
  ∀ (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
⊢ ∃ (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 f hf using fun i ↦ mk_surjective (g i)

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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 j : ι
hj : Membership.mem (γ := Finset ι) {i}ᶜ j
⊢ i ≠ j

Tactic:
simpa [ne_comm, isCoprime_iff_add] using hj

Premises used: ne_comm, Ideal.isCoprime_iff_add
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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 j : ι
hj : Membership.mem (γ := Finset ι) {i}ᶜ j
⊢ IsCoprime (I i) (I j)

Tactic:
exact hI (by simpa [ne_comm, isCoprime_iff_add] using hj)
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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 : ι
⊢ ∀ (j : ι), Membership.mem (γ := Finset ι) {i}ᶜ j → IsCoprime (I i) (I j)

Tactic:
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)
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
rcases :
  ∀ (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)
⊢ ∃ (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:
rcases isCoprime_iff_exists.mp (isCoprime_biInf hI') with ⟨u, hu, e, he, hue⟩

Premises used: Ideal.isCoprime_iff_exists, Iff.mp, Ideal.isCoprime_biInf
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
⊢ ∀ (j : ι), j ≠ i → e ∈ I j

Tactic:
simpa using he
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
⊢ ∀ (j : ι), j ≠ i → e ∈ I j

Tactic:
replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)

Tactic:
⟨e, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
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)
⊢ ∃ (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:
refine ⟨e, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
⊢ Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) e : R ⧸ I i) (1 : R ⧸ I i)

Tactic:
simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]

Premises used: Iff.mpr, map_sub, eq_sub_of_add_eq', Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
⊢ ∀ (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:
fun j hj ↦ eq_zero_iff_mem.mpr (he j hj)

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
⊢ ∀ (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:
exact fun j hj ↦ eq_zero_iff_mem.mpr (he j hj)

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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 : ι),
    ∃ (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)
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
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
⊢ ∃ (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
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
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
⊢ ∃ (a : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)),
    (quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i) a = g

Tactic:
use mk _ (∑ i, f i * e i)

Premises used: HMul.hMul, Finset.univ, Ideal.Quotient.mk, DFunLike.coe, Finset.sum
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
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
⊢ (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:
ext i
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
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)
⊢ (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:
rw [quotientInfToPiQuotient_mk', map_sum, Fintype.sum_eq_single i]

Premises used: map_sum, Ideal.quotientInfToPiQuotient_mk', Fintype.sum_eq_single
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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 : ι
⊢ (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i * e i) = g i

Tactic:
simp [(he i).1, hf]

Premises used: And.left
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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 j : ι
hj : j ≠ i
⊢ Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) (f j * e j) : R ⧸ I i) (0 : R ⧸ I i)

Tactic:
simp [(he j).2 i hj.symm]

Premises used: Ne.symm, And.right
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
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)
⊢ ∃ (r : R), ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) r = x i

Tactic:
obtain ⟨y, rfl⟩ := Ideal.quotientInfToPiQuotient_surj hf x

Premises used: Ideal.quotientInfToPiQuotient_surj, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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)
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)
⊢ ∃ (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 ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective, rfl