awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
rw : I.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon
⊢ I ≤ { ringCon := I.ringCon ⊔ J.ringCon }

Tactic:
rw [ringCon_le_iff]

Premises used: TwoSidedIdeal.ringCon_le_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
rw : J.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon
⊢ J ≤ { ringCon := I.ringCon ⊔ J.ringCon }

Tactic:
rw [ringCon_le_iff]

Premises used: TwoSidedIdeal.ringCon_le_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ J.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ J.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I ≤ K
h2 : J ≤ K
rw :
  ∀ (h1 : I.ringCon ≤ K.ringCon) (h2 : J.ringCon ≤ K.ringCon),
    { ringCon := I.ringCon ⊔ J.ringCon : TwoSidedIdeal R }.ringCon ≤ K.ringCon
⊢ { ringCon := I.ringCon ⊔ J.ringCon : TwoSidedIdeal R } ≤ K

Tactic:
rw [ringCon_le_iff] at h1 h2 ⊢

Premises used: TwoSidedIdeal.ringCon_le_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I.ringCon ≤ K.ringCon
h2 : J.ringCon ≤ K.ringCon
⊢ { ringCon := I.ringCon ⊔ J.ringCon : TwoSidedIdeal R }.ringCon ≤ K.ringCon

Tactic:
sup_le h1 h2

Premises used: sup_le
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I.ringCon ≤ K.ringCon
h2 : J.ringCon ≤ K.ringCon
⊢ { ringCon := I.ringCon ⊔ J.ringCon : TwoSidedIdeal R }.ringCon ≤ K.ringCon

Tactic:
exact sup_le h1 h2

Premises used: sup_le
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ (I ⊔ J).ringCon = I.ringCon ⊔ J.ringCon

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
h : x ∈ I
⊢ x ∈ I ⊔ J

Tactic:
(show I ≤ I ⊔ J from le_sup_left) h

Premises used: le_sup_left
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
h : x ∈ J
⊢ x ∈ I ⊔ J

Tactic:
(show J ≤ I ⊔ J from le_sup_right) h

Premises used: le_sup_right
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
mp : x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x
mpr : (∃ y ∈ I, ∃ z ∈ J, y + z = x) → x ∈ I ⊔ J
⊢ x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
constructor
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 x : R
hx : x ∈ I
y : R
hy : y ∈ J
a : R
ha : a ∈ I
b : R
hb : b ∈ J
⊢ x + a + (y + b) = x + y + (a + b)

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 x : R
hx : x ∈ I
y : R
hy : y ∈ J
a : R
ha : a ∈ I
b : R
hb : b ∈ J
⊢ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (x + y + (a + b))

Tactic:
exact ⟨x + a, ⟨add_mem _ hx ha, ⟨y + b, ⟨add_mem _ hy hb, by abel⟩⟩⟩⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ -x + -y = -(x + y)

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (-(x + y))

Tactic:
exact ⟨-x, ⟨neg_mem _ hx, ⟨-y, ⟨neg_mem _ hy, by abel⟩⟩⟩⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 r x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (r * (x + y))

Tactic:
⟨_, ⟨mul_mem_left _ _ _ hx, ⟨_, ⟨mul_mem_left _ _ _ hy, mul_add _ _ _ |>.symm⟩⟩⟩⟩

Premises used: TwoSidedIdeal.mul_mem_left, Set.Mem, setOf, And.intro, Exists.intro, mul_add, Eq.symm
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 r x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (r * (x + y))

Tactic:
exact ⟨_, ⟨mul_mem_left _ _ _ hx, ⟨_, ⟨mul_mem_left _ _ _ hy, mul_add _ _ _ |>.symm⟩⟩⟩⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 y_1 x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ((x + y) * y_1)

Tactic:
⟨_, ⟨mul_mem_right _ _ _ hx, ⟨_, ⟨mul_mem_right _ _ _ hy, add_mul _ _ _ |>.symm⟩⟩⟩⟩

Premises used: add_mul, TwoSidedIdeal.mul_mem_right, Set.Mem, setOf, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 y_1 x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ((x + y) * y_1)

