awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Surjective (α := R ⊗[R] M) (β := ((i : ι) → R ⧸ I i) ⊗[R] M)
    (⇑((↑(LinearEquiv.symm (piLeft R M fun (i : ι) ↦ R ⧸ I i)) :
            ((i : ι) → (R ⧸ I i) ⊗[R] M) →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M) ∘ₗ
          (LinearMap.pi (φ := fun (i : ι) ↦ (R ⧸ I i) ⊗[R] M) fun (i : ι) ↦
              (TensorProduct.mk R (R ⧸ I i) M : (a : R ⧸ I i) → M →ₗ[R] (R ⧸ I i) ⊗[R] M) 1) ∘ₗ
            (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M)) :
      (a : R ⊗[R] M) → ((i : ι) → R ⧸ I i) ⊗[R] M)
⊢ Surjective (α := M) (β := (i : ι) → (R ⧸ I i) ⊗[R] M)
    (⇑(LinearMap.pi (φ := fun (i : ι) ↦ (R ⧸ I i) ⊗[R] M) fun (i : ι) ↦
          (TensorProduct.mk R (R ⧸ I i) M : (a : R ⧸ I i) → M →ₗ[R] (R ⧸ I i) ⊗[R] M) 1) :
      (a : M) → (i : ι) → (R ⧸ I i) ⊗[R] M)

Tactic:
simpa using this
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
⊢ Exact (M :=
    ↥(ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
      M)
    (N := R ⊗[R] M) (P := ((i : ι) → R ⧸ I i) ⊗[R] M)
    (⇑(rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))) :
      (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker ⊗[R] M) → R ⊗[R] M)
    (⇑(rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) :
      (a : R ⊗[R] M) → ((i : ι) → R ⧸ I i) ⊗[R] M)

Tactic:
have := rTensor_exact M (exact_subtype_ker_map _) (pi_mkQ_surjective hI)
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Exact (M :=
    ↥(ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
      M)
    (N := R ⊗[R] M) (P := ((i : ι) → R ⧸ I i) ⊗[R] M)
    (⇑(rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))) :
      (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker ⊗[R] M) → R ⊗[R] M)
    (⇑(rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) :
      (a : R ⊗[R] M) → ((i : ι) → R ⧸ I i) ⊗[R] M)
⊢ Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))

Tactic:
rw [← (TensorProduct.lid R M).conj_exact_iff_exact, exact_iff] at this

Premises used: LinearEquiv.conj_exact_iff_exact, TensorProduct.lid, LinearMap.exact_iff
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))
⊢ Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))

Tactic:
this
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))
h :
  Eq (α := Submodule R M)
    (ker (M₂ := (i : ι) → (R ⧸ I i) ⊗[R] M)
      (LinearMap.pi (φ := fun (i : ι) ↦ (R ⧸ I i) ⊗[R] M) fun (i : ι) ↦
        (TensorProduct.mk R (R ⧸ I i) M : (a : R ⧸ I i) → M →ₗ[R] (R ⧸ I i) ⊗[R] M) 1))
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
h₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤ =
    range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))))
⊢ ker (M₂ := (i : ι) → (R ⧸ I i) ⊗[R] M)
      (LinearMap.pi (φ := fun (i : ι) ↦ (R ⧸ I i) ⊗[R] M) fun (i : ι) ↦
        (TensorProduct.mk R (R ⧸ I i) M : (a : R ⧸ I i) → M →ₗ[R] (R ⧸ I i) ⊗[R] M) 1) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤

Tactic:
convert! this
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))
⊢ Eq (α := Submodule R M)
    (ker (M₂ := (i : ι) → (R ⧸ I i) ⊗[R] M)
      (LinearMap.pi (φ := fun (i : ι) ↦ (R ⧸ I i) ⊗[R] M) fun (i : ι) ↦
        (TensorProduct.mk R (R ⧸ I i) M : (a : R ⧸ I i) → M →ₗ[R] (R ⧸ I i) ⊗[R] M) 1))
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))

