awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ GaloisConnection (β := NonUnitalSubalgebra R A) (adjoin R) SetLike.coe

Tactic:
fun s S =>
  ⟨fun H => (NonUnitalSubsemiring.subset_closure.trans Submodule.subset_span).trans H,
    fun H => show Submodule.span R _ ≤ S.toSubmodule from Submodule.span_le.mpr <|
      show NonUnitalSubsemiring.closure s ≤ S.toNonUnitalSubsemiring from
        NonUnitalSubsemiring.closure_le.2 H⟩

Premises used: Iff.mpr, NonUnitalSubsemiring.subset_closure, HasSubset.Subset.trans, Iff.intro, NonUnitalSubsemiring.closure_le, Submodule.subset_span, Submodule.span_le, GaloisConnection
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
s : Set A
hs : s ⊆ (↑S : Set A)
⊢ adjoin R s ≤ S

Tactic:
NonUnitalAlgebra.gc.l_le hs

Premises used: NonUnitalAlgebra.gc, GaloisConnection.l_le
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
s : Set A
⊢ adjoin R s ≤ S ↔ s ⊆ (↑S : Set A)

Tactic:
NonUnitalAlgebra.gc _ _

Premises used: NonUnitalAlgebra.gc
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s t : Set A
H : s ⊆ t
⊢ LE.le (α := NonUnitalSubalgebra R A) (adjoin R s) (adjoin R t)

Tactic:
NonUnitalAlgebra.gc.monotone_l H

Premises used: NonUnitalAlgebra.gc, GaloisConnection.monotone_l
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s t : Set A
⊢ Eq (α := NonUnitalSubalgebra R A) (adjoin R (s ∪ t)) (adjoin R s ⊔ adjoin R t)

Tactic:
(NonUnitalAlgebra.gc : GaloisConnection _ ((↑) : NonUnitalSubalgebra R A → Set A)).l_sup

Premises used: NonUnitalAlgebra.gc, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : NonUnitalSubalgebra R A
⊢ adjoin R (↑s : Set A) = s

Tactic:
le_antisymm (adjoin_le le_rfl) (subset_adjoin R)

Premises used: NonUnitalAlgebra.adjoin_le, le_rfl, NonUnitalAlgebra.subset_adjoin, le_antisymm
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p : (x : A) → Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x hx → p (r • x) ⋯
x : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
⊢ p x hx

Tactic:
let S : NonUnitalSubalgebra R A :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem' := (Exists.elim · fun _ ha ↦ (Exists.elim · fun _ hb ↦ ⟨_, mul _ _ _ _ ha hb⟩))
      add_mem' := (Exists.elim · fun _ ha ↦ (Exists.elim · fun _ hb ↦ ⟨_, add _ _ _ _ ha hb⟩))
      smul_mem' := fun r ↦ (Exists.elim · fun _ hb ↦ ⟨_, smul r _ _ hb⟩)
      zero_mem' := ⟨_, zero⟩ }
  adjoin_le (S := S) (fun y hy ↦ ⟨subset_adjoin R hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: SMulMemClass.smul_mem, NonUnitalAlgebra.adjoin_le, NonUnitalAlgebra.subset_adjoin, setOf, NonUnitalAlgebra.adjoin, Exists, id, NonUnitalSubsemiring.mk, AddSubmonoid.mk, AddSubsemigroup.mk, NonUnitalSubalgebra.mk, Exists.intro, AddMemClass.add_mem, ZeroMemClass.zero_mem, Exists.elim, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y z : A
hz : z ∈ s
x_1 : A
h : x_1 ∈ s
⊢ p x_1 z ⋯ ⋯

Tactic:
mem_mem _ _ h hz
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y z : A
hz : z ∈ s
x_1 : A
h : x_1 ∈ s
⊢ p x_1 z ⋯ ⋯

Tactic:
exact mem_mem _ _ h hz
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y z : A
hz : z ∈ s
⊢ p 0 z ⋯ ⋯

Tactic:
zero_left _ _
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y z : A
hz : z ∈ s
⊢ p 0 z ⋯ ⋯

Tactic:
exact zero_left _ _
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y z : A
hz : z ∈ s
x_1 y_1 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R 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.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y z : A
hz : z ∈ s
x_1 y_1 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R 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₂
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y z : A
hz : z ∈ s
x_1 y_1 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y_1
h₁ : p x_1 z hx ⋯
h₂ : p y_1 z hy ⋯
⊢ p (x_1 + y_1) z ⋯ ⋯

Tactic:
add_left _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y z : A
hz : z ∈ s
x_1 y_1 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y_1
h₁ : p x_1 z hx ⋯
h₂ : p y_1 z hy ⋯
⊢ p (x_1 + y_1) z ⋯ ⋯

Tactic:
exact add_left _ _ _ _ _ _ h₁ h₂