awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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:
⟨r, fun i ↦ rfl⟩

Premises used: Exists.intro, 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)
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:
exact ⟨r, fun i ↦ rfl⟩
-- 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)
⊢ Surjective (α := R) (β := (i : ι) → R ⧸ I i)
    (⇑(LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) : (a : R) → (i : ι) → R ⧸ I i)

Tactic:
fun x ↦ have ⟨r, eq⟩ := pi_quotient_surjective hI x; ⟨r, funext eq⟩

Premises used: Exists, LinearMap.pi, funext, Exists.intro, Submodule.mkQ, _private.0.Ideal.pi_mkQ_surjective.match_1, Eq, DFunLike.coe, Function.Surjective, Ideal.pi_quotient_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)
x : ι → R
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
⊢ ∃ (r : R), ∀ (i : ι), r - x i ∈ I i

Tactic:
obtain ⟨y, hy⟩ := Ideal.pi_quotient_surjective hI (fun i ↦ x i)

Premises used: Ideal.Quotient.mk, DFunLike.coe, Ideal.pi_quotient_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)
x : ι → R
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:
⟨y, fun i ↦ (Submodule.Quotient.eq (I i)).mp <| hy i⟩

Premises used: Submodule.Quotient.eq, Exists.intro, Iff.mp
-- 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)
x : ι → R
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:
exact ⟨y, fun i ↦ (Submodule.Quotient.eq (I i)).mp <| hy i⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
1 : ∀ (h : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j), (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ (IsCoprime on f) i j

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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, ⋯⟩)
h_1 :
  ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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) ⟨1, ⋯⟩ ≠ j
1 :
  ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h_1 :
  ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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]
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, ⋯⟩)

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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]
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, ⋯⟩)

Tactic:
try contradiction
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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]
h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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]
h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
try contradiction
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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]
h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
assumption
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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]
h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
coprime.symm

Premises used: Eq.mpr, IsCoprime.symm, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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]
h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
exact coprime.symm

Premises used: IsCoprime.symm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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]
hf : Pairwise (IsCoprime on f)
⊢ I ⊓ J = ⨅ (i : Fin 2), f i

Tactic:
simp [f, iInf, inf_comm]

Premises used: iInf, inf_comm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x : R ⧸ I ⊓ J
⊢ Eq (α := R ⧸ I) (((I.quotientInfEquivQuotientProd J coprime : (a : R ⧸ I ⊓ J) → (R ⧸ I) × R ⧸ J) x).1 : R ⧸ I)
    ((factor ⋯ : (a : R ⧸ I ⊓ J) → R ⧸ I) x : R ⧸ I)

Tactic:
Quot.inductionOn x fun _ => rfl

Premises used: Quot.inductionOn
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x : R ⧸ I ⊓ J
⊢ Eq (α := R ⧸ J) (((I.quotientInfEquivQuotientProd J coprime : (a : R ⧸ I ⊓ J) → (R ⧸ I) × R ⧸ J) x).2 : R ⧸ J)
    ((factor ⋯ : (a : R ⧸ I ⊓ J) → R ⧸ J) x : R ⧸ J)

Tactic:
Quot.inductionOn x fun _ => rfl

Premises used: Quot.inductionOn
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
h :
  Eq (α := R →+* R ⧸ I)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
        (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I ⊓ J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I ⊓ J)))
⊢ Eq (α := R ⧸ I ⊓ J →+* R ⧸ I)
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
      (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
    (factor ⋯)

Tactic:
apply Quotient.ringHom_ext

Premises used: Ideal.Quotient.ringHom_ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
h :
  ∀ (x : R),
    Eq (α := R ⧸ I)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
                (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
              (Quotient.mk (I ⊓ J)) :
            (a : R) → R ⧸ I)
          x :
        R ⧸ I)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I ⊓ J)) : (a : R) → R ⧸ I) x :
        R ⧸ I)
⊢ Eq (α := R →+* R ⧸ I)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
        (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I ⊓ J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I ⊓ J)))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x : R
