awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
x y : R
rw : Membership.mem (γ := Ideal R) (span {x}) y ↔ x ∣ y
rw₁ rw₂ : x ∣ y ↔ x ∣ y
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {x}))
      ((mk (span {x}) : (a : R) → R ⧸ span {x}) y : HasQuotient.Quotient R (B := Ideal R) (span {x}))
      (0 : HasQuotient.Quotient R (B := Ideal R) (span {x})) ↔
    x ∣ y

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]

Premises used: Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
x : R
inst_1 : IsTwoSided (α := R) (span {x})
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {x}))
    ((mk (span {x}) : (a : R) → R ⧸ span {x}) x : HasQuotient.Quotient R (B := Ideal R) (span {x}))
    (0 : HasQuotient.Quotient R (B := Ideal R) (span {x}))

Tactic:
(Submodule.Quotient.mk_eq_zero _).mpr (mem_span_singleton_self _)

Premises used: Iff.mpr, Submodule.Quotient.mk, Ideal.mem_span_singleton_self, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b x y : R
inst_1 : I.IsTwoSided
hI : I.IsPrime
⊢ IsDomain.{u_3} (R ⧸ I)

Tactic:
let _ := Quotient.nontrivial_iff.mpr hI.1
  NoZeroDivisors.to_isDomain _

Premises used: Iff.mpr, Ideal.Quotient.nontrivial_iff, HasQuotient.Quotient, Ideal.IsPrime.ne_top', NoZeroDivisors.to_isDomain
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ IsDomain.{u_3} (R ⧸ I) ↔ I.IsPrime

Tactic:
⟨fun H => ⟨zero_ne_one_iff.1 ?_, fun {x y} h => ?_⟩, fun h => inferInstance⟩

Premises used: inferInstance, Iff.intro, Iff.mp, Ideal.IsPrime.mk, Ideal.Quotient.zero_ne_one_iff
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
refine_1 : ∀ (H : IsDomain.{u_3} (R ⧸ I)), Ne.{u_3 + 1} (α := R ⧸ I) 0 1
refine_2 : ∀ (H : IsDomain.{u_3} (R ⧸ I)) {x y : R} (h : x * y ∈ I), x ∈ I ∨ y ∈ I
⊢ IsDomain.{u_3} (R ⧸ I) ↔ I.IsPrime

Tactic:
refine ⟨fun H => ⟨zero_ne_one_iff.1 ?_, fun {x y} h => ?_⟩, fun h => inferInstance⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
H : IsDomain.{u_3} (R ⧸ I)
⊢ Nontrivial.{u_3} (R ⧸ I)

Tactic:
haveI : Nontrivial (R ⧸ I) := ⟨H.2.1⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
H : IsDomain.{u_3} (R ⧸ I)
this : Nontrivial.{u_3} (R ⧸ I)
⊢ Ne.{u_3 + 1} (α := R ⧸ I) 0 1

Tactic:
zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
H : IsDomain.{u_3} (R ⧸ I)
this : Nontrivial.{u_3} (R ⧸ I)
⊢ Ne.{u_3 + 1} (α := R ⧸ I) 0 1

Tactic:
exact zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
H : IsDomain.{u_3} (R ⧸ I)
x y : R
h : x * y ∈ I
refine_2 :
  ∀
    (h :
      HMul.hMul (α := 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) (0 : R ⧸ I) ∨
      Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) (0 : R ⧸ I)
⊢ x ∈ I ∨ y ∈ I

Tactic:
simp only [← eq_zero_iff_mem, (mk I).map_mul] at h ⊢

Premises used: Ideal.Quotient.mk, Ideal.Quotient.eq_zero_iff_mem, RingHom.map_mul
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
H : IsDomain.{u_3} (R ⧸ I)
x y : R
h : HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) = 0
⊢ NoZeroDivisors.{u_3} (R ⧸ I)

Tactic:
haveI := @IsDomain.to_noZeroDivisors (R ⧸ I) _ H
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
H : IsDomain.{u_3} (R ⧸ I)
x y : R
h : HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) = 0
this : NoZeroDivisors.{u_3} (R ⧸ I)
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I) ∨
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) (0 : R ⧸ I)

Tactic:
eq_zero_or_eq_zero_of_mul_eq_zero h

