awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x : R
hx : Membership.mem (γ := Subsemiring R) (Subsemiring.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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
⊢ Eq (α := Subsemiring R) (closure (↑(Submonoid.closure s) : Set R)) (closure s)

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

Premises used: Iff.mpr, Subsemiring.closure_le, Subsemiring.closure_mono, Submonoid.mem_closure, Subsemiring.closure, Subsemiring.subset_closure, Subsemiring.toSubmonoid, le_antisymm, Iff.mp, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
⊢ (↑(closure s) : Set R) = (↑(AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) : Set R)

Tactic:
simp [← Submonoid.subsemiringClosure_toAddSubmonoid, Submonoid.subsemiringClosure_eq_closure]

Premises used: Submonoid.subsemiringClosure_toAddSubmonoid, Submonoid.subsemiringClosure_eq_closure
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
x : R
⊢ Membership.mem (γ := Subsemiring R) (closure s) x ↔
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) x

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

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

Tactic:
ext x
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
x : R
⊢ Membership.mem (γ := Subsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x ↔
    Membership.mem (γ := Subsemiring R) (closure s) x

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

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

Tactic:
refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
x : R
hx : Membership.mem (γ := Subsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x
H : Subsemiring R
J : Membership.mem (γ := Set (Subsemiring R)) {S : Subsemiring R | s ⊆ (↑S : Set R)} H
⊢ Membership.mem (γ := Set R)
    ((fun (h : Membership.mem (γ := Set (Subsemiring R)) {S : Subsemiring 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, AddSubmonoid.mem_closure, Iff.mp, Subsemiring.toAddSubmonoid, Subsemiring.mem_closure_iff
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
x : R
hx : Membership.mem (γ := Subsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x
H : Subsemiring R
J : Membership.mem (γ := Set (Subsemiring R)) {S : Subsemiring R | s ⊆ (↑S : Set R)} H
h :
  ∀ (y : R) (hy : y ∈ (↑(Submonoid.closure (↑(AddSubmonoid.closure s) : Set R)) : Set R)),
    y ∈ (↑H.toAddSubmonoid : Set R)
⊢ Membership.mem (γ := Set R)
    ((fun (h : Membership.mem (γ := Set (Subsemiring R)) {S : Subsemiring 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: AddSubmonoid.mem_closure, Iff.mp, Subsemiring.toAddSubmonoid, Subsemiring.mem_closure_iff
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
x : R
hx : Membership.mem (γ := Subsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x
H : Subsemiring R
J : Membership.mem (γ := Set (Subsemiring R)) {S : Subsemiring R | s ⊆ (↑S : Set R)} H
y : R
hy : y ∈ (↑(Submonoid.closure (↑(AddSubmonoid.closure s) : Set R)) : Set R)
⊢ y ∈ (↑H.toAddSubmonoid : Set R)

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

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

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

Premises used: Submonoid.mem_closure, Subsemiring.toSubmonoid, Iff.mp
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
x : R
hx : Membership.mem (γ := Subsemiring R) (closure (↑(AddSubmonoid.closure s) : Set R)) x
H : Subsemiring R
J : Membership.mem (γ := Set (Subsemiring R)) {S : Subsemiring R | s ⊆ (↑S : Set R)} H
y : R
hy : y ∈ (↑(Submonoid.closure (↑(AddSubmonoid.closure s) : Set R)) : Set R)
z : R
hz : z ∈ (↑(AddSubmonoid.closure s) : Set R)
⊢ z ∈ (↑H.toSubmonoid : Set R)

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

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

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

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

Tactic:
let K : Subsemiring R :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      one_mem' := ⟨_, one⟩
      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, Subsemiring.closure_le, HMul.hMul, _private.0.Subsemiring.closure_induction.match_1, Subsemiring.closure, Subsemigroup.mk, setOf, Membership.mem, Exists, Subsemiring.subset_closure, id, HAdd.hAdd, Subsemiring.mk, Exists.intro, AddMemClass.add_mem, Submonoid.mk, ZeroMemClass.zero_mem, OneMemClass.one_mem, Exists.elim, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := Subsemiring R) (closure s) x → Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := Subsemiring R) (closure s) x → Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := Subsemiring R) (closure s) x → Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := Subsemiring R) (closure s) x → Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := Subsemiring R) (closure s) x → Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 1 z ⋯ ⋯

Tactic:
one_left _ _
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := Subsemiring R) (closure s) x → Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 1 z ⋯ ⋯

Tactic:
exact one_left _ _
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := Subsemiring R) (closure s) x → Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x_1
hy : Membership.mem (γ := Subsemiring 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₂
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := Subsemiring R) (closure s) x → Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x)
    (hy : Membership.mem (γ := Subsemiring R) (closure s) y) (hz : Membership.mem (γ := Subsemiring 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 (γ := Subsemiring R) (closure s) x_1
hy : Membership.mem (γ := Subsemiring R) (closure s) y_1
h₁ : p x_1 z hx ⋯
h₂ : p y_1 z hy ⋯
⊢ p (x_1 * y_1) z ⋯ ⋯

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