awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x y : R
hxy : x - y ∈ s
hI : x - y ∈ (↑I : Set R)
rwa : ∀ (hI : x - y ∈ I), (I.ringCon : (a : R) → R → Prop) x y
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hI : (I.ringCon : (a : R) → R → Prop) x y), (I.ringCon : (a : R) → R → Prop) x y
⊢ (I.ringCon : (a : R) → R → Prop) x y

Tactic:
rwa [SetLike.mem_coe, ← rel_iff] at hI

Premises used: TwoSidedIdeal.rel_iff, SetLike.mem_coe
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x
rw : ∀ (hx : ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I) (I : TwoSidedIdeal R), t ⊆ (↑I : Set R) → x ∈ I
⊢ Membership.mem (γ := TwoSidedIdeal R) (span t) x

Tactic:
rw [mem_span_iff] at hx ⊢

Premises used: TwoSidedIdeal.mem_span_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I
⊢ ∀ (I : TwoSidedIdeal R), t ⊆ (↑I : Set R) → x ∈ I

Tactic:
fun I hI => hx I <| h.trans hI

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → x ∈ I
⊢ ∀ (I : TwoSidedIdeal R), t ⊆ (↑I : Set R) → x ∈ I

Tactic:
exact fun I hI => hx I <| h.trans hI

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
rw : LE.le (α := R → R → Prop) (fun (a b : R) ↦ a - b ∈ s) (⇑I.ringCon : (a : R) → R → Prop) ↔ s ⊆ (↑I : Set R)
⊢ span s ≤ I ↔ s ⊆ (↑I : Set R)

Tactic:
rw [TwoSidedIdeal.ringCon_le_iff, RingCon.gi _ |>.gc]

Premises used: RingCon.gi, TwoSidedIdeal.ringCon_le_iff, GaloisInsertion.gc
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
h : LE.le (α := R → R → Prop) (fun (a b : R) ↦ a - b ∈ s) (⇑I.ringCon : (a : R) → R → Prop)
x : R
hx : x ∈ s
⊢ x ∈ (↑I : Set R)

Tactic:
aesop
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
⊢ LE.le (α := R → R → Prop) (fun (a b : R) ↦ a - b ∈ s) (⇑I.ringCon : (a : R) → R → Prop) ↔ s ⊆ (↑I : Set R)