⊢ Eq (α := R ⧸ I)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
              (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
            (Quotient.mk (I ⊓ J)) :
          (a : R) → R ⧸ I)
        x :
      R ⧸ I)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I ⊓ J)) : (a : R) → R ⧸ I) x : R ⧸ I)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
h :
  Eq (α := R →+* R ⧸ J)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
        (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I ⊓ J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I ⊓ J)))
⊢ Eq (α := R ⧸ I ⊓ J →+* R ⧸ J)
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
      (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
    (factor ⋯)

Tactic:
apply Quotient.ringHom_ext

Premises used: Ideal.Quotient.ringHom_ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
h :
  ∀ (x : R),
    Eq (α := R ⧸ J)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
                (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
              (Quotient.mk (I ⊓ J)) :
            (a : R) → R ⧸ J)
          x :
        R ⧸ J)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I ⊓ J)) : (a : R) → R ⧸ J) x :
        R ⧸ J)
⊢ Eq (α := R →+* R ⧸ J)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
        (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I ⊓ J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I ⊓ J)))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x : R
⊢ Eq (α := R ⧸ J)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
              (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
            (Quotient.mk (I ⊓ J)) :
          (a : R) → R ⧸ J)
        x :
      R ⧸ J)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I ⊓ J)) : (a : R) → R ⧸ J) x : R ⧸ J)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x : R ⧸ I * J
⊢ Eq (α := R ⧸ I) (((I.quotientMulEquivQuotientProd J coprime : (a : R ⧸ I * J) → (R ⧸ I) × R ⧸ J) x).1 : R ⧸ I)
    ((factor ⋯ : (a : R ⧸ I * J) → R ⧸ I) x : R ⧸ I)

Tactic:
Quot.inductionOn x fun _ => rfl

Premises used: Quot.inductionOn
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x : R ⧸ I * J
⊢ Eq (α := R ⧸ J) (((I.quotientMulEquivQuotientProd J coprime : (a : R ⧸ I * J) → (R ⧸ I) × R ⧸ J) x).2 : R ⧸ J)
    ((factor ⋯ : (a : R ⧸ I * J) → R ⧸ J) x : R ⧸ J)

Tactic:
Quot.inductionOn x fun _ => rfl

Premises used: Quot.inductionOn
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
h :
  Eq (α := R →+* R ⧸ I)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
        (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I * J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I * J)))
⊢ Eq (α := R ⧸ I * J →+* R ⧸ I)
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
      (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
    (factor ⋯)

Tactic:
apply Quotient.ringHom_ext

Premises used: Ideal.Quotient.ringHom_ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
h :
  ∀ (x : R),
    Eq (α := R ⧸ I)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
                (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
              (Quotient.mk (I * J)) :
            (a : R) → R ⧸ I)
          x :
        R ⧸ I)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I * J)) : (a : R) → R ⧸ I) x :
        R ⧸ I)
⊢ Eq (α := R →+* R ⧸ I)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
        (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I * J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I * J)))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x : R
⊢ Eq (α := R ⧸ I)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
              (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
            (Quotient.mk (I * J)) :
          (a : R) → R ⧸ I)
        x :
      R ⧸ I)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I * J)) : (a : R) → R ⧸ I) x : R ⧸ I)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
h :
  Eq (α := R →+* R ⧸ J)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
        (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I * J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I * J)))
⊢ Eq (α := R ⧸ I * J →+* R ⧸ J)
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
      (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
    (factor ⋯)

Tactic:
apply Quotient.ringHom_ext

Premises used: Ideal.Quotient.ringHom_ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
h :
  ∀ (x : R),
    Eq (α := R ⧸ J)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
                (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
              (Quotient.mk (I * J)) :
            (a : R) → R ⧸ J)
          x :
        R ⧸ J)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I * J)) : (a : R) → R ⧸ J) x :
        R ⧸ J)
⊢ Eq (α := R →+* R ⧸ J)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
        (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I * J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I * J)))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x : R
