awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
p : (x y : R) → Membership.mem (γ := Subring R) (closure s) x → Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p x 1 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := Subring R) (closure s) x) (hy : Membership.mem (γ := Subring R) (closure s) y),
    p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := Subring R) (closure s) x) (hy : Membership.mem (γ := Subring R) (closure s) y),
    p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x
x_1 y_1 : R
hx_1 : Membership.mem (γ := Subring R) (closure s) x_1
hy : Membership.mem (γ := Subring 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.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
p : (x y : R) → Membership.mem (γ := Subring R) (closure s) x → Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p x 1 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := Subring R) (closure s) x) (hy : Membership.mem (γ := Subring R) (closure s) y),
    p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := Subring R) (closure s) x) (hy : Membership.mem (γ := Subring R) (closure s) y),
    p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x
x_1 y_1 : R
hx_1 : Membership.mem (γ := Subring R) (closure s) x_1
hy : Membership.mem (γ := Subring 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.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
p : (x y : R) → Membership.mem (γ := Subring R) (closure s) x → Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p x 1 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := Subring R) (closure s) x) (hy : Membership.mem (γ := Subring R) (closure s) y),
    p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := Subring R) (closure s) x) (hy : Membership.mem (γ := Subring R) (closure s) y),
    p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x
x_1 y_1 : R
hx_1 : Membership.mem (γ := Subring R) (closure s) x_1
hy : Membership.mem (γ := Subring 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.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
p : (x y : R) → Membership.mem (γ := Subring R) (closure s) x → Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p x 1 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := Subring R) (closure s) x) (hy : Membership.mem (γ := Subring R) (closure s) y),
    p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := Subring R) (closure s) x) (hy : Membership.mem (γ := Subring R) (closure s) y),
    p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x
x_1 : R
hx_1 : Membership.mem (γ := Subring R) (closure s) x_1
h : p x x_1 hx hx_1
⊢ p x (-x_1) hx ⋯

Tactic:
neg_right _ _ _ _ h
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
p : (x y : R) → Membership.mem (γ := Subring R) (closure s) x → Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subring R) (closure s) x), p x 1 hx ⋯
neg_left :
  ∀ (x y : R) (hx : Membership.mem (γ := Subring R) (closure s) x) (hy : Membership.mem (γ := Subring R) (closure s) y),
    p x y hx hy → p (-x) y ⋯ hy
neg_right :
  ∀ (x y : R) (hx : Membership.mem (γ := Subring R) (closure s) x) (hy : Membership.mem (γ := Subring R) (closure s) y),
    p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x)
    (hy : Membership.mem (γ := Subring R) (closure s) y) (hz : Membership.mem (γ := Subring 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 (γ := Subring R) (closure s) x
x_1 : R
hx_1 : Membership.mem (γ := Subring 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.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 : R
hx : x_1 ∈ s
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1

Tactic:
AddSubgroup.subset_closure (Submonoid.subset_closure hx)

Premises used: Submonoid.subset_closure, AddSubgroup.subset_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 : R
hx : x_1 ∈ s
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1

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

Premises used: Submonoid.subset_closure, AddSubgroup.subset_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 1

Tactic:
AddSubgroup.subset_closure (one_mem _)

Premises used: OneMemClass.one_mem, AddSubgroup.subset_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 1

Tactic:
exact AddSubgroup.subset_closure (one_mem _)

Premises used: OneMemClass.one_mem, AddSubgroup.subset_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y : R
hx_1 : Membership.mem (γ := Subring R) (closure s) x_1
hy_1 : Membership.mem (γ := Subring R) (closure s) y
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x_1 + y)

Tactic:
add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y : R
hx_1 : Membership.mem (γ := Subring R) (closure s) x_1
hy_1 : Membership.mem (γ := Subring R) (closure s) y
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x_1 + y)

Tactic:
exact add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 : R
hx_1 : Membership.mem (γ := Subring R) (closure s) x_1
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (-x_1)

Tactic:
neg_mem hx

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 : R
hx_1 : Membership.mem (γ := Subring R) (closure s) x_1
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (-x_1)

Tactic:
exact neg_mem hx

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y x_2 y_1 : R
hx : x_2 ∈ (↑(Submonoid.closure s) : Set R)
hy : y_1 ∈ (↑(Submonoid.closure s) : Set R)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.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.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y x_2 y_1 : R
hx : x_2 ∈ (↑(Submonoid.closure s) : Set R)
hy : y_1 ∈ (↑(Submonoid.closure s) : Set R)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.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.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y x_2 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_2
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (0 * x_2)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y x_2 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_2
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x_2 * 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y x_2 y_1 z : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_2
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y_1
hz : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) z
h₁ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x_2 * z)
h₂ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (y_1 * z)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.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.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y y_1 z x_2 : R
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y_1
hz : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) z
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_2
h₁ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x_2 * y_1)
h₂ : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x_2 * z)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.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
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y x_2 y_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_2
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y_1
h : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x_2 * y_1)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (-x_2 * y_1)

