awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubring R) (closure s) y → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p x 0 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x
⊢ p x 0 hx ⋯

Tactic:
zero_right x hx
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubring R) (closure s) y → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p x 0 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x
⊢ p x 0 hx ⋯

Tactic:
exact zero_right x hx
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubring R) (closure s) y → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p x 0 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x
x_1 y_1 : R
hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1
hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y_1
h₁ : p x x_1 hx hx_1
h₂ : p x y_1 hx hy
⊢ p x (x_1 * y_1) hx ⋯

Tactic:
mul_right _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubring R) (closure s) y → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p x 0 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x
x_1 y_1 : R
hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1
hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y_1
h₁ : p x x_1 hx hx_1
h₂ : p x y_1 hx hy
⊢ p x (x_1 * y_1) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubring R) (closure s) y → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p x 0 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x
x_1 y_1 : R
hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1
hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y_1
h₁ : p x x_1 hx hx_1
h₂ : p x y_1 hx hy
⊢ p x (x_1 + y_1) hx ⋯

Tactic:
add_right _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubring R) (closure s) y → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p x 0 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x
x_1 y_1 : R
hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1
hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y_1
h₁ : p x x_1 hx hx_1
h₂ : p x y_1 hx hy
⊢ p x (x_1 + y_1) hx ⋯

Tactic:
exact add_right _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubring R) (closure s) y → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p x 0 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x
x_1 : R
hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1
h : p x x_1 hx hx_1
⊢ p x (-x_1) hx ⋯

Tactic:
neg_right _ _ _ _ h
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubring R) (closure s) y → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x), p x 0 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x
x_1 : R
hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1
h : p x x_1 hx hx_1
⊢ p x (-x_1) hx ⋯

Tactic:
exact neg_right _ _ _ _ h
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 : R
hx : x_1 ∈ s
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_1

Tactic:
AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)

Premises used: Subsemigroup.subset_closure, AddSubgroup.subset_closure
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 : R
hx : x_1 ∈ s
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_1

Tactic:
exact AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)

Premises used: Subsemigroup.subset_closure, AddSubgroup.subset_closure
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y : R
hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1
hy_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) y
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_1 + y)

Tactic:
add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y : R
hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1
hy_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) y
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_1 + y)

Tactic:
exact add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x_1 x : R
hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (-x)

Tactic:
neg_mem hx

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x_1 x : R
hx_1 : Membership.mem (γ := NonUnitalSubring R) (closure s) x
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (-x)

Tactic:
exact neg_mem hx

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y x_2 y_1 : R
hx : x_2 ∈ (↑(Subsemigroup.closure s) : Set R)
hy : y_1 ∈ (↑(Subsemigroup.closure s) : Set R)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_2 * y_1)

Tactic:
AddSubgroup.subset_closure (mul_mem hx hy)

Premises used: AddSubgroup.subset_closure, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y x_2 y_1 : R
hx : x_2 ∈ (↑(Subsemigroup.closure s) : Set R)
hy : y_1 ∈ (↑(Subsemigroup.closure s) : Set R)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_2 * y_1)

Tactic:
exact AddSubgroup.subset_closure (mul_mem hx hy)

Premises used: AddSubgroup.subset_closure, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y x_2 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_2
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (0 * x_2)

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y x_2 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_2
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_2 * 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y x_2 y_1 z : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_2
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y_1
hz : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) z
h₁ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_2 * z)
h₂ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (y_1 * z)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) ((x_2 + y_1) * z)

Tactic:
simpa [add_mul] using add_mem h₁ h₂

Premises used: add_mul, AddMemClass.add_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y y_1 z x_2 : R
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y_1
hz : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) z
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_2
h₁ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_2 * y_1)
h₂ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_2 * z)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_2 * (y_1 + z))

Tactic:
simpa [mul_add] using add_mem h₁ h₂

Premises used: AddMemClass.add_mem, mul_add