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
a :
  LE.le (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) (span R (↑(Subsemigroup.closure s) : Set A))
a₁ :
  LE.le (α := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (NonUnitalSubalgebra.toSubmodule (adjoin R s))
⊢ Eq (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) (span R (↑(Subsemigroup.closure s) : Set A))

Tactic:
apply le_antisymm

Premises used: 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
x_1 x : A
hx : x ∈ s
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x

Tactic:
subset_span <| Subsemigroup.subset_closure hx

Premises used: Subsemigroup.subset_closure, Submodule.subset_span
-- 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
x_1 x : A
hx : x ∈ s
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x

Tactic:
exact subset_span <| Subsemigroup.subset_closure hx

Premises used: Subsemigroup.subset_closure, Submodule.subset_span
-- 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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x + y)

Tactic:
add_mem hpx hpy

Premises used: AddMemClass.add_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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x + y)

Tactic:
exact add_mem hpx hpy

Premises used: AddMemClass.add_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
x : A
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_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
x : A
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (y : A) (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (0 * y)

Tactic:
simp
-- 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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (x : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * 0)

Tactic:
simp
-- 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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
apply :
  ∀ (x y : A) (hx : x ∈ (↑(Subsemigroup.closure s) : Set A)) (hy : y ∈ (↑(Subsemigroup.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
apply₁ :
  ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (y * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) ((x + y) * z)
apply₂ :
  ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * (y + z))
apply₃ :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (r • x * y)
apply₄ :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * r • y)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)

Tactic:
apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy

Premises used: Submodule.span_induction₂
-- 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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (x y : A) (hx : x ∈ (↑(Subsemigroup.closure s) : Set A)) (hy : y ∈ (↑(Subsemigroup.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)

Tactic:
fun x y hx hy ↦ subset_span <| mul_mem hx hy

Premises used: Submodule.subset_span, 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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (x y : A) (hx : x ∈ (↑(Subsemigroup.closure s) : Set A)) (hy : y ∈ (↑(Subsemigroup.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)

Tactic:
exact fun x y hx hy ↦ subset_span <| mul_mem hx hy

Premises used: Submodule.subset_span, 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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (x y : A) (hx : x ∈ (↑(Subsemigroup.closure s) : Set A)) (hy : y ∈ (↑(Subsemigroup.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)

Tactic:
case Hs => exact fun x y hx hy ↦ subset_span <| mul_mem hx hy

Premises used: Submodule.subset_span, 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
x_1 x_2 y_1 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_2
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y_1
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x_2
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y_1
x y z : A
h : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
h_1 : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
h_2 : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z
hxz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z)
hyz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (y * z)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) ((x + y) * z)

Tactic:
simpa [add_mul] using add_mem hxz hyz

Premises used: add_mul, AddMemClass.add_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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (y * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) ((x + y) * z)

Tactic:
exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
-- 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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (y * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) ((x + y) * z)

Tactic:
case Hadd_l => exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
-- 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
x_1 x_2 y_1 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_2
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y_1
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x_2
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y_1
x y z : A
h : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
h_1 : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
h_2 : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z
hxz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
hyz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * (y + z))

Tactic:
simpa [mul_add] using add_mem hxz hyz

Premises used: AddMemClass.add_mem, mul_add
-- 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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * (y + z))

Tactic:
exact fun x y z _ _ _ hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
-- 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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * (y + z))

Tactic:
case Hadd_r => exact fun x y z _ _ _ hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
-- 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
x_1 x_2 y_1 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_2
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y_1
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x_2
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y_1
r : R
x y : A
h : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
h_1 : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
hxy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (r • x * y)

Tactic:
simpa [smul_mul_assoc] using smul_mem _ _ hxy

Premises used: smul_mul_assoc, Submodule.smul_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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (r : R) (x y : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (r • x * y)

Tactic:
exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
-- 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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (r : R) (x y : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (r • x * y)

Tactic:
case Hsmul_l => exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
-- 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
x_1 x_2 y_1 : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x_2
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y_1
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x_2
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y_1
r : R
x y : A
h : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
h_1 : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
hxy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * r • y)

Tactic:
simpa [mul_smul_comm] using smul_mem _ _ hxy

Premises used: mul_smul_comm, Submodule.smul_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
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ ∀ (r : R) (x y : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * r • y)

Tactic:
exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy