awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
K : NonUnitalSubsemiring S
⊢ Eq (α := NonUnitalSubsemiring R) (comap (F := R →ₙ+* S) (↑f : R →ₙ+* S) K) (map f.symm K)

Tactic:
(map_equiv_eq_comap_symm f.symm K).symm

Premises used: NonUnitalSubsemiring.comap, NonUnitalSubsemiring.map_equiv_eq_comap_symm, NonUnitalRingHomClass.toNonUnitalRingHom, NonUnitalSubsemiring.map, Eq.symm, RingEquiv.symm
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
⊢ (↑M.nonUnitalSubsemiringClosure : Set R) = (↑(AddSubmonoid.closure (↑M : Set R)) : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
⊢ M.nonUnitalSubsemiringClosure.toAddSubmonoid = AddSubmonoid.closure (↑M : Set R)

Tactic:
rfl

Premises used: AddSubmonoid.closure, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
h :
  ∀ (x : R),
    x ∈ M.nonUnitalSubsemiringClosure ↔
      Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x
⊢ M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure (↑M : Set R)

Tactic:
ext
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x : R
⊢ x ∈ M.nonUnitalSubsemiringClosure ↔
    Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x

Tactic:
⟨fun hx => ?_,
    fun hx => (NonUnitalSubsemiring.mem_closure.mp hx) M.nonUnitalSubsemiringClosure fun s sM => ?_⟩

Premises used: Iff.intro, Iff.mp, NonUnitalSubsemiring.mem_closure, Subsemigroup.nonUnitalSubsemiringClosure
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x : R
h :
  ∀ (hx : x ∈ M.nonUnitalSubsemiringClosure),
    Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x
h₁ :
  ∀ (hx : Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x) (s : R)
    (sM : s ∈ (↑M : Set R)), s ∈ (↑M.nonUnitalSubsemiringClosure : Set R)
⊢ x ∈ M.nonUnitalSubsemiringClosure ↔
    Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x

Tactic:
refine ⟨fun hx => ?_,
    fun hx => (NonUnitalSubsemiring.mem_closure.mp hx) M.nonUnitalSubsemiringClosure fun s sM => ?_⟩
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x : R
hx : x ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
H2 : Membership.mem (γ := Set (NonUnitalSubsemiring R)) {S : NonUnitalSubsemiring R | (↑M : Set R) ⊆ (↑S : Set R)} H1
⊢ Membership.mem (γ := Set R)
    ((fun
          (h :
            Membership.mem (γ := Set (NonUnitalSubsemiring R))
              {S : NonUnitalSubsemiring R | (↑M : Set R) ⊆ (↑S : Set R)} H1) ↦
        (↑H1 : Set R))
      H2)
    x

Tactic:
AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2

Premises used: Set.Mem, NonUnitalSubsemiring.toAddSubmonoid, AddSubmonoid.mem_closure, Iff.mp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x : R
hx : x ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
H2 : Membership.mem (γ := Set (NonUnitalSubsemiring R)) {S : NonUnitalSubsemiring R | (↑M : Set R) ⊆ (↑S : Set R)} H1
⊢ Membership.mem (γ := Set R)
    ((fun
          (h :
            Membership.mem (γ := Set (NonUnitalSubsemiring R))
              {S : NonUnitalSubsemiring R | (↑M : Set R) ⊆ (↑S : Set R)} H1) ↦
        (↑H1 : Set R))
      H2)
    x

Tactic:
exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2

Premises used: NonUnitalSubsemiring.toAddSubmonoid, AddSubmonoid.mem_closure, Iff.mp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x
s : R
sM : s ∈ (↑M : Set R)
H1 : AddSubmonoid R
H2 : Membership.mem (γ := Set (AddSubmonoid R)) {S : AddSubmonoid R | (↑M : Set R) ⊆ (↑S : Set R)} H1
⊢ Membership.mem (γ := Set R)
    ((fun (h : Membership.mem (γ := Set (AddSubmonoid R)) {S : AddSubmonoid R | (↑M : Set R) ⊆ (↑S : Set R)} H1) ↦
        (↑H1 : Set R))
      H2)
    s

Tactic:
H2 sM

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x
s : R
sM : s ∈ (↑M : Set R)
H1 : AddSubmonoid R
H2 : Membership.mem (γ := Set (AddSubmonoid R)) {S : AddSubmonoid R | (↑M : Set R) ⊆ (↑S : Set R)} H1
⊢ Membership.mem (γ := Set R)
    ((fun (h : Membership.mem (γ := Set (AddSubmonoid R)) {S : AddSubmonoid R | (↑M : Set R) ⊆ (↑S : Set R)} H1) ↦
        (↑H1 : Set R))
      H2)
    s

Tactic:
exact H2 sM
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
⊢ Eq (α := NonUnitalSubsemiring R) (closure (↑(Subsemigroup.closure s) : Set R)) (closure s)

Tactic:
le_antisymm
    (closure_le.mpr fun _ hy =>
      (Subsemigroup.mem_closure.mp hy) (closure s).toSubsemigroup subset_closure)
    (closure_mono Subsemigroup.subset_closure)

Premises used: Iff.mpr, NonUnitalSubsemiring.toSubsemigroup, NonUnitalSubsemiring.subset_closure, NonUnitalSubsemiring.closure_mono, Subsemigroup.mem_closure, le_antisymm, NonUnitalSubsemiring.closure, Subsemigroup.subset_closure, Iff.mp, NonUnitalSubsemiring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
⊢ (↑(closure s) : Set R) = (↑(AddSubmonoid.closure (↑(Subsemigroup.closure s) : Set R)) : Set R)

Tactic:
simp [← Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid,
    Subsemigroup.nonUnitalSubsemiringClosure_eq_closure]

Premises used: Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid, Subsemigroup.nonUnitalSubsemiringClosure_eq_closure
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
x : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x ↔
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Subsemigroup.closure s) : Set R)) x

