awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (hypothesis)
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)
    (⇑(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)
⊢ 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)
have 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)
Tactic: classical rw [pi_mkQ_rTensor] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (hypothesis)
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 ι
⊢ 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) ⊤
have 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)
Tactic: have := rTensor_exact M (exact_subtype_ker_map _) (pi_mkQ_surjective hI)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (hypothesis)
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)
⊢ 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) ⊤
have 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))))))
Tactic: rw [← (TensorProduct.lid R M).conj_exact_iff_exact, exact_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (goal)
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))))))
⊢ 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) ⊤
have 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)))
Tactic: convert! this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (goal)
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)))
⊢ 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) ⊤
have 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)))))
Tactic: convert! this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (goal)
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)))))
have 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
Tactic: refine le_antisymm (Submodule.smul_le.mpr fun r hr m _ ↦ ⟨⟨r, ?_⟩ ⊗ₜ m, rfl⟩) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (goal)
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
⊢ 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)))))
have 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) ⊤
Tactic: refine le_antisymm (Submodule.smul_le.mpr fun r hr m _ ↦ ⟨⟨r, ?_⟩ ⊗ₜ m, rfl⟩) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (goal)
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)
        x :
      M)
have h : ∀ (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: refine x.induction_on (by simp) (fun r m ↦ Submodule.smul_mem_smul ?_ ⟨⟩) fun _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
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₂
⊢ ((QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid : R → R → Prop) (a₁ * a₂) (b₁ * b₂)
have rw : ∀ (h₁ : a₁ - b₁ ∈ I) (h₂ : a₂ - b₂ ∈ I), a₁ * a₂ - b₁ * b₂ ∈ I
Tactic: rw [Submodule.quotientRel_def] at h₁ h₂ ⊢
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x y : R
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔ x - y ∈ I
have rw : Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) (x - y) : R ⧸ I) (0 : R ⧸ I)
Tactic: rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x y : R
rw :
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) (x - y) : R ⧸ I) (0 : R ⧸ I)
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔ x - y ∈ I
have rw₁ : Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔
  HSub.hSub (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) = 0
Tactic: rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x y : R
rw :
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) (x - y) : R ⧸ I) (0 : R ⧸ I)
rw₁ :
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔
    HSub.hSub (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) = 0
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔ x - y ∈ I
have rw₂ : Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) ↔
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I)
Tactic: rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (1 : R ⧸ I) ↔ x - 1 ∈ I
have rw : Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (1 : R ⧸ I) ↔
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) 1 : R ⧸ I)
Tactic: rw [← mk_eq_mk_iff_sub_mem, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
rw :
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (1 : R ⧸ I) ↔
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) 1 : R ⧸ I)
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (1 : R ⧸ I) ↔ x - 1 ∈ I
have rw₁ : Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (1 : R ⧸ I) ↔
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (1 : R ⧸ I)
Tactic: rw [← mk_eq_mk_iff_sub_mem, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
s : Set R
⊢ Eq (α := Set R) (preimage (β := R ⧸ I) (⇑(mk I) : (a : R) → R ⧸ I) ((⇑(mk I) : (a : R) → R ⧸ I) '' s))
    (⋃ (x : ↥I), (fun (y : R) ↦ (↑x : R) + y) '' s)
have h : ∀ (x : R),
  Membership.mem (γ := Set R) (preimage (β := R ⧸ I) (⇑(mk I) : (a : R) → R ⧸ I) ((⇑(mk I) : (a : R) → R ⧸ I) '' s)) x ↔
    Membership.mem (γ := Set R) (⋃ (x : ↥I), (fun (y : R) ↦ (↑x : R) + y) '' s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
s : Set R
x : R
⊢ Membership.mem (γ := Set R) (preimage (β := R ⧸ I) (⇑(mk I) : (a : R) → R ⧸ I) ((⇑(mk I) : (a : R) → R ⧸ I) '' s)) x ↔
    Membership.mem (γ := Set R) (⋃ (x : ↥I), (fun (y : R) ↦ (↑x : R) + y) '' s) x
have h : (∃ x_1 ∈ s, x_1 - x ∈ I) ↔ ∃ (i : ↥I), ∃ x_1 ∈ s, (↑i : R) + x_1 = x
Tactic: simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
s : Set R
x : R
h : ∃ (i : ↥I), ∃ x_1 ∈ s, (↑i : R) + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R) + a = x
⊢ a - x ∈ I
have rw : -(↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R) ∈ I
Tactic: rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
S : Type v
inst_1 : I.IsTwoSided
inst_2 : Semiring S
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
y : S
⊢ ∃ (a : R ⧸ I), (lift I f H : (a : R ⧸ I) → S) a = y
have obtain : ∀ (x : R), ∃ (a : R ⧸ I), Eq.{v + 1} (α := S) ((lift I f H : (a : R ⧸ I) → S) a : S) ((f : (a : R) → S) x : S)
Tactic: obtain ⟨x, rfl⟩ := hf y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
S : Type v
inst_1 : I.IsTwoSided
inst_2 : Semiring S
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
⊢ ∃ (a : R ⧸ I), Eq.{v + 1} (α := S) ((lift I f H : (a : R ⧸ I) → S) a : S) ((f : (a : R) → S) x : S)
have h : Eq.{v + 1} (α := S) ((lift I f H : (a : R ⧸ I) → S) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) : S) ((f : (a : R) → S) x : S)
Tactic: use Ideal.Quotient.mk I x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
S : Ideal R
inst_1 : S.IsTwoSided
⊢ Eq (α := R ⧸ S →+* R ⧸ S) (factor ⋯) (RingHom.id (R ⧸ S))
have h : ∀ (x : R),
  Eq (α := R ⧸ S) ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor sorry) (mk S) : (a : R) → R ⧸ S) x : R ⧸ S)
    ((RingHom.comp (RingHom.id (R ⧸ S)) (mk S) : (a : R) → R ⧸ S) x : R ⧸ S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
S T : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
H : S ≤ T
⊢ Eq (α := R →+* R ⧸ T) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H) (mk S)) (mk T)
have a : ∀ (x : R),
  Eq (α := R ⧸ T) ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H) (mk S) : (a : R) → R ⧸ T) x : R ⧸ T)
    ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