Tactic:
simpa [neg_mul] using neg_mem h

Premises used: neg_mul, NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y x_2 y_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_2
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y_1
h : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x_2 * y_1)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x_2 * -y_1)

Tactic:
simpa [mul_neg] using neg_mem h

Premises used: mul_neg, NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := Subring R) (closure s) x
mem :
  ∀ (x : R) (hx : x ∈ s), Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
zero : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 0
one : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) 1
add :
  ∀ (x y : R),
    Membership.mem (γ := Subring R) (closure s) x →
      Membership.mem (γ := Subring R) (closure s) y →
        ∀ (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x)
          (hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y),
          Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x + y)
neg :
  ∀ (x : R),
    Membership.mem (γ := Subring R) (closure s) x →
      ∀ (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x),
        Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (-x)
mul :
  ∀ (x y : R) (_hx : Membership.mem (γ := Subring R) (closure s) x)
    (_hy : Membership.mem (γ := Subring R) (closure s) y)
    (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x)
    (hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) (x * y)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x

Tactic:
induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Submonoid.subset_closure hx)
    | zero => exact zero_mem _
    | one => exact AddSubgroup.subset_closure (one_mem _)
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg _ _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h

Premises used: add_mul, mul_add, neg_mul, ZeroMemClass.zero_mem, OneMemClass.one_mem, mul_neg, NegMemClass.neg_mem, AddSubgroup.subset_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x_1 x x_2 : R
h : x_2 ∈ s
⊢ Membership.mem (γ := Subring R) (closure s) x_2

Tactic:
subset_closure h

Premises used: Subring.subset_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x_1 x x_2 : R
h : x_2 ∈ s
⊢ Membership.mem (γ := Subring R) (closure s) x_2

Tactic:
exact subset_closure h

Premises used: Subring.subset_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x_1 x : R
⊢ Membership.mem (γ := Subring R) (closure s) 1

Tactic:
one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x_1 x : R
⊢ Membership.mem (γ := Subring R) (closure s) 1

Tactic:
exact one_mem _

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x_1 x x_2 y : R
hx : Membership.mem (γ := Submonoid R) (Submonoid.closure s) x_2
hy : Membership.mem (γ := Submonoid R) (Submonoid.closure s) y
h₁ : Membership.mem (γ := Subring R) (closure s) x_2
h₂ : Membership.mem (γ := Subring R) (closure s) y
⊢ Membership.mem (γ := Subring R) (closure s) (x_2 * y)

Tactic:
mul_mem h₁ h₂

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x_1 x x_2 y : R
hx : Membership.mem (γ := Submonoid R) (Submonoid.closure s) x_2
hy : Membership.mem (γ := Submonoid R) (Submonoid.closure s) y
h₁ : Membership.mem (γ := Subring R) (closure s) x_2
h₂ : Membership.mem (γ := Subring R) (closure s) y
⊢ Membership.mem (γ := Subring R) (closure s) (x_2 * y)

Tactic:
exact mul_mem h₁ h₂

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x_1 x : R
hx : x ∈ (↑(Submonoid.closure s) : Set R)
mem : ∀ (x : R) (h : x ∈ s), Membership.mem (γ := Subring R) (closure s) x
mem₁ : Membership.mem (γ := Subring R) (closure s) 1
mem₂ :
  ∀ (x y : R),
    Membership.mem (γ := Submonoid R) (Submonoid.closure s) x →
      Membership.mem (γ := Submonoid R) (Submonoid.closure s) y →
        ∀ (h₁ : Membership.mem (γ := Subring R) (closure s) x) (h₂ : Membership.mem (γ := Subring R) (closure s) y),
          Membership.mem (γ := Subring R) (closure s) (x * y)
⊢ Membership.mem (γ := Subring R) (closure s) x

Tactic:
induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂

Premises used: OneMemClass.one_mem