Premises used: NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
H : IsDomain.{u_3} (R ⧸ I)
x y : R
h : HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) = 0
this : NoZeroDivisors.{u_3} (R ⧸ I)
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I) ∨
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) (0 : R ⧸ I)

Tactic:
exact eq_zero_or_eq_zero_of_mul_eq_zero h

Premises used: NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
h : ∀ (a : R ⧸ I), a ≠ 0 → ∃ (b : R ⧸ I), b * a = 1
⊢ ∀ {a : R ⧸ I}, a ≠ 0 → ∃ (b : R ⧸ I), a * b = 1

Tactic:
apply exists_right_inv_of_exists_left_inv

Premises used: exists_right_inv_of_exists_left_inv
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
h₁ :
  ∀ (b c : R) (hc : c ∈ I) (abc : b * a + c = 1),
    ∃ (b : R ⧸ I), b * Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a = 1
⊢ ∃ (b : R ⧸ I), b * Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a = 1

Tactic:
rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩

Premises used: Iff.mpr, mt, Ideal.Quotient.eq_zero_iff_mem, Ideal.IsMaximal.exists_inv
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ ∃ (b : R ⧸ I), b * Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a = 1

Tactic:
⟨mk _ b, Quot.sound ?_⟩

Premises used: Quot.sound, Ideal.Quotient.mk, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
h₁ : ((Quotient.ringCon I).toSetoid : R → R → Prop) ((fun (x1 x2 : R) ↦ x1 * x2) b a) 1
⊢ ∃ (b : R ⧸ I), b * Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a = 1

Tactic:
refine ⟨mk _ b, Quot.sound ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
h₁ : b * a - 1 ∈ I
⊢ ((Quotient.ringCon I).toSetoid : R → R → Prop) ((fun (x1 x2 : R) ↦ x1 * x2) b a) 1

Tactic:
simp only [Submodule.quotientRel_def]

Premises used: Submodule.quotientRel_def
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ c = 1 - b * a

Tactic:
rw [← eq_sub_iff_add_eq'] at abc

Premises used: eq_sub_iff_add_eq'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : c = 1 - b * a
h₁ : ∀ (hc : 1 - b * a ∈ I) (abc : c = 1 - b * a), b * a - 1 ∈ I
h₂ : ∀ (hc : -(1 - b * a) ∈ I) (abc : c = 1 - b * a), b * a - 1 ∈ I
h₃ h₄ h₅ h₆ : ∀ (hc : b * a - 1 ∈ I) (abc : c = 1 - b * a), b * a - 1 ∈ I
⊢ b * a - 1 ∈ I

Tactic:
rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc

Premises used: neg_mem_iff, neg_sub
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b x y : R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a : R ⧸ I
ha : a ≠ 0
rw : a * choose (p := fun (x : R ⧸ I) ↦ a * x = 1) ⋯ = 1
⊢ (a * if ha : a = 0 then 0 else choose (p := fun (x : R ⧸ I) ↦ a * x = 1) ⋯) = 1

Tactic:
rw [dif_neg ha]

Premises used: dif_neg
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b x y : R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a : R ⧸ I
ha : a ≠ 0
⊢ a * choose (p := fun (x : R ⧸ I) ↦ a * x = 1) ⋯ = 1

Tactic:
Classical.choose_spec (exists_inv ha)

Premises used: Ideal.Quotient.exists_inv, Classical.choose_spec
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b x y : R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a : R ⧸ I
ha : a ≠ 0
⊢ a * choose (p := fun (x : R ⧸ I) ↦ a * x = 1) ⋯ = 1

Tactic:
exact Classical.choose_spec (exists_inv ha)

Premises used: Ideal.Quotient.exists_inv, Classical.choose_spec
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
apply : 1 ∉ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ I.IsMaximal

Tactic:
apply Ideal.isMaximal_iff.2

Premises used: Iff.mpr, Ideal.isMaximal_iff
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
left : 1 ∉ I
right : ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ 1 ∉ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
h : 1 ∈ I
left :
  ∀ (w : R ⧸ I) (x : R) (w : R ⧸ I) (y : R)
    (hxy :
      Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x)
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y)),
    False
⊢ False

Tactic:
rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩

Premises used: IsField.exists_pair_ne
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
h : 1 ∈ I
w : R ⧸ I
x : R
w_1 : R ⧸ I
y : R
hxy :
  Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x)
    (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y)