S T : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
H : S ≤ T
x : R
⊢ Eq (α := R ⧸ T) ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H) (mk S) : (a : R) → R ⧸ T) x : R ⧸ T)
    ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)
have a : Eq (α := R ⧸ T) ((factor H : (a : R ⧸ S) → R ⧸ T) ((mk S : (a : R) → R ⧸ S) x) : R ⧸ T)
  ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)
Tactic: rw [RingHom.comp_apply, factor_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
S T : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
H : S ≤ T
x : R
a :
  Eq (α := R ⧸ T) ((factor H : (a : R ⧸ S) → R ⧸ T) ((mk S : (a : R) → R ⧸ S) x) : R ⧸ T)
    ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)
⊢ Eq (α := R ⧸ T) ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H) (mk S) : (a : R) → R ⧸ T) x : R ⧸ T)
    ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)
have a₁ : Eq (α := R ⧸ T) ((mk T : (a : R) → R ⧸ T) x : R ⧸ T) ((mk T : (a : R) → R ⧸ T) x : R ⧸ T)
Tactic: rw [RingHom.comp_apply, factor_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
S T U : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
inst_3 : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
⊢ Eq (α := R ⧸ S →+* R ⧸ U) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H2) (factor H1)) (factor ⋯)
have h : ∀ (x : R),
  Eq (α := R ⧸ U)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H2) (factor H1)) (mk S) :
          (a : R) → R ⧸ U)
        x :
      R ⧸ U)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor sorry) (mk S) : (a : R) → R ⧸ U) x : R ⧸ U)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Defs (goal)
Goal:
R : Type u
inst : Ring R
S T U : Ideal R
inst_1 : S.IsTwoSided
inst_2 : T.IsTwoSided
inst_3 : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R ⧸ S
⊢ Eq (α := R ⧸ U) ((factor H2 : (a : R ⧸ T) → R ⧸ U) ((factor H1 : (a : R ⧸ S) → R ⧸ T) x) : R ⧸ U)
    ((factor ⋯ : (a : R ⧸ S) → R ⧸ U) x : R ⧸ U)
have rw : Eq (α := R ⧸ U)
  ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor H2) (factor H1) : (a : R ⧸ S) → R ⧸ U) x : R ⧸ U)
  ((factor sorry : (a : R ⧸ S) → R ⧸ U) x : R ⧸ U)
Tactic: rw [← RingHom.comp_apply]