Tactic:
Set.ext_iff.mp (coe_closure_eq s) x

Premises used: Iff.mp, Set.ext_iff, NonUnitalSubsemiring.coe_closure_eq
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
h :
  ∀ (x : R),
    Membership.mem (γ := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x ↔
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x
⊢ Eq (α := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) (closure s)

Tactic:
ext x
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
x : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x ↔
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x

Tactic:
⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩

Premises used: AddSubmonoid.subset_closure, NonUnitalSubsemiring.closure_mono, Iff.intro
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
x : R
h :
  ∀ (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x),
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x ↔
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x

Tactic:
refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x
H : NonUnitalSubsemiring R
J : Membership.mem (γ := Set (NonUnitalSubsemiring R)) {S : NonUnitalSubsemiring R | s ⊆ (↑S : Set R)} H
⊢ Membership.mem (γ := Set R)
    ((fun (h : Membership.mem (γ := Set (NonUnitalSubsemiring R)) {S : NonUnitalSubsemiring R | s ⊆ (↑S : Set R)} H) ↦
        (↑H : Set R))
      J)
    x

Tactic:
(AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => ?_

Premises used: Set.Mem, NonUnitalSubsemiring.toAddSubmonoid, AddSubmonoid.mem_closure, Iff.mp, NonUnitalSubsemiring.mem_closure_iff
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x
H : NonUnitalSubsemiring R
J : Membership.mem (γ := Set (NonUnitalSubsemiring R)) {S : NonUnitalSubsemiring R | s ⊆ (↑S : Set R)} H
h :
  ∀ (y : R) (hy : y ∈ (↑(Subsemigroup.closure (↑(AddSubmonoid.closure s) : Set R)) : Set R)),
    y ∈ (↑H.toAddSubmonoid : Set R)
⊢ Membership.mem (γ := Set R)
    ((fun (h : Membership.mem (γ := Set (NonUnitalSubsemiring R)) {S : NonUnitalSubsemiring R | s ⊆ (↑S : Set R)} H) ↦
        (↑H : Set R))
      J)
    x

Tactic:
refine (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => ?_

Premises used: NonUnitalSubsemiring.toAddSubmonoid, AddSubmonoid.mem_closure, Iff.mp, NonUnitalSubsemiring.mem_closure_iff
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x
H : NonUnitalSubsemiring R
J : Membership.mem (γ := Set (NonUnitalSubsemiring R)) {S : NonUnitalSubsemiring R | s ⊆ (↑S : Set R)} H
y : R
hy : y ∈ (↑(Subsemigroup.closure (↑(AddSubmonoid.closure s) : Set R)) : Set R)
⊢ y ∈ (↑H.toAddSubmonoid : Set R)

Tactic:
(Subsemigroup.mem_closure.mp hy) H.toSubsemigroup fun z hz => ?_

Premises used: NonUnitalSubsemiring.toSubsemigroup, Set.Mem, Subsemigroup.mem_closure, Iff.mp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x
H : NonUnitalSubsemiring R
J : Membership.mem (γ := Set (NonUnitalSubsemiring R)) {S : NonUnitalSubsemiring R | s ⊆ (↑S : Set R)} H
y : R
hy : y ∈ (↑(Subsemigroup.closure (↑(AddSubmonoid.closure s) : Set R)) : Set R)
h : ∀ (z : R) (hz : z ∈ (↑(AddSubmonoid.closure s) : Set R)), z ∈ (↑H.toSubsemigroup : Set R)
⊢ y ∈ (↑H.toAddSubmonoid : Set R)

Tactic:
refine (Subsemigroup.mem_closure.mp hy) H.toSubsemigroup fun z hz => ?_

Premises used: NonUnitalSubsemiring.toSubsemigroup, Subsemigroup.mem_closure, Iff.mp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x
H : NonUnitalSubsemiring R
J : Membership.mem (γ := Set (NonUnitalSubsemiring R)) {S : NonUnitalSubsemiring R | s ⊆ (↑S : Set R)} H
y : R
hy : y ∈ (↑(Subsemigroup.closure (↑(AddSubmonoid.closure s) : Set R)) : Set R)
z : R
hz : z ∈ (↑(AddSubmonoid.closure s) : Set R)
⊢ z ∈ (↑H.toSubsemigroup : Set R)

Tactic:
(AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

Premises used: Set.Mem, NonUnitalSubsemiring.toAddSubmonoid, AddSubmonoid.mem_closure, Iff.mp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x
H : NonUnitalSubsemiring R
J : Membership.mem (γ := Set (NonUnitalSubsemiring R)) {S : NonUnitalSubsemiring R | s ⊆ (↑S : Set R)} H
y : R
hy : y ∈ (↑(Subsemigroup.closure (↑(AddSubmonoid.closure s) : Set R)) : Set R)
z : R
hz : z ∈ (↑(AddSubmonoid.closure s) : Set R)
⊢ z ∈ (↑H.toSubsemigroup : Set R)

Tactic:
exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

Premises used: NonUnitalSubsemiring.toAddSubmonoid, AddSubmonoid.mem_closure, Iff.mp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p : (x : R) → Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x → Prop
mem : ∀ (x : R) (hx : x ∈ s), p x ⋯
zero : p 0 ⋯
add :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y), p x hx → p y hy → p (x + y) ⋯
mul :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x
⊢ p x hx

Tactic:
let K : NonUnitalSubsemiring R :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      zero_mem' := ⟨_, zero⟩ }
  closure_le (t := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, HMul.hMul, NonUnitalSubsemiring.subset_closure, _private.0.NonUnitalSubsemiring.closure_induction.match_1, setOf, Membership.mem, Exists, id, NonUnitalSubsemiring.mk, AddSubmonoid.mk, AddSubsemigroup.mk, NonUnitalSubsemiring.closure, HAdd.hAdd, Exists.intro, AddMemClass.add_mem, NonUnitalSubsemiring.closure_le, ZeroMemClass.zero_mem, Exists.elim, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
x_1 : R
h : x_1 ∈ s
⊢ p x_1 z ⋯ ⋯

Tactic:
mem_mem _ h _ hz
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
x_1 : R
h : x_1 ∈ s
⊢ p x_1 z ⋯ ⋯

Tactic:
exact mem_mem _ h _ hz
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
⊢ p 0 z ⋯ ⋯

Tactic:
zero_left _ _
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
⊢ p 0 z ⋯ ⋯

Tactic:
exact zero_left _ _
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring 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 (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
x_1 y_1 : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x_1
hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y_1
h₁ : p x_1 z hx ⋯
h₂ : p y_1 z hy ⋯
⊢ p (x_1 * y_1) z ⋯ ⋯

Tactic:
mul_left _ _ _ _ _ _ h₁ h₂