⊢ Eq (α := R ⧸ J)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
              (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
            (Quotient.mk (I * J)) :
          (a : R) → R ⧸ J)
        x :
      R ⧸ J)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I * J)) : (a : R) → R ⧸ J) x : R ⧸ J)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
I : Ideal A
inst_7 : I.IsTwoSided
r : R₁
x_1 : A ⧸ I
x : A
⊢ HMul.hMul (α := A ⧸ I) (β := A ⧸ I)
      (((RingHom.comp (mk I) (algebraMap R₁ A) : RingHom.{u_1, u_3} R₁ (A ⧸ I)) : (a : R₁) → A ⧸ I) r : A ⧸ I)
      (Quot.mk (⇑(Submodule.quotientRel I) : A → A → Prop) x) =
    HMul.hMul (α := A ⧸ I) (β := A ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : A → A → Prop) x)
      (((RingHom.comp (mk I) (algebraMap R₁ A) : RingHom.{u_1, u_3} R₁ (A ⧸ I)) : (a : R₁) → A ⧸ I) r : A ⧸ I)

Tactic:
congr_arg (⟦·⟧) (Algebra.commutes r x)

Premises used: Quotient.map₂, Quotient.mk, congr_arg, Submodule.quotientRel, AddAction.orbitRel, Algebra.commutes
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
I : Ideal A
inst_7 : I.IsTwoSided
r : R₁
x_1 : A ⧸ I
x : A
⊢ HMul.hMul (α := A ⧸ I) (β := A ⧸ I)
      (((RingHom.comp (mk I) (algebraMap R₁ A) : RingHom.{u_1, u_3} R₁ (A ⧸ I)) : (a : R₁) → A ⧸ I) r : A ⧸ I)
      (Quot.mk (⇑(Submodule.quotientRel I) : A → A → Prop) x) =
    HMul.hMul (α := A ⧸ I) (β := A ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : A → A → Prop) x)
      (((RingHom.comp (mk I) (algebraMap R₁ A) : RingHom.{u_1, u_3} R₁ (A ⧸ I)) : (a : R₁) → A ⧸ I) r : A ⧸ I)

Tactic:
exact congr_arg (⟦·⟧) (Algebra.commutes r x)

Premises used: Quotient.mk, congr_arg, Algebra.commutes
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
inst_7 : SMul R₁ R₂
inst_8 : IsScalarTower R₁ R₂ A
I : Ideal A
⊢ IsScalarTower.{u_1, u_2, u_3} R₁ R₂ (A ⧸ I)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I : Ideal A
inst_3 : I.IsTwoSided
S : Type u_5
inst_4 : Semiring S
inst_5 : Algebra R₁ S
f g : AlgHom.{u_1, u_3, u_5} R₁ (A ⧸ I) S
h : f.comp (mkₐ R₁ I) = g.comp (mkₐ R₁ I)
⊢ f = g

Tactic:
AlgHom.ext fun x => Quotient.inductionOn' x <| AlgHom.congr_fun h

Premises used: Quotient.inductionOn', AlgHom.ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
A : Type u_5
inst_1 : CommRing A
inst_2 : Algebra R₁ A
I : Ideal A
⊢ Eq (α := RingHom.{u_1, u_5} R₁ (A ⧸ I)) (algebraMap R₁ (A ⧸ I))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A (A ⧸ I)) (algebraMap R₁ A))

Tactic:
rfl

Premises used: Ideal.Quotient.mk, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I : Ideal A
inst_3 : I.IsTwoSided
⊢ Eq (α := A →+* A ⧸ I) (AlgHom.toRingHom (mkₐ R₁ I)) (mk I)

Tactic:
rfl

Premises used: Ideal.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I : Ideal A
inst_3 : I.IsTwoSided
⊢ Eq (α := (a : A) → A ⧸ I) (⇑(mkₐ R₁ I) : (a : A) → A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
⊢ Eq (α := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) (mk I)

Tactic:
rfl

Premises used: Ideal.Quotient.mk, Submodule.Quotient.mk, rfl