awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ⋯ ⋯ ⋯ ⋯ ⋯
rw : (∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I) ↔ z ∈ I
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ z ∈ I

Tactic:
rw [mem_span_iff]

Premises used: TwoSidedIdeal.mem_span_iff
-- 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) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I) ↔ z ∈ I

Tactic:
⟨fun h ↦ h I fun x hx ↦ ?mem_closure_of_forall, fun hz J hJ ↦ ?mem_ideal_of_subset⟩

Premises used: Iff.intro
-- 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) ⋯ ⋯ ⋯ ⋯ ⋯
refine : ∀ (h : ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I) (x : R) (hx : x ∈ s), x ∈ (↑I : Set R)
refine₁ : ∀ (hz : z ∈ I) (J : TwoSidedIdeal R) (hJ : s ⊆ (↑J : Set R)), z ∈ J
⊢ (∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I) ↔ z ∈ I

Tactic:
refine ⟨fun h ↦ h I fun x hx ↦ ?mem_closure_of_forall, fun hz J hJ ↦ ?mem_ideal_of_subset⟩
-- 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) ⋯ ⋯ ⋯ ⋯ ⋯
h : ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I
x : R
hx : x ∈ s
⊢ x ∈ (↑I : Set R)

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

Premises used: SetLike.mem_coe, TwoSidedIdeal.mem_mk', AddSubgroup.subset_closure
-- 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) ⋯ ⋯ ⋯ ⋯ ⋯
h : ∀ (I : TwoSidedIdeal R), s ⊆ (↑I : Set R) → z ∈ I
x : R
hx : x ∈ s
⊢ x ∈ (↑I : Set R)

Tactic:
case mem_closure_of_forall => simpa only [I, SetLike.mem_coe, mem_mk'] using subset_closure hx

Premises used: SetLike.mem_coe, TwoSidedIdeal.mem_mk', AddSubgroup.subset_closure
-- 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) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
⊢ Membership.mem (γ := AddSubgroup R) (closure s) z

Tactic:
simp only [I, SetLike.mem_coe, mem_mk'] at hz

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) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
x : R
hx : x ∈ s
⊢ x ∈ J

Tactic:
hJ hx
-- 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) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
x : R
hx : x ∈ s
⊢ x ∈ J

Tactic:
exact hJ hx
-- 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) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
⊢ 0 ∈ J

Tactic:
zero_mem _

Premises used: Set.Mem, setOf, TwoSidedIdeal.zero_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)
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) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
⊢ 0 ∈ J

Tactic:
exact zero_mem _

Premises used: TwoSidedIdeal.zero_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)
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) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
x y : R
hx_1 : Membership.mem (γ := AddSubgroup R) (closure s) x
hy_1 : Membership.mem (γ := AddSubgroup R) (closure s) y
hx : x ∈ J
hy : y ∈ J
⊢ x + y ∈ J

Tactic:
J.add_mem hx hy

Premises used: Set.Mem, setOf, TwoSidedIdeal.add_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)
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) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
x y : R
hx_1 : Membership.mem (γ := AddSubgroup R) (closure s) x
hy_1 : Membership.mem (γ := AddSubgroup R) (closure s) y
hx : x ∈ J
hy : y ∈ J
⊢ x + y ∈ J

Tactic:
exact J.add_mem hx hy

Premises used: TwoSidedIdeal.add_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)
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) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
x : R
hx_1 : Membership.mem (γ := AddSubgroup R) (closure s) x
hx : x ∈ J
⊢ -x ∈ J

Tactic:
J.neg_mem hx

Premises used: Set.Mem, TwoSidedIdeal.neg_mem, setOf
-- 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) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
x : R
hx_1 : Membership.mem (γ := AddSubgroup R) (closure s) x
hx : x ∈ J
⊢ -x ∈ J

Tactic:
exact J.neg_mem hx

Premises used: TwoSidedIdeal.neg_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)
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) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
hz : Membership.mem (γ := AddSubgroup R) (closure s) z
mem : ∀ (x : R) (hx : x ∈ s), x ∈ J
zero : 0 ∈ J
add :
  ∀ (x y : R),
    Membership.mem (γ := AddSubgroup R) (closure s) x →
      Membership.mem (γ := AddSubgroup R) (closure s) y → ∀ (hx : x ∈ J) (hy : y ∈ J), x + y ∈ J
