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
s : NonUnitalSubalgebra R A
⊢ Submodule.span R (↑s : Set A) = s.toSubmodule

Tactic:
simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]

Premises used: SetLike.ext'_iff, Submodule.coe_span_eq_self
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (a * b)

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ ha

Premises used: Submodule.span_induction
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
refine_1 :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)
refine_2 : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (0 * b)
refine_3 :
  ∀ (x y : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b) →
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (y * b) →
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) ((x + y) * b)
refine_4 :
  ∀ (a : R) (x : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b) →
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (a • x * b)
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (a * b)

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ ha
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ hb

Premises used: Submodule.span_induction
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
refine_1 :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 : A)
    (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)
refine_1₁ :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * 0)
refine_1₂ :
  ∀ (x y : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) y),
    (∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)) →
      (∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
          Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * y)) →
        ∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
          Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A))
            (x_1 * (x + y))
refine_1₃ :
  ∀ (a : R) (x : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x),
    (∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)) →
      ∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * a • x)
⊢ ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hb
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 : A)
    (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)

Tactic:
fun x (hx : x ∈ NonUnitalSubsemiring.closure s) y
              (hy : y ∈ NonUnitalSubsemiring.closure s) => Submodule.subset_span (mul_mem hy hx)

Premises used: Submodule.subset_span, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 : A)
    (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)

Tactic:
exact fun x (hx : x ∈ NonUnitalSubsemiring.closure s) y
              (hy : y ∈ NonUnitalSubsemiring.closure s) => Submodule.subset_span (mul_mem hy hx)

Premises used: Submodule.subset_span, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * 0)

Tactic:
fun x _hx => (mul_zero x).symm ▸ Submodule.zero_mem _

Premises used: Set.Mem, Eq.rec, MulZeroClass.mul_zero, NonUnitalSubsemiring.closure, SetLike.coe, Submodule.zero_mem, Submodule.span, Eq.symm
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * 0)

Tactic:
exact fun x _hx => (mul_zero x).symm ▸ Submodule.zero_mem _
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (x y : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) y),
    (∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)) →
      (∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
          Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * y)) →
        ∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
          Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A))
            (x_1 * (x + y))

Tactic:
fun x y _ _ hx hy z hz => (mul_add z x y).symm ▸ add_mem (hx z hz) (hy z hz)

Premises used: Set.Mem, Eq.rec, AddMemClass.add_mem, mul_add, Eq.symm
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (x y : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) y),
    (∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)) →
      (∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
          Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * y)) →
        ∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
          Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A))
            (x_1 * (x + y))

Tactic:
exact fun x y _ _ hx hy z hz => (mul_add z x y).symm ▸ add_mem (hx z hz) (hy z hz)
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (a : R) (x : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x),
    (∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)) →
      ∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * a • x)

Tactic:
fun r x _ hx y hy =>
              (mul_smul_comm r y x).symm ▸ SMulMemClass.smul_mem r (hx y hy)

Premises used: SMulMemClass.smul_mem, Eq.rec, mul_smul_comm, Eq.symm
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (a : R) (x : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x),
    (∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)) →
      ∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * a • x)

Tactic:
exact fun r x _ hx y hy =>
              (mul_smul_comm r y x).symm ▸ SMulMemClass.smul_mem r (hx y hy)
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (0 * b)

Tactic:
(zero_mul b).symm ▸ Submodule.zero_mem _

Premises used: Set.Mem, MulZeroClass.zero_mul, Eq.rec, Submodule.zero_mem, Eq.symm
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (0 * b)

Tactic:
exact (zero_mul b).symm ▸ Submodule.zero_mem _
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (x y : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b) →
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (y * b) →
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) ((x + y) * b)

Tactic:
fun x y _ _ => (add_mul x y b).symm ▸ add_mem

Premises used: add_mul, Set.Mem, Eq.rec, AddMemClass.add_mem, Eq.symm
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (x y : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b) →
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (y * b) →
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) ((x + y) * b)

Tactic:
exact fun x y _ _ => (add_mul x y b).symm ▸ add_mem
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (a : R) (x : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b) →
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (a • x * b)

Tactic:
fun r x _ hx => (smul_mul_assoc r x b).symm ▸ SMulMemClass.smul_mem r hx

Premises used: SMulMemClass.smul_mem, Eq.rec, smul_mul_assoc, Eq.symm
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (a : R) (x : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b) →
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (a • x * b)

Tactic:
exact fun r x _ hx => (smul_mul_assoc r x b).symm ▸ SMulMemClass.smul_mem r 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
⊢ Eq (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s))
    (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A))

Tactic:
rfl

Premises used: Submodule.span, rfl
-- 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
⊢ s ⊆ (↑(adjoin R s) : Set A)

Tactic:
NonUnitalSubsemiring.subset_closure.trans Submodule.subset_span

Premises used: NonUnitalSubsemiring.subset_closure, HasSubset.Subset.trans, 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 : A
hx : x ∈ s
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x

Tactic:
subset_adjoin R hx

Premises used: NonUnitalAlgebra.subset_adjoin
-- 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
x : A
⊢ Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R {x}) x

Tactic:
NonUnitalAlgebra.subset_adjoin R (Set.mem_singleton x)

Premises used: Set.mem_singleton, NonUnitalAlgebra.subset_adjoin