Tactic:
simp [pi_mkQ_rTensor, LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc, Ideal.pi_mkQ_rTensor
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤ =
    range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))))

Tactic:
le_antisymm (Submodule.smul_le.mpr fun r hr m _ ↦ ⟨⟨r, ?_⟩ ⊗ₜ m, rfl⟩) ?_

Premises used: Iff.mpr, Subtype.mk, le_antisymm, Exists.intro, Submodule.smul_le, TensorProduct.tmul, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))
h :
  ∀ (r : R) (hr : Membership.mem (γ := Submodule R R) (⨅ (i : ι), I i) r) (m : M),
    Membership.mem (γ := Submodule R M) ⊤ m →
      Membership.mem (γ := Submodule R R)
        (ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) r
h₁ :
  range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))) ≤
    HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤ =
    range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))))

Tactic:
refine le_antisymm (Submodule.smul_le.mpr fun r hr m _ ↦ ⟨⟨r, ?_⟩ ⊗ₜ m, rfl⟩) ?_
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))
r : R
hr : Membership.mem (γ := Submodule R R) (⨅ (i : ι), I i) r
m : M
h : Membership.mem (γ := Submodule R M) ⊤ m
⊢ Membership.mem (γ := Submodule R R)
    (ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) r

Tactic:
simpa only [ker_pi, Submodule.ker_mkQ]

Premises used: LinearMap.ker_pi, Submodule.ker_mkQ
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))
x :
  ↥(ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R] M
⊢ Membership.mem (α := M) (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤)
    (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
            rTensor M
              (Submodule.subtype
                (ker (M₂ := (i : ι) → R ⧸ I i)
                  (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))) :
          (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker ⊗[R] M) → M)
        0 :
      M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))
x :
  ↥(ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R] M
r : ↥(ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))
m : M
⊢ Membership.mem (α := R) (γ := Submodule R R) (⨅ (i : ι), I i)
    (((Submodule.subtype
                (ker (M₂ := (i : ι) → R ⧸ I i)
                  (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) :
              (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker) → R)
            (r, m).1,
          (LinearMap.id : (a : M) → M) (r, m).2).1 :
      R)

Tactic:
simpa only [← (I _).ker_mkQ, ← ker_pi] using Subtype.mem _

Premises used: LinearMap.ker_pi, Subtype.mem, Submodule.ker_mkQ
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))
x x_1 x_2 :
  ↥(ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R] M
⊢ Membership.mem (α := M) (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤)
      (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
              rTensor M
                (Submodule.subtype
                  (ker (M₂ := (i : ι) → R ⧸ I i)
                    (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))) :
            (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker ⊗[R] M) → M)
          x_1 :
        M) →
    Membership.mem (α := M) (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤)
        (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
                rTensor M
                  (Submodule.subtype
                    (ker (M₂ := (i : ι) → R ⧸ I i)
                      (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))) :
              (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker ⊗[R] M) → M)
            x_2 :
          M) →
      Membership.mem (α := M) (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤)
        (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
                rTensor M
                  (Submodule.subtype
                    (ker (M₂ := (i : ι) → R ⧸ I i)
                      (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))) :
              (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker ⊗[R] M) → M)
            (x_1 + x_2) :
          M)