Tactic:
exact ⟨_, ⟨mul_mem_right _ _ _ hx, ⟨_, ⟨mul_mem_right _ _ _ hy, add_mul _ _ _ |>.symm⟩⟩⟩⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ (s.ringCon : (a : R) → R → Prop) x 0

Tactic:
this h
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
a : (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ (s.ringCon : (a : R) → R → Prop) x 0
⊢ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
convert! this h
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
a : (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} x
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ (s.ringCon : (a : R) → R → Prop) x 0

Tactic:
rw [rel_iff, sub_zero, mem_mk']

Premises used: sub_zero, TwoSidedIdeal.rel_iff, TwoSidedIdeal.mem_mk'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} x

Tactic:
rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
mp : I.ringCon ⊔ J.ringCon ≤ s.ringCon
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
suffices (I.ringCon ⊔ J.ringCon) ≤ s.ringCon by
      intro h; convert! this h; rw [rel_iff, sub_zero, mem_mk']; rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
⊢ I.ringCon ⊔ J.ringCon ≤ s.ringCon

Tactic:
sup_le (fun x y h => ?_) (fun x y h => ?_)

Premises used: sup_le
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
mp : ∀ (x y : R) (h : (I.ringCon : (a : R) → R → Prop) x y), (s.ringCon : (a : R) → R → Prop) x y
mp₁ : ∀ (x y : R) (h : (J.ringCon : (a : R) → R → Prop) x y), (s.ringCon : (a : R) → R → Prop) x y
⊢ I.ringCon ⊔ J.ringCon ≤ s.ringCon

Tactic:
refine sup_le (fun x y h => ?_) (fun x y h => ?_)

Premises used: sup_le
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : (I.ringCon : (a : R) → R → Prop) x y
mp : ∀ (h : x - y ∈ I), x - y ∈ s
⊢ (s.ringCon : (a : R) → R → Prop) x y

Tactic:
rw [rel_iff] at h ⊢

Premises used: TwoSidedIdeal.rel_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : (J.ringCon : (a : R) → R → Prop) x y
mp : ∀ (h : x - y ∈ J), x - y ∈ s
⊢ (s.ringCon : (a : R) → R → Prop) x y

Tactic:
rw [rel_iff] at h ⊢

Premises used: TwoSidedIdeal.rel_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ I
mp : Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (x - y)
⊢ x - y ∈ s

Tactic:
rw [mem_mk']

Premises used: TwoSidedIdeal.mem_mk'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ J
mp : Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (x - y)
⊢ x - y ∈ s

Tactic:
rw [mem_mk']

Premises used: TwoSidedIdeal.mem_mk'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ I
⊢ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (x - y)

Tactic:
⟨_, ⟨h, ⟨0, ⟨zero_mem _, add_zero _⟩⟩⟩⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, add_zero, OfNat.ofNat, TwoSidedIdeal.zero_mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ J
⊢ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (x - y)

Tactic:
⟨0, ⟨zero_mem _, ⟨_, ⟨h, zero_add _⟩⟩⟩⟩

Premises used: Set.Mem, setOf, zero_add, And.intro, Exists.intro, OfNat.ofNat, TwoSidedIdeal.zero_mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ I
⊢ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (x - y)

Tactic:
exacts [⟨_, ⟨h, ⟨0, ⟨zero_mem _, add_zero _⟩⟩⟩⟩, ⟨0, ⟨zero_mem _, ⟨_, ⟨h, zero_add _⟩⟩⟩⟩]
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
y : R
hy : y ∈ I
z : R
hz : z ∈ J
⊢ y + z ∈ I ⊔ J

Tactic:
add_mem _ (mem_sup_left hy) (mem_sup_right hz)

Premises used: TwoSidedIdeal.mem_sup_right, TwoSidedIdeal.add_mem, TwoSidedIdeal.mem_sup_left
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
y : R
hy : y ∈ I
z : R
hz : z ∈ J
⊢ y + z ∈ I ⊔ J

Tactic:
exact add_mem _ (mem_sup_left hy) (mem_sup_right hz)

Premises used: TwoSidedIdeal.mem_sup_right, TwoSidedIdeal.add_mem, TwoSidedIdeal.mem_sup_left
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
rw : { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R }.ringCon ≤ I.ringCon
⊢ { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R } ≤ I

Tactic:
rw [ringCon_le_iff]

Premises used: TwoSidedIdeal.ringCon_le_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R }.ringCon ≤ I.ringCon

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R }.ringCon ≤ I.ringCon

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
rw : { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R }.ringCon ≤ J.ringCon
⊢ { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R } ≤ J

Tactic:
rw [ringCon_le_iff]

Premises used: TwoSidedIdeal.ringCon_le_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R }.ringCon ≤ J.ringCon

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R }.ringCon ≤ J.ringCon

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I ≤ J
h2 : I ≤ K
rw :
  ∀ (h1 : I.ringCon ≤ J.ringCon) (h2 : I.ringCon ≤ K.ringCon), I.ringCon ≤ { ringCon := J.ringCon ⊓ K.ringCon }.ringCon
⊢ I ≤ { ringCon := J.ringCon ⊓ K.ringCon }

Tactic:
rw [ringCon_le_iff] at h1 h2 ⊢

Premises used: TwoSidedIdeal.ringCon_le_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I.ringCon ≤ J.ringCon
h2 : I.ringCon ≤ K.ringCon
⊢ I.ringCon ≤ { ringCon := J.ringCon ⊓ K.ringCon }.ringCon

Tactic:
le_inf h1 h2

Premises used: le_inf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I.ringCon ≤ J.ringCon
h2 : I.ringCon ≤ K.ringCon
⊢ I.ringCon ≤ { ringCon := J.ringCon ⊓ K.ringCon }.ringCon

Tactic:
exact le_inf h1 h2

Premises used: le_inf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ (I ⊓ J).ringCon = I.ringCon ⊓ J.ringCon

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
S : Set (TwoSidedIdeal R)
⊢ (sSup S).ringCon = sSup (ringCon '' S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
e_a :
  Eq.{u_1 + 1} (α := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) (Set.range fun (i : ι) ↦ (I i).ringCon)
⊢ Eq.{u_1 + 1} (α := RingCon R) (sSup (ringCon '' Set.range fun (i : ι) ↦ I i))
    (sSup (Set.range fun (i : ι) ↦ (I i).ringCon))

Tactic:
congr
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
e_a :
  ∀ (x : RingCon R),
    Membership.mem (γ := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) x ↔
      Membership.mem (γ := Set (RingCon R)) (Set.range fun (i : ι) ↦ (I i).ringCon) x
⊢ Eq.{u_1 + 1} (α := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) (Set.range fun (i : ι) ↦ (I i).ringCon)

Tactic:
ext
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x : RingCon R
⊢ Membership.mem (γ := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) x ↔
    Membership.mem (γ := Set (RingCon R)) (Set.range fun (i : ι) ↦ (I i).ringCon) x

Tactic:
simp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
S : Set (TwoSidedIdeal R)
⊢ (sInf S).ringCon = sInf (ringCon '' S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
h : Eq.{u_1 + 1} (α := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) (Set.range fun (i : ι) ↦ (I i).ringCon)
⊢ Eq.{u_1 + 1} (α := RingCon R) (sInf (ringCon '' Set.range fun (i : ι) ↦ I i))
    (sInf (Set.range fun (i : ι) ↦ (I i).ringCon))

Tactic:
congr!
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
h :
  ∀ (x : RingCon R),
    Membership.mem (γ := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) x ↔
      Membership.mem (γ := Set (RingCon R)) (Set.range fun (i : ι) ↦ (I i).ringCon) x
⊢ Eq.{u_1 + 1} (α := Set (RingCon R)) (ringCon '' Set.range fun (i : ι) ↦ I i) (Set.range fun (i : ι) ↦ (I i).ringCon)

Tactic:
ext
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x : R
⊢ (∀ x_1 ∈ ringCon '' Set.range I, (x_1 : (a : R) → R → Prop) x 0) ↔ ∀ (i : ι), x ∈ I i

Tactic:
simp [mem_iff]

Premises used: TwoSidedIdeal.mem_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
S : Set (TwoSidedIdeal R)
x : R
⊢ (∀ x_1 ∈ ringCon '' S, (x_1 : (a : R) → R → Prop) x 0) ↔ ∀ I ∈ S, x ∈ I

Tactic:
simp [mem_iff]

Premises used: TwoSidedIdeal.mem_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
⊢ Eq.{u_1 + 1} (α := RingCon R) (ringCon ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R) ⊤ x

Tactic:
trivial

Premises used: trivial, Set.Mem, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
⊢ Eq.{u_1 + 1} (α := RingCon R) (ringCon ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R) ⊥ x ↔ x = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : TwoSidedIdeal R
rw : x.ringCon ≤ ringCon ⊤
⊢ x ≤ ⊤

Tactic:
rw [ringCon_le_iff]

Premises used: TwoSidedIdeal.ringCon_le_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : TwoSidedIdeal R
⊢ x.ringCon ≤ ringCon ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : TwoSidedIdeal R
⊢ x.ringCon ≤ ringCon ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : TwoSidedIdeal R
rw : ringCon ⊥ ≤ x.ringCon
⊢ ⊥ ≤ x

Tactic:
rw [ringCon_le_iff]

Premises used: TwoSidedIdeal.ringCon_le_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : TwoSidedIdeal R
⊢ ringCon ⊥ ≤ x.ringCon

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
x : TwoSidedIdeal R
⊢ ringCon ⊥ ≤ x.ringCon

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
⊢ (↑⊥ : Set R) = {0}

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
⊢ (↑⊤ : Set R) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice
Goal:
R : Type u_2
inst : NonAssocRing R
I : TwoSidedIdeal R
h : 1 ∈ I
x : R
h_1 : Membership.mem (γ := TwoSidedIdeal R) ⊤ x
⊢ x ∈ I

Tactic:
simpa using I.mul_mem_left x _ h

Premises used: TwoSidedIdeal.mul_mem_left
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x : R
hx : x ∈ s
⊢ x - 0 ∈ s

Tactic:
simpa using hx
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x : R
hx : x ∈ s
⊢ (ringCon (span s) : (a : R) → R → Prop) x 0

Tactic:
exact RingConGen.Rel.of _ _ (by simpa using hx)

Premises used: RingConGen.Rel.of
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) x ↔ ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I

Tactic:
⟨?_, fun h => h _ subset_span⟩

Premises used: TwoSidedIdeal.span, Iff.intro, TwoSidedIdeal.subset_span
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x : R
refine : Membership.mem (γ := TwoSidedIdeal R) (span s) x → ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) x ↔ ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I

Tactic:
refine ⟨?_, fun h => h _ subset_span⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x : R
rw :
  Membership.mem (γ := TwoSidedIdeal R)
      { ringCon := sInf {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y} } x →
    ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I
⊢ Membership.mem (γ := TwoSidedIdeal R) { ringCon := ringConGen fun (a b : R) ↦ a - b ∈ s } x →
    ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I

Tactic:
rw [RingCon.ringConGen_eq]

Premises used: RingCon.ringConGen_eq
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x : R
h :
  Membership.mem (γ := TwoSidedIdeal R)
    { ringCon := sInf {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y} } x
I : TwoSidedIdeal R
hI : s ⊆ (↑I : Set R)
⊢ x ∈ I

Tactic:
sInf_le (α := RingCon R) ?_ h

Premises used: Set.Mem, setOf, sInf_le
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x : R
h :
  Membership.mem (γ := TwoSidedIdeal R)
    { ringCon := sInf {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y} } x
I : TwoSidedIdeal R
hI : s ⊆ (↑I : Set R)
refine :
  Membership.mem (γ := Set (RingCon R)) {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y}
    I.ringCon
⊢ x ∈ I

Tactic:
refine sInf_le (α := RingCon R) ?_ h

Premises used: sInf_le
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
x_1 : R
h :
  Membership.mem (γ := TwoSidedIdeal R)
    { ringCon := sInf {s_1 : RingCon R | ∀ (x y : R), x - y ∈ s → (s_1 : (a : R) → R → Prop) x y} } x_1
I : TwoSidedIdeal R
hI : s ⊆ (↑I : Set R)
x y : R
hxy : x - y ∈ s
⊢ x - y ∈ (↑I : Set R)

Tactic:
specialize hI hxy