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
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
r : R
x_1 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
h : p x_1 z hx ⋯
⊢ p (r • x_1) z ⋯ ⋯

Tactic:
smul_left _ _ _ _ _ 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
r : R
x_1 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
h : p x_1 z hx ⋯
⊢ p (r • x_1) z ⋯ ⋯

Tactic:
exact smul_left _ _ _ _ _ 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 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
⊢ p x 0 hx ⋯

Tactic:
zero_right x hx
-- 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 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
⊢ p x 0 hx ⋯

Tactic:
exact zero_right x hx
-- 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 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
x_1 y_1 : A
hx_1 : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y_1
h₁ : p x x_1 hx hx_1
h₂ : p x y_1 hx hy
⊢ p x (x_1 * y_1) hx ⋯

Tactic:
mul_right _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.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 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
x_1 y_1 : A
hx_1 : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R 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.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 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
x_1 y_1 : A
hx_1 : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R 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.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 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
x_1 y_1 : A
hx_1 : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R 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.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 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
r : R
x_1 : A
hx_1 : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
h : p x x_1 hx hx_1
⊢ p x (r • x_1) hx ⋯

Tactic:
smul_right _ _ _ _ _ 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 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
r : R
x_1 : A
hx_1 : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_1
h : p x x_1 hx hx_1
⊢ p x (r • x_1) hx ⋯

Tactic:
exact smul_right _ _ _ _ _ h