Tactic:
exact ⟨fun h x hx ↦ by aesop, fun h x y hxy ↦ (rel_iff I x y).mpr (h hxy)⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → Membership.mem (γ := TwoSidedIdeal R) (span s) x → Prop
mem : ∀ (x : R) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add :
  ∀ (x y : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x)
    (hy : Membership.mem (γ := TwoSidedIdeal R) (span s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx → p (-x) ⋯
left_absorb : ∀ (a x : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx → p (a * x) ⋯
right_absorb : ∀ (b x : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx → p (x * b) ⋯
x_1 : R
hx_1 : Membership.mem (γ := TwoSidedIdeal R) (span s) x_1
J : TwoSidedIdeal R := mk' {x : R | ∃ (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx} ⋯ ⋯ ⋯ ⋯ ⋯
x : R
hx : x ∈ s
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) (x - 0)

Tactic:
simpa using (mem_span_iff.2 fun I a ↦ a hx)

Premises used: Iff.mpr, TwoSidedIdeal.mem_span_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → Membership.mem (γ := TwoSidedIdeal R) (span s) x → Prop
mem : ∀ (x : R) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add :
  ∀ (x y : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x)
    (hy : Membership.mem (γ := TwoSidedIdeal R) (span s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx → p (-x) ⋯
left_absorb : ∀ (a x : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx → p (a * x) ⋯
right_absorb : ∀ (b x : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx → p (x * b) ⋯
x_1 : R
hx_1 : Membership.mem (γ := TwoSidedIdeal R) (span s) x_1
J : TwoSidedIdeal R := mk' {x : R | ∃ (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx} ⋯ ⋯ ⋯ ⋯ ⋯
x : R
hx : x ∈ s
⊢ p (x - 0) ⋯

Tactic:
simp_all
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → Membership.mem (γ := TwoSidedIdeal R) (span s) x → Prop
mem : ∀ (x : R) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add :
  ∀ (x y : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x)
    (hy : Membership.mem (γ := TwoSidedIdeal R) (span s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx → p (-x) ⋯
left_absorb : ∀ (a x : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx → p (a * x) ⋯
right_absorb : ∀ (b x : R) (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx → p (x * b) ⋯
x : R
hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x
J : TwoSidedIdeal R := mk' {x : R | ∃ (hx : Membership.mem (γ := TwoSidedIdeal R) (span s) x), p x hx} ⋯ ⋯ ⋯ ⋯ ⋯
h : Membership.mem (γ := TwoSidedIdeal R) (span s) (x - 0)
⊢ p (x - 0) h → p x hx

Tactic:
simp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
I J : TwoSidedIdeal R
h : I ≤ J
⊢ LE.le.{u_2} (α := TwoSidedIdeal S) (map f I) (map f J)

Tactic:
span_mono <| Set.image_mono h

Premises used: TwoSidedIdeal.span_mono, Set.Mem, Set.image_mono, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
I J : TwoSidedIdeal S
h : I ≤ J
⊢ (↑I : Set S) ⊆ (↑J : Set S)

Tactic:
rw [le_iff] at h

Premises used: TwoSidedIdeal.le_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
I J : TwoSidedIdeal S
h : (↑I : Set S) ⊆ (↑J : Set S)
x : R
⊢ Membership.mem (α := S) (↑I : Set S) ((f : (a : R) → S) x : S) →
    Membership.mem (α := S) (↑J : Set S) ((f : (a : R) → S) x : S)

Tactic:
specialize @h (f x)
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
I J : TwoSidedIdeal S
x : R
h :
  Membership.mem (α := S) (↑I : Set S) ((f : (a : R) → S) x : S) →
    Membership.mem (α := S) (↑J : Set S) ((f : (a : R) → S) x : S)
⊢ Membership.mem (γ := TwoSidedIdeal R)
      ((fun (I : TwoSidedIdeal S) ↦ ({ ringCon := I.ringCon.comap f } : TwoSidedIdeal R)) I) x →
    Membership.mem (γ := TwoSidedIdeal R)
      ((fun (I : TwoSidedIdeal S) ↦ ({ ringCon := I.ringCon.comap f } : TwoSidedIdeal R)) J) x

Tactic:
simpa [mem_iff, RingCon.comap]

Premises used: TwoSidedIdeal.mem_iff, RingCon.comap
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
I J : TwoSidedIdeal S
h : I ≤ J
⊢ LE.le.{u_1} (α := TwoSidedIdeal R)
    (((comap f : OrderHom.{u_2, u_1} (TwoSidedIdeal S) (TwoSidedIdeal R)) : (a : TwoSidedIdeal S) → TwoSidedIdeal R) I :
      TwoSidedIdeal R)
    (((comap f : OrderHom.{u_2, u_1} (TwoSidedIdeal S) (TwoSidedIdeal R)) : (a : TwoSidedIdeal S) → TwoSidedIdeal R) J :
      TwoSidedIdeal R)

Tactic:
(comap f).monotone h

Premises used: TwoSidedIdeal.comap, OrderHom.monotone, Set.Mem, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
I : TwoSidedIdeal S
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R)
      (((comap f : OrderHom.{u_2, u_1} (TwoSidedIdeal S) (TwoSidedIdeal R)) : (a : TwoSidedIdeal S) → TwoSidedIdeal R)
          I :
        TwoSidedIdeal R)
      x ↔
    Membership.mem (α := S) I ((f : (a : R) → S) x : S)

Tactic:
simp [comap, RingCon.comap, mem_iff]

Premises used: TwoSidedIdeal.comap, TwoSidedIdeal.mem_iff, RingCon.comap
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
e : R ≃+* S
h :
  ∀ (x : TwoSidedIdeal S) (x_1 : S),
    Membership.mem (γ := TwoSidedIdeal S)
        ((OrderHom.comp (β := TwoSidedIdeal R) (comap e.symm) (comap e) : (a : TwoSidedIdeal S) → TwoSidedIdeal S) x :
          TwoSidedIdeal S)
        x_1 ↔
      Membership.mem (γ := TwoSidedIdeal S)
        ((OrderHom.id : (a : TwoSidedIdeal S) → TwoSidedIdeal S) x : TwoSidedIdeal S) x_1
⊢ Eq (α := TwoSidedIdeal S →o TwoSidedIdeal S) (OrderHom.comp (β := TwoSidedIdeal R) (comap e.symm) (comap e))
    OrderHom.id

Tactic:
ext
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
e : R ≃+* S
x : TwoSidedIdeal S
x_1 : S
⊢ Membership.mem (γ := TwoSidedIdeal S)
      ((OrderHom.comp (β := TwoSidedIdeal R) (comap e.symm) (comap e) : (a : TwoSidedIdeal S) → TwoSidedIdeal S) x :
        TwoSidedIdeal S)
      x_1 ↔
    Membership.mem (γ := TwoSidedIdeal S) ((OrderHom.id : (a : TwoSidedIdeal S) → TwoSidedIdeal S) x : TwoSidedIdeal S)
      x_1

Tactic:
simp [mem_comap]

Premises used: TwoSidedIdeal.mem_comap
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
e : R ≃+* S
h :
  ∀ (x : TwoSidedIdeal R) (x_1 : R),
    Membership.mem (γ := TwoSidedIdeal R)
        ((OrderHom.comp (β := TwoSidedIdeal S) (comap e) (comap e.symm) : (a : TwoSidedIdeal R) → TwoSidedIdeal R) x :
          TwoSidedIdeal R)
        x_1 ↔
      Membership.mem (γ := TwoSidedIdeal R)
        ((OrderHom.id : (a : TwoSidedIdeal R) → TwoSidedIdeal R) x : TwoSidedIdeal R) x_1
⊢ Eq (α := TwoSidedIdeal R →o TwoSidedIdeal R) (OrderHom.comp (β := TwoSidedIdeal S) (comap e) (comap e.symm))
    OrderHom.id

Tactic:
ext
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
F : Type u_3
inst_2 : FunLike F R S
f : F
inst_3 : NonUnitalRingHomClass F R S
e : R ≃+* S
x : TwoSidedIdeal R
x_1 : R
⊢ Membership.mem (γ := TwoSidedIdeal R)
      ((OrderHom.comp (β := TwoSidedIdeal S) (comap e) (comap e.symm) : (a : TwoSidedIdeal R) → TwoSidedIdeal R) x :
        TwoSidedIdeal R)
      x_1 ↔
    Membership.mem (γ := TwoSidedIdeal R) ((OrderHom.id : (a : TwoSidedIdeal R) → TwoSidedIdeal R) x : TwoSidedIdeal R)
      x_1

Tactic:
simp [mem_comap]

Premises used: TwoSidedIdeal.mem_comap
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
e : R ≃+* S
I : TwoSidedIdeal R
⊢ Eq.{u_2 + 1} (α := TwoSidedIdeal S)
    ((e.mapTwoSidedIdeal : (a : TwoSidedIdeal R) → TwoSidedIdeal S) I : TwoSidedIdeal S)
    (((comap e.symm : OrderHom.{u_1, u_2} (TwoSidedIdeal R) (TwoSidedIdeal S)) :
          (a : TwoSidedIdeal R) → TwoSidedIdeal S)
        I :
      TwoSidedIdeal S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
e : R ≃+* S
⊢ e.mapTwoSidedIdeal.symm = e.symm.mapTwoSidedIdeal

Tactic:
rfl

Premises used: RingEquiv.mapTwoSidedIdeal, RelIso.symm, Equiv.symm, RingEquiv.symm, rfl, OrderIso.ofHomInv
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
h :
  ∀ (x : R),
    Membership.mem (γ := TwoSidedIdeal R)
        (((comap f : OrderHom.{u_2, u_1} (TwoSidedIdeal S) (TwoSidedIdeal R)) : (a : TwoSidedIdeal S) → TwoSidedIdeal R)
            (((comap g : OrderHom.{u_3, u_2} (TwoSidedIdeal T) (TwoSidedIdeal S)) :
                (a : TwoSidedIdeal T) → TwoSidedIdeal S)
              I) :
          TwoSidedIdeal R)
        x ↔
      Membership.mem (γ := TwoSidedIdeal R)
        (((comap (g.comp f) : OrderHom.{u_3, u_1} (TwoSidedIdeal T) (TwoSidedIdeal R)) :
              (a : TwoSidedIdeal T) → TwoSidedIdeal R)
            I :
          TwoSidedIdeal R)
        x
⊢ Eq.{u_1 + 1} (α := TwoSidedIdeal R)
    (((comap f : OrderHom.{u_2, u_1} (TwoSidedIdeal S) (TwoSidedIdeal R)) : (a : TwoSidedIdeal S) → TwoSidedIdeal R)
        (((comap g : OrderHom.{u_3, u_2} (TwoSidedIdeal T) (TwoSidedIdeal S)) : (a : TwoSidedIdeal T) → TwoSidedIdeal S)
          I) :
      TwoSidedIdeal R)
    (((comap (g.comp f) : OrderHom.{u_3, u_1} (TwoSidedIdeal T) (TwoSidedIdeal R)) :
          (a : TwoSidedIdeal T) → TwoSidedIdeal R)
        I :
      TwoSidedIdeal R)

Tactic:
ext
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R)
      (((comap f : OrderHom.{u_2, u_1} (TwoSidedIdeal S) (TwoSidedIdeal R)) : (a : TwoSidedIdeal S) → TwoSidedIdeal R)
          (((comap g : OrderHom.{u_3, u_2} (TwoSidedIdeal T) (TwoSidedIdeal S)) :
              (a : TwoSidedIdeal T) → TwoSidedIdeal S)
            I) :
        TwoSidedIdeal R)
      x ↔
    Membership.mem (γ := TwoSidedIdeal R)
      (((comap (g.comp f) : OrderHom.{u_3, u_1} (TwoSidedIdeal T) (TwoSidedIdeal R)) :
            (a : TwoSidedIdeal T) → TwoSidedIdeal R)
          I :
        TwoSidedIdeal R)
      x

Tactic:
simp [mem_comap]

Premises used: TwoSidedIdeal.mem_comap
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : Membership.mem (γ := AddSubgroup R) (closure s) y
⊢ Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) y : R)

Tactic:
have := (AddMonoidHom.mulLeft x).map_closure s ▸ mem_map_of_mem _ hy
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : Membership.mem (γ := AddSubgroup R) (closure s) y
this :
  Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) y : R)
⊢ Membership.mem (γ := AddSubgroup R) (closure s) (x * y)

Tactic:
closure_mono ?_ this

Premises used: AddSubgroup.closure_mono
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : Membership.mem (γ := AddSubgroup R) (closure s) y
this :
  Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) y : R)
refine : (⇑(AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) '' s ⊆ s
⊢ Membership.mem (γ := AddSubgroup R) (closure s) (x * y)

Tactic:
refine closure_mono ?_ this

Premises used: AddSubgroup.closure_mono
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y_1 : R
hy_1 : Membership.mem (γ := AddSubgroup R) (closure s) y_1
this :
  Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) y_1 : R)
y : R
hy : y ∈ s
⊢ Membership.mem (α := R) s (((AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) y : R)

Tactic:
h_left x y hy

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y_1 : R
hy_1 : Membership.mem (γ := AddSubgroup R) (closure s) y_1
this :
  Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) y_1 : R)
y : R
hy : y ∈ s
⊢ Membership.mem (α := R) s (((AddMonoidHom.mulLeft x : R →+ R) : (a : R) → R) y : R)

Tactic:
exact h_left x y hy
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
⊢ ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)

Tactic:
have h_left' {x y} (hy : y ∈ closure s) : x * y ∈ closure s := by
    have := (AddMonoidHom.mulLeft x).map_closure s ▸ mem_map_of_mem _ hy
    refine closure_mono ?_ this
    rintro - ⟨y, hy, rfl⟩
    exact h_left x y hy
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' :
  ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
y x : R
hy : Membership.mem (γ := AddSubgroup R) (closure s) y
⊢ Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) y : R)

