awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsMaximal
x : S
inst_4 : IsDedekindDomain R
inst_5 : IsDomain S
inst_6 : IsTorsionFree R S
inst_7 : Module.Finite R S
inst_8 : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
this_1 : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R Rₚ Sₚ
this_3 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) p.primeCompl) Sₚ
e : LE.le (α := Submonoid S) (algebraMapSubmonoid S p.primeCompl) S⁰
this_4 : IsDomain Sₚ
this_5 : IsTorsionFree Rₚ Sₚ
this_6 : Module.Finite Rₚ Sₚ
this_7 : IsIntegrallyClosed Sₚ
this_8 : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ Eq (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) : (a : R) → Rₚ ⧸ maximalIdeal Rₚ)
        ((intTrace R S : (a : S) → R) x) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((equivQuotMaximalIdeal p Rₚ : (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((intTrace R S : (a : S) → R) x)) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))

Tactic:
simp only [equivQuotMaximalIdeal, RingHom.quotientKerEquivOfSurjective, RingEquiv.coe_trans,
    Function.comp_apply, Ideal.quotEquivOfEq_mk, RingHom.quotientKerEquivOfRightInverse.apply,
    RingHom.kerLift_mk]

Premises used: Ideal.quotEquivOfEq_mk, RingHom.quotientKerEquivOfSurjective, Function.comp_apply, RingHom.quotientKerEquivOfRightInverse.apply, RingEquiv.coe_trans, RingHom.kerLift_mk, IsLocalization.AtPrime.equivQuotMaximalIdeal
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
inst_1 : Nontrivial R
⊢ Nontrivial.{u_1} (RingCon R)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
inst_1 : Nontrivial R
obtain : ∀ (I J : RingCon R) (h : I ≠ J), Nontrivial.{u_1} (TwoSidedIdeal R)
⊢ Nontrivial.{u_1} (TwoSidedIdeal R)

Tactic:
obtain ⟨I, J, h⟩ : Nontrivial (RingCon R) := inferInstance

Premises used: Nontrivial, RingCon
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 : TwoSidedIdeal R
inst_1 : Nontrivial R
I J : RingCon R
h : I ≠ J
contrapose : ∀ (h : { ringCon := I : TwoSidedIdeal R } = { ringCon := J }), I = J
⊢ { ringCon := I : TwoSidedIdeal R } ≠ { ringCon := J }

Tactic:
contrapose h
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 : TwoSidedIdeal R
inst_1 : Nontrivial R
I J : RingCon R
h : { ringCon := I : TwoSidedIdeal R } = { ringCon := J }
⊢ I = J

Tactic:
aesop
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 : TwoSidedIdeal R
inst_1 : Nontrivial R
I J : RingCon R
h : I ≠ J
⊢ Nontrivial.{u_1} (TwoSidedIdeal R)

Tactic:
exact ⟨⟨I⟩, ⟨J⟩, by contrapose h; aesop⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
e_ringCon : t₁ = t₂
⊢ { ringCon := t₁ : TwoSidedIdeal R } = { ringCon := t₂ }

Tactic:
congr 1
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
⊢ t₁ = t₂

Tactic:
RingCon.ext fun a b ↦ ⟨fun H ↦ ?_, fun H ↦ ?_⟩

Premises used: RingCon.ext, Iff.intro
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
e_ringCon : ∀ (a b : R) (H : (t₁ : (a : R) → R → Prop) a b), (t₂ : (a : R) → R → Prop) a b
e_ringCon₁ : ∀ (a b : R) (H : (t₂ : (a : R) → R → Prop) a b), (t₁ : (a : R) → R → Prop) a b
⊢ t₁ = t₂

Tactic:
refine RingCon.ext fun a b ↦ ⟨fun H ↦ ?_, fun H ↦ ?_⟩