Tactic:
simpa using add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I_1 J : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
inst_1 : I.IsTwoSided
a₁ b₁ a₂ b₂ : R
h₁ : ((QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid : R → R → Prop) a₁ b₁
h₂ : ((QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid : R → R → Prop) a₂ b₂
rw : ∀ (h₁ : a₁ - b₁ ∈ I) (h₂ : a₂ - b₂ ∈ I), a₁ * a₂ - b₁ * b₂ ∈ I
⊢ ((QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid : R → R → Prop) (a₁ * a₂) (b₁ * b₂)

Tactic:
rw [Submodule.quotientRel_def] at h₁ h₂ ⊢

Premises used: Submodule.quotientRel_def
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I_1 J : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
inst_1 : I.IsTwoSided
a₁ b₁ a₂ b₂ : R
h₁ : a₁ - b₁ ∈ I
h₂ : a₂ - b₂ ∈ I
⊢ a₁ * a₂ - b₁ * b₂ ∈ I

Tactic:
mul_sub_mul_mem I h₁ h₂

Premises used: Set.Mem, Ideal.mul_sub_mul_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I_1 J : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
inst_1 : I.IsTwoSided
a₁ b₁ a₂ b₂ : R
h₁ : a₁ - b₁ ∈ I
h₂ : a₂ - b₂ ∈ I
⊢ a₁ * a₂ - b₁ * b₂ ∈ I

Tactic:
exact mul_sub_mul_mem I h₁ h₂

Premises used: Ideal.mul_sub_mul_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R_1 : Type u
inst : Ring R_1
I_1 J : Ideal R_1
a_1 b_1 : R_1
S : Type v
x y : R_1
R : Type u_1
inst_1 : CommRing R
I : Ideal R
a_2 : R ⧸ I
a : R
b_2 : R ⧸ I
b : R
⊢ HMul.hMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b) =
    HMul.hMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)

Tactic:
congr_arg _ (mul_comm a b)

Premises used: Quotient.map₂, congr_arg, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R_1 : Type u
inst : Ring R_1
I_1 J : Ideal R_1
a_1 b_1 : R_1
S : Type v
x y : R_1
R : Type u_1
inst_1 : CommRing R
I : Ideal R
a_2 : R ⧸ I
a : R
b_2 : R ⧸ I
b : R
⊢ HMul.hMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b) =
    HMul.hMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)

Tactic:
exact congr_arg _ (mul_comm a b)

Premises used: congr_arg, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I J : Ideal R
a b : R
S : Type v
x y : R
inst_1 : I.IsTwoSided
⊢ Eq.{u + 1} (α := AddCommGroup (R ⧸ I)) Ring.toAddCommGroup (Submodule.Quotient.addCommGroup I)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I J : Ideal R
a b : R
S : Type v
x y : R
inst_1 : I.IsTwoSided
⊢ Eq.{u + 1} (α := AddCommGroup (R ⧸ I)) Ring.toAddCommGroup (Submodule.Quotient.addCommGroup I)

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
S : Type v
inst_1 : I.IsTwoSided
inst_2 : NonAssocSemiring S
f g : RingHom.{u, v} (R ⧸ I) S
h : f.comp (mk I) = g.comp (mk I)
⊢ f = g

Tactic:
RingHom.ext fun x => Quotient.inductionOn' x <| (RingHom.congr_fun h :)

Premises used: Quotient.inductionOn', RingHom.ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I J : Ideal R
a b : R
S : Type v
x y : R
inst_1 : I.IsTwoSided
⊢ Nonempty.{u + 1} (R ⧸ I)

Tactic:
⟨mk I 37⟩

Premises used: Ideal.Quotient.mk, Nonempty.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
x y : R
inst_1 : I.IsTwoSided
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔ x - y ∈ I

Tactic:
Submodule.Quotient.eq I

Premises used: Submodule.Quotient.eq, Set.Mem, Submodule.Quotient.mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
⊢ Eq (α := R ⧸ I) (Submodule.Quotient.mk x) ((mk I : (a : R) → R ⧸ I) x)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Defs
Goal:
R : Type u
inst : Ring R
I : Ideal R
a : R
inst_1 : I.IsTwoSided
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) (0 : R ⧸ I) ↔ a ∈ I

Tactic:
Submodule.Quotient.mk_eq_zero _

Premises used: Set.Mem, Submodule.Quotient.mk, Submodule.Quotient.mk_eq_zero