⊢ False

Tactic:
hxy (Ideal.Quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h))

Premises used: Iff.mpr, HSub.hSub, Eq.rec, Ideal.Quotient.eq, mul_one, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
h : 1 ∈ I
w : R ⧸ I
x : R
w_1 : R ⧸ I
y : R
hxy :
  Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x)
    (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y)
⊢ False

Tactic:
exact hxy (Ideal.Quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h))

Premises used: Iff.mpr, HSub.hSub, Eq.rec, Ideal.Quotient.eq, mul_one, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
right :
  ∀ (w : R ⧸ I) (y : R)
    (hy :
      HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I)
          (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y) =
        1),
    1 ∈ J
⊢ 1 ∈ J

Tactic:
rcases hqf.mul_inv_cancel (mt Ideal.Quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩

Premises used: mt, Ideal.Quotient.eq_zero_iff_mem, Iff.mp, IsField.mul_inv_cancel
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w : R ⧸ I
y : R
hy :
  HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y) =
    1
right : x * y - (x * y - 1) ∈ J
⊢ 1 ∈ J

Tactic:
rw [← zero_add (1 : R), ← sub_self (x * y), sub_add]

Premises used: sub_add, HMul.hMul, sub_self, zero_add, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w : R ⧸ I
y : R
hy :
  HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y) =
    1
⊢ x * y - (x * y - 1) ∈ J

Tactic:
J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (Ideal.Quotient.eq.1 hy))

Premises used: Set.Mem, Ideal.Quotient.eq, Ideal.mul_mem_right, Iff.mp, Ideal.sub_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w : R ⧸ I
y : R
hy :
  HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y) =
    1
⊢ x * y - (x * y - 1) ∈ J

Tactic:
exact J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (Ideal.Quotient.eq.1 hy))

Premises used: Ideal.Quotient.eq, Ideal.mul_mem_right, Iff.mp, Ideal.sub_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
⊢ I.IsMaximal ↔ IsField.{u_5} (R ⧸ I)

Tactic:
⟨fun h =>
    let _i := @Quotient.field _ _ I h
    Field.toIsField _,
    maximal_of_isField _⟩

Premises used: Field.toIsField, Ideal.Quotient.field, HasQuotient.Quotient, Iff.intro, Ideal.Quotient.maximal_of_isField
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b : R
inst_1 : I.IsTwoSided
c : R ⧸ I
m : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c₁ : R
m₁ : (i : ι) → R
c₂ : R
m₂ : (i : ι) → R
hc : (Submodule.quotientRel I : R → R → Prop) c₁ c₂
hm : (Submodule.quotientRel (pi fun (x : ι) ↦ I) : ((i : ι) → R) → ((i : ι) → R) → Prop) m₁ m₂
apply : Membership.mem (γ := Ideal (ι → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) (c₁ • m₁ - c₂ • m₂)
⊢ Eq (α := HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
    ((fun (r : R) (m : (i : ι) → R) ↦
        (Submodule.Quotient.mk (r • m) :
          HasQuotient.Quotient (ι → R) (B := Submodule ((i : ι) → R) (ι → R))
            (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)))
      c₁ m₁)
    ((fun (r : R) (m : (i : ι) → R) ↦
        (Submodule.Quotient.mk (r • m) :
          HasQuotient.Quotient (ι → R) (B := Submodule ((i : ι) → R) (ι → R))
            (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)))
      c₂ m₂)

Tactic:
apply Ideal.Quotient.eq.2

Premises used: Iff.mpr, Ideal.Quotient.eq
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b : R
inst_1 : I.IsTwoSided
c : R ⧸ I
m : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c₁ : R
m₁ : (i : ι) → R
c₂ : R
m₂ : (i : ι) → R
hc : (Submodule.quotientRel I : R → R → Prop) c₁ c₂
hm : (Submodule.quotientRel (pi fun (x : ι) ↦ I) : ((i : ι) → R) → ((i : ι) → R) → Prop) m₁ m₂
⊢ c₁ - c₂ ∈ I

Tactic:
rw [Submodule.quotientRel_def] at hc hm

Premises used: Submodule.quotientRel_def
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b : R
inst_1 : I.IsTwoSided
c : R ⧸ I
m : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c₁ : R
m₁ : (i : ι) → R
c₂ : R
m₂ : (i : ι) → R
hc : (Submodule.quotientRel I : R → R → Prop) c₁ c₂
hm : (Submodule.quotientRel (pi fun (x : ι) ↦ I) : ((i : ι) → R) → ((i : ι) → R) → Prop) m₁ m₂
hc₁ : c₁ - c₂ ∈ I
⊢ Membership.mem (γ := Submodule ((i : ι) → R) ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) (m₁ - m₂)

Tactic:
rw [Submodule.quotientRel_def] at hc hm

Premises used: Submodule.quotientRel_def
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b : R
inst_1 : I.IsTwoSided
c : R ⧸ I
m : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c₁ : R
m₁ : (i : ι) → R
c₂ : R
m₂ : (i : ι) → R
hc : c₁ - c₂ ∈ I
hm : Membership.mem (γ := Submodule ((i : ι) → R) ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) (m₁ - m₂)
i : ι
⊢ Membership.mem (γ := Ideal ((fun (x : ι) ↦ R) i)) ((fun (x : ι) ↦ I) i) ((c₁ • m₁ - c₂ • m₂) i)

Tactic:
I.mul_sub_mul_mem hc (hm i)

Premises used: Set.Mem, Ideal.mul_sub_mul_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b : R
inst_1 : I.IsTwoSided
c : R ⧸ I
m : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c₁ : R
m₁ : (i : ι) → R
c₂ : R
m₂ : (i : ι) → R
hc : c₁ - c₂ ∈ I
hm : Membership.mem (γ := Submodule ((i : ι) → R) ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) (m₁ - m₂)
i : ι
⊢ Membership.mem (γ := Ideal ((fun (x : ι) ↦ R) i)) ((fun (x : ι) ↦ I) i) ((c₁ • m₁ - c₂ • m₂) i)

Tactic:
exact I.mul_sub_mul_mem hc (hm i)

Premises used: Ideal.mul_sub_mul_mem
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b_1 : R
inst_1 : I.IsTwoSided
x : R ⧸ I
a : R
y : R ⧸ I
b : R
b_2 : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c : (i : ι) → R
⊢ HSMul.hSMul (β := HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
      (HMul.hMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b))
      (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c) =
    HSMul.hSMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
      (HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c))

Tactic:
congr_arg _ (mul_smul _ _ _)

Premises used: Submodule.Quotient.mk, congr_arg, SemigroupAction.mul_smul, Quotient.liftOn₂'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b_1 : R
inst_1 : I.IsTwoSided
x : R ⧸ I
a : R
y : R ⧸ I
b : R
b_2 : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c : (i : ι) → R
⊢ HSMul.hSMul (β := HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
      (HMul.hMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b))
      (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c) =
    HSMul.hSMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
      (HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c))

Tactic:
exact congr_arg _ (mul_smul _ _ _)

Premises used: congr_arg, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b : R
inst_1 : I.IsTwoSided
b_1 : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
a : (i : ι) → R
⊢ HSMul.hSMul (α := R ⧸ I) (β :=
      HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)) 1
      (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a) =
    Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a

Tactic:
congr_arg _ (one_smul _ _)

Premises used: Submodule.Quotient.mk, one_smul, congr_arg, Quotient.liftOn₂'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b : R
inst_1 : I.IsTwoSided
b_1 : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
a : (i : ι) → R
⊢ HSMul.hSMul (α := R ⧸ I) (β :=
      HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)) 1
      (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a) =
    Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a

Tactic:
exact congr_arg _ (one_smul _ _)

Premises used: one_smul, congr_arg
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b : R
inst_1 : I.IsTwoSided
a_2 : R ⧸ I
a : R
⊢ HSMul.hSMul (α := R ⧸ I) (β :=
      HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0 =
    0

Tactic:
congr_arg _ (smul_zero _)

Premises used: Submodule.Quotient.mk, smul_zero, congr_arg, Quotient.liftOn₂'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b : R
inst_1 : I.IsTwoSided
a_2 : R ⧸ I
a : R
⊢ HSMul.hSMul (α := R ⧸ I) (β :=
      HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0 =
    0

Tactic:
exact congr_arg _ (smul_zero _)

Premises used: smul_zero, congr_arg