Premises used: RingCon.ext, Iff.intro
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₁ : (a : R) → R → Prop) a b
⊢ Membership.mem (γ := Set R) {x : R | (t₁ : (a : R) → R → Prop) x 0} (a - b)

Tactic:
have H' : a - b ∈ {x | t₁ x 0} := sub_self b ▸ t₁.sub H (t₁.refl b)
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₁ : (a : R) → R → Prop) a b
H' : Membership.mem (γ := Set R) {x : R | (t₁ : (a : R) → R → Prop) x 0} (a - b)
⊢ Membership.mem (γ := Set R) {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)

Tactic:
rw [h] at H'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₁ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
⊢ (t₂ : (a : R) → R → Prop) (a - b + b) (0 + b)

Tactic:
t₂.add H' (t₂.refl b)

Premises used: RingCon.refl, RingCon.add
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₁ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
h₁ : a = a - b + b
h₂ : b = 0 + b
⊢ (t₂ : (a : R) → R → Prop) a b

Tactic:
convert! t₂.add H' (t₂.refl b) using 1

Premises used: RingCon.refl, RingCon.add
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₁ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
⊢ a = a - b + b

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₁ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
⊢ b = 0 + b

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₂ : (a : R) → R → Prop) a b
⊢ Membership.mem (γ := Set R) {x : R | (t₂ : (a : R) → R → Prop) x 0} (a - b)

Tactic:
have H' : a - b ∈ {x | t₂ x 0} := sub_self b ▸ t₂.sub H (t₂.refl b)
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₂ : (a : R) → R → Prop) a b
H' : Membership.mem (γ := Set R) {x : R | (t₂ : (a : R) → R → Prop) x 0} (a - b)
⊢ Membership.mem (γ := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)

Tactic:
rw [← h] at H'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₂ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
⊢ (t₁ : (a : R) → R → Prop) (a - b + b) (0 + b)

Tactic:
t₁.add H' (t₁.refl b)

Premises used: RingCon.refl, RingCon.add
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₂ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
h₁ : a = a - b + b
h₂ : b = 0 + b
⊢ (t₁ : (a : R) → R → Prop) a b

Tactic:
convert! t₁.add H' (t₁.refl b) using 1

Premises used: RingCon.refl, RingCon.add
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₂ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
⊢ a = a - b + b

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₂ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
⊢ b = 0 + b

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x : R
⊢ x ∈ I ↔ (I.ringCon : (a : R) → R → Prop) x 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : R
c : RingCon R
⊢ x ∈ { ringCon := c : TwoSidedIdeal R } ↔ (c : (a : R) → R → Prop) x 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
c : RingCon R
⊢ (↑{ ringCon := c : TwoSidedIdeal R } : Set R) = {x : R | (c : (a : R) → R → Prop) x 0}

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
rw : (I.ringCon : (a : R) → R → Prop) x y ↔ (I.ringCon : (a : R) → R → Prop) (x - y) 0
⊢ (I.ringCon : (a : R) → R → Prop) x y ↔ x - y ∈ I

Tactic:
rw [mem_iff]

Premises used: TwoSidedIdeal.mem_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
mp : (I.ringCon : (a : R) → R → Prop) x y → (I.ringCon : (a : R) → R → Prop) (x - y) 0
mpr : (I.ringCon : (a : R) → R → Prop) (x - y) 0 → (I.ringCon : (a : R) → R → Prop) x y
⊢ (I.ringCon : (a : R) → R → Prop) x y ↔ (I.ringCon : (a : R) → R → Prop) (x - y) 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : (I.ringCon : (a : R) → R → Prop) x y
⊢ (I.ringCon : (a : R) → R → Prop) (x - y) (y - y)

Tactic:
I.ringCon.sub h (I.ringCon.refl y)

Premises used: RingCon.refl, RingCon.sub, TwoSidedIdeal.ringCon
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : (I.ringCon : (a : R) → R → Prop) x y
h₁ : 0 = y - y
⊢ (I.ringCon : (a : R) → R → Prop) (x - y) 0