neg : ∀ (x : R), Membership.mem (γ := AddSubgroup R) (closure s) x → ∀ (hx : x ∈ J), -x ∈ J
⊢ z ∈ J

Tactic:
induction hz using closure_induction with
    | mem x hx => exact hJ hx
    | zero => exact zero_mem _
    | add x y _ _ hx hy => exact J.add_mem hx hy
    | neg x _ hx => exact J.neg_mem hx

Premises used: AddSubgroup.neg, AddSubgroup.zero, AddSubgroup.add, TwoSidedIdeal.zero_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)
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) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ (↑J : Set R)
⊢ Membership.mem (γ := AddSubgroup R) (closure s) z

Tactic:
case mem_ideal_of_subset =>
    simp only [I, SetLike.mem_coe, mem_mk'] at hz
    induction hz using closure_induction with
    | mem x hx => exact hJ hx
    | zero => exact zero_mem _
    | add x y _ _ hx hy => exact J.add_mem hx hy
    | neg x _ hx => exact J.neg_mem hx

Premises used: AddSubgroup.neg, SetLike.mem_coe, AddSubgroup.zero, AddSubgroup.add, TwoSidedIdeal.zero_mem, TwoSidedIdeal.mem_mk'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ (↑I : Set R)
t : Set R
r x : R
hx : x ∈ s
⊢ (fun (x1 x2 : R) ↦ x1 * x2) r x ∈ (↑I : Set R)

Tactic:
mul_mem_left _ _ _ (h hx)

Premises used: TwoSidedIdeal.mul_mem_left, Set.Mem, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ (↑I : Set R)
t : Set R
r x : R
hx : x ∈ s
⊢ (fun (x1 x2 : R) ↦ x1 * x2) r x ∈ (↑I : Set R)

Tactic:
exact mul_mem_left _ _ _ (h hx)

Premises used: TwoSidedIdeal.mul_mem_left
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ (↑I : Set R)
t : Set R
x : R
hx : x ∈ s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) x r ∈ (↑I : Set R)

Tactic:
mul_mem_right _ _ _ (h hx)

Premises used: TwoSidedIdeal.mul_mem_right, Set.Mem, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ (↑I : Set R)
t : Set R
x : R
hx : x ∈ s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) x r ∈ (↑I : Set R)

Tactic:
exact mul_mem_right _ _ _ (h hx)

Premises used: TwoSidedIdeal.mul_mem_right
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
trans :
  Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
    Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
trans₁ :
  Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z

Tactic:
trans z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)

Premises used: HMul.hMul, Set.univ, TwoSidedIdeal.span, Union.union
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
h : Membership.mem (γ := TwoSidedIdeal R) (span s) z
⊢ s ⊆ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
simp only [Set.union_assoc, Set.subset_union_left]

Premises used: Set.subset_union_left, Set.union_assoc
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
refine :
  ∀ (h : Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z),
    Membership.mem (γ := TwoSidedIdeal R) (span s) z
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
    Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z

Tactic:
refine ⟨(span_mono (by simp only [Set.union_assoc, Set.subset_union_left]) ·), fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
h : Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z

Tactic:
mem_span_iff.mp h (span s) ?_

Premises used: TwoSidedIdeal.span, TwoSidedIdeal.mem_span_iff, Iff.mp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
h : Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
refine : s ∪ s * univ ∪ univ * s ∪ univ * s * univ ⊆ (↑(span s) : Set R)
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z

Tactic:
refine mem_span_iff.mp h (span s) ?_

Premises used: TwoSidedIdeal.span, TwoSidedIdeal.mem_span_iff, Iff.mp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
h : Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
simp :
  s ⊆ (↑(span s) : Set R) ∧
    s * univ ⊆ (↑(span s) : Set R) ∧ univ * s ⊆ (↑(span s) : Set R) ∧ univ * s * univ ⊆ (↑(span s) : Set R)
⊢ s ∪ s * univ ∪ univ * s ∪ univ * s * univ ⊆ (↑(span s) : Set R)

Tactic:
simp only [union_subset_iff, union_assoc]

Premises used: Set.union_subset_iff, Set.union_assoc
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
h : Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
⊢ s ⊆ (↑(span s) : Set R) ∧
    s * univ ⊆ (↑(span s) : Set R) ∧ univ * s ⊆ (↑(span s) : Set R) ∧ univ * s * univ ⊆ (↑(span s) : Set R)