Tactic:
have := (AddMonoidHom.mulRight x).map_closure s ▸ mem_map_of_mem _ hy
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' :
  ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
y x : R
hy : Membership.mem (γ := AddSubgroup R) (closure s) y
this :
  Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) y : R)
⊢ Membership.mem (γ := AddSubgroup R) (closure s) (y * x)

Tactic:
closure_mono ?_ this

Premises used: AddSubgroup.closure_mono
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' :
  ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
y x : R
hy : Membership.mem (γ := AddSubgroup R) (closure s) y
this :
  Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) y : R)
refine : (⇑(AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) '' s ⊆ s
⊢ Membership.mem (γ := AddSubgroup R) (closure s) (y * x)

Tactic:
refine closure_mono ?_ this

Premises used: AddSubgroup.closure_mono
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' :
  ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
y_1 x : R
hy_1 : Membership.mem (γ := AddSubgroup R) (closure s) y_1
this :
  Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) y_1 : R)
y : R
hy : y ∈ s
⊢ Membership.mem (α := R) s (((AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) y : R)

Tactic:
h_right y x hy

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' :
  ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
y_1 x : R
hy_1 : Membership.mem (γ := AddSubgroup R) (closure s) y_1
this :
  Membership.mem (α := R) (γ := AddSubgroup R) (closure ((⇑(AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) '' s))
    (((AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) y_1 : R)
y : R
hy : y ∈ s
⊢ Membership.mem (α := R) s (((AddMonoidHom.mulRight x : R →+ R) : (a : R) → R) y : R)

Tactic:
exact h_right y x hy
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' :
  ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
⊢ ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)

Tactic:
have h_right' {y x} (hy : y ∈ closure s) : y * x ∈ closure s := by
    have := (AddMonoidHom.mulRight x).map_closure s ▸ mem_map_of_mem _ hy
    refine closure_mono ?_ this
    rintro - ⟨y, hy, rfl⟩
    exact h_right y x hy
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' :
  ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
this : Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ z ∈ I
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := AddSubgroup R) (closure s) z

Tactic:
simpa only [I, mem_mk', SetLike.mem_coe]

Premises used: SetLike.mem_coe, TwoSidedIdeal.mem_mk'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' :
  ∀ {x y : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (x * y)
h_right' :
  ∀ {y x : R} (hy : Membership.mem (γ := AddSubgroup R) (closure s) y),
    Membership.mem (γ := AddSubgroup R) (closure s) (y * x)
I : TwoSidedIdeal R := mk' (↑(closure s) : Set R) ⋯ ⋯ ⋯ ⋯ ⋯
suffices : Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ z ∈ I
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := AddSubgroup R) (closure s) z

Tactic:
suffices z ∈ span s ↔ z ∈ I by simpa only [I, mem_mk', SetLike.mem_coe]