Tactic:
convert! I.ringCon.sub h (I.ringCon.refl y)

Premises used: RingCon.refl, RingCon.sub, TwoSidedIdeal.ringCon
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : (I.ringCon : (a : R) → R → Prop) x y
⊢ 0 = y - y

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : (I.ringCon : (a : R) → R → Prop) (x - y) 0
⊢ (I.ringCon : (a : R) → R → Prop) (x - y + y) (0 + y)

Tactic:
I.ringCon.add h (I.ringCon.refl y)

Premises used: RingCon.refl, TwoSidedIdeal.ringCon, RingCon.add
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : (I.ringCon : (a : R) → R → Prop) (x - y) 0
h₁ : x = x - y + y
h₂ : y = 0 + y
⊢ (I.ringCon : (a : R) → R → Prop) x y

Tactic:
convert! I.ringCon.add h (I.ringCon.refl y)

Premises used: RingCon.refl, TwoSidedIdeal.ringCon, RingCon.add
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : (I.ringCon : (a : R) → R → Prop) (x - y) 0
⊢ x = x - y + y

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : (I.ringCon : (a : R) → R → Prop) (x - y) 0
⊢ y = 0 + y

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I ≤ J ↔ (↑I : Set R) ⊆ (↑J : Set R)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Subset
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 I J : TwoSidedIdeal R
h : (↑I : Set R) ⊆ (↑J : Set R)
x y : R
r :
  ((({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) I :
        RingCon R) :
      (a : R) → R → Prop)
    x y
rw :
  ∀
    (r :
      Membership.mem (γ := TwoSidedIdeal R)
        {
          ringCon :=
            ({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) I }
        (x - y)),
    Membership.mem (γ := TwoSidedIdeal R)
      {
        ringCon :=
          ({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) J }
      (x - y)
⊢ ((({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) J :
        RingCon R) :
      (a : R) → R → Prop)
    x y

Tactic:
rw [rel_iff] at r ⊢

Premises used: TwoSidedIdeal.rel_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 I J : TwoSidedIdeal R
h : (↑I : Set R) ⊆ (↑J : Set R)
x y : R
r :
  Membership.mem (γ := TwoSidedIdeal R)
    {
      ringCon :=
        ({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) I }
    (x - y)
⊢ Membership.mem (γ := TwoSidedIdeal R)
    {
      ringCon :=
        ({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) J }
    (x - y)

Tactic:
h r

Premises used: Set.Mem, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 I J : TwoSidedIdeal R
h : (↑I : Set R) ⊆ (↑J : Set R)
x y : R
r :
  Membership.mem (γ := TwoSidedIdeal R)
    {
      ringCon :=
        ({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) I }
    (x - y)
⊢ Membership.mem (γ := TwoSidedIdeal R)
    {
      ringCon :=
        ({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) J }
    (x - y)

Tactic:
exact h r
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 I J : TwoSidedIdeal R
h :
  LE.le (α := RingCon R)
    (({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) I :
      RingCon R)
    (({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) J :
      RingCon R)
x : R
hx : x ∈ (↑I : Set R)
rw : ∀ (hx : (I.ringCon : (a : R) → R → Prop) x 0), (J.ringCon : (a : R) → R → Prop) x 0
⊢ x ∈ (↑J : Set R)

Tactic:
rw [SetLike.mem_coe, mem_iff] at hx ⊢

Premises used: TwoSidedIdeal.mem_iff, SetLike.mem_coe
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 I J : TwoSidedIdeal R
h :
  LE.le (α := RingCon R)
    (({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) I :
      RingCon R)
    (({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) J :
      RingCon R)
x : R
hx : (I.ringCon : (a : R) → R → Prop) x 0
⊢ (J.ringCon : (a : R) → R → Prop) x 0

Tactic:
h hx
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 I J : TwoSidedIdeal R
h :
  LE.le (α := RingCon R)
    (({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) I :
      RingCon R)
    (({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) J :
      RingCon R)
x : R
hx : (I.ringCon : (a : R) → R → Prop) x 0
⊢ (J.ringCon : (a : R) → R → Prop) x 0

Tactic:
exact h hx
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : RingCon R
⊢ { ringCon := x : TwoSidedIdeal R } = { ringCon := { ringCon := x }.ringCon }

Tactic:
rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I ≤ J ↔ I.ringCon ≤ J.ringCon

Tactic:
orderIsoRingCon.map_rel_iff.symm

Premises used: RelIso.map_rel_iff, TwoSidedIdeal.orderIsoRingCon, Iff.symm
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
h : ∀ (x : R), x ∈ I ↔ x ∈ J
⊢ I = J

Tactic:
coeOrderEmbedding.injective (Set.ext h)

Premises used: Set.ext, TwoSidedIdeal.coeOrderEmbedding, RelEmbedding.injective
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
rw : (↑I : Set R) ⊆ (↑J : Set R) ∧ I ≠ J ↔ (↑I : Set R) ⊆ (↑J : Set R) ∧ (↑I : Set R) ≠ (↑J : Set R)
⊢ I < J ↔ (↑I : Set R) ⊂ (↑J : Set R)

Tactic:
rw [lt_iff_le_and_ne, Set.ssubset_iff_subset_ne, le_iff]

Premises used: lt_iff_le_and_ne, Set.ssubset_iff_subset_ne, TwoSidedIdeal.le_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ (↑I : Set R) ⊆ (↑J : Set R) ∧ I ≠ J ↔ (↑I : Set R) ⊆ (↑J : Set R) ∧ (↑I : Set R) ≠ (↑J : Set R)

Tactic:
simp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
⊢ 0 ∈ I

Tactic:
I.ringCon.refl 0

Premises used: Set.Mem, setOf, RingCon.refl, TwoSidedIdeal.ringCon, OfNat.ofNat
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hx : x ∈ I
hy : y ∈ I
⊢ x + y ∈ I

Tactic:
simpa using I.ringCon.add hx hy

Premises used: TwoSidedIdeal.ringCon, RingCon.add
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x : R
hx : x ∈ I
⊢ -x ∈ I

Tactic:
simpa using I.ringCon.neg hx

Premises used: RingCon.neg, TwoSidedIdeal.ringCon
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hx : x ∈ I
hy : y ∈ I
⊢ x - y ∈ I

Tactic:
_root_.sub_mem hx hy

Premises used: sub_mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hy : y ∈ I
⊢ x * y ∈ I

Tactic:
simpa using I.ringCon.mul (I.ringCon.refl x) hy

Premises used: RingCon.mul, RingCon.refl, TwoSidedIdeal.ringCon
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hx : x ∈ I
⊢ x * y ∈ I

Tactic:
simpa using I.ringCon.mul hx (I.ringCon.refl y)

Premises used: RingCon.mul, RingCon.refl, TwoSidedIdeal.ringCon
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x : R
n : ℕ
hx : x ∈ I
⊢ n • x ∈ I

Tactic:
_root_.nsmul_mem hx _

Premises used: nsmul_mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x : R
n : ℤ
hx : x ∈ I
⊢ n • x ∈ I

Tactic:
_root_.zsmul_mem hx _

Premises used: zsmul_mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x : R
⊢ x - x ∈ carrier

Tactic:
simpa using zero_mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x y : R
h : x - y ∈ carrier
⊢ y - x ∈ carrier

Tactic:
simpa using neg_mem h
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x y z : R
h1 : x - y ∈ carrier
h2 : y - z ∈ carrier
⊢ x - z = x - y + (y - z)

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x y z : R
h1 : x - y ∈ carrier
h2 : y - z ∈ carrier
⊢ x - z ∈ carrier

Tactic:
simpa only [show x - z = (x - y) + (y - z) by abel] using add_mem h1 h2