Tactic:
⟨subset_span, subset_mul_set subset_span _, set_mul_subset subset_span _,
      subset_mul_set (set_mul_subset subset_span _) _⟩

Premises used: TwoSidedIdeal.set_mul_subset, TwoSidedIdeal.subset_mul_set, And.intro, TwoSidedIdeal.subset_span
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
h : Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z
⊢ s ⊆ (↑(span s) : Set R) ∧
    s * univ ⊆ (↑(span s) : Set R) ∧ univ * s ⊆ (↑(span s) : Set R) ∧ univ * s * univ ⊆ (↑(span s) : Set R)

Tactic:
exact ⟨subset_span, subset_mul_set subset_span _, set_mul_subset subset_span _,
      subset_mul_set (set_mul_subset subset_span _) _⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z

Tactic:
mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_

Premises used: TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z : R
refine_1 :
  ∀ (x y : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
refine_2 :
  ∀ (y x : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
⊢ Membership.mem (γ := TwoSidedIdeal R) (span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)) z

Tactic:
refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_

Premises used: TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
⊢ x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
.inl <| .inr <| ⟨x, mem_univ _, y, hy, rfl⟩

Premises used: Set.union, Set.Mem, setOf, And.intro, Exists.intro, Set.mem_univ, Or.inl, Or.inr, rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
⊢ x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
exact .inl <| .inr <| ⟨x, mem_univ _, y, hy, rfl⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ x * (fun (x1 x2 : R) ↦ x1 * x2) y r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
.inr <| ⟨x * y, ⟨x, mem_univ _, y, hy, rfl⟩, r, mem_univ _, mul_assoc ..⟩

Premises used: Set.union, HMul.hMul, Set.Mem, mul_assoc, setOf, And.intro, Exists.intro, Set.mem_univ, Or.inr, rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ x * (fun (x1 x2 : R) ↦ x1 * x2) y r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
exact .inr <| ⟨x * y, ⟨x, mem_univ _, y, hy, rfl⟩, r, mem_univ _, mul_assoc ..⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ x * (fun (x1 x2 : R) ↦ x1 * x2) r y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
.inl <| .inr <| ⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩

Premises used: Set.union, HMul.hMul, Set.Mem, mul_assoc, setOf, And.intro, Exists.intro, Set.mem_univ, Or.inl, Or.inr
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ x * (fun (x1 x2 : R) ↦ x1 * x2) r y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
exact .inl <| .inr <| ⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
.inr <| ⟨x * r' * y, ⟨x * r', mem_univ _, y, hy, ?_⟩, ⟨r, mem_univ _, ?_⟩⟩

Premises used: Set.union, HMul.hMul, Set.Mem, setOf, And.intro, Exists.intro, Set.mem_univ, Or.inr
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
refine_1 : (fun (x1 x2 : R) ↦ x1 * x2) (x * r') y = x * r' * y
refine_1₁ :
  (fun (x1 x2 : R) ↦ x1 * x2) (x * r' * y) r = x * (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r
⊢ x * (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
refine .inr <| ⟨x * r' * y, ⟨x * r', mem_univ _, y, hy, ?_⟩, ⟨r, mem_univ _, ?_⟩⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) (x * r') y = x * r' * y

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) (x * r' * y) r = x * (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z y x : R
hy : y ∈ s
⊢ y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
.inl <| .inl <| .inr ⟨y, hy, x, mem_univ _, rfl⟩

Premises used: Set.union, Set.Mem, setOf, And.intro, Exists.intro, Set.mem_univ, Or.inl, Or.inr, rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z y x : R
hy : y ∈ s
⊢ y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
exact .inl <| .inl <| .inr ⟨y, hy, x, mem_univ _, rfl⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) y r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
.inl <| .inl <| .inr ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩

Premises used: Set.union, HMul.hMul, Set.Mem, mul_assoc, setOf, And.intro, Exists.intro, Set.mem_univ, Or.inl, Eq.symm, Or.inr
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) y r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
exact .inl <| .inl <| .inr ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ (fun (x1 x2 : R) ↦ x1 * x2) r y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
.inr <| ⟨r * y, ⟨r, mem_univ _, y, hy, rfl⟩, x, mem_univ _, rfl⟩

Premises used: Set.union, HMul.hMul, Set.Mem, setOf, And.intro, Exists.intro, Set.mem_univ, Or.inr, rfl