awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hsur : Function.Surjective.{u + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
X : Set M
refine :
  ∀ (m : M) (hm : Membership.mem (γ := Submodule R M) (restrictScalars R (span A X)) m),
    Membership.mem (γ := Submodule R M) (span R X) m
⊢ Eq (α := Submodule R M) (restrictScalars R (span A X)) (span R X)

Tactic:
refine ((span_le_restrictScalars R A X).antisymm fun m hm => ?_).symm

Premises used: Submodule.span_le_restrictScalars, LE.le.antisymm, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hsur : Function.Surjective.{u + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
X : Set M
m : M
hm : Membership.mem (γ := Submodule R M) (restrictScalars R (span A X)) m
⊢ Membership.mem (γ := Submodule R M) (span R X) m

Tactic:
span_induction subset_span (zero_mem _) (fun _ _ _ _ => add_mem) (fun a m _ hm => ?_) hm

Premises used: Submodule.span_induction
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hsur : Function.Surjective.{u + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
X : Set M
m : M
hm : Membership.mem (γ := Submodule R M) (restrictScalars R (span A X)) m
refine :
  ∀ (a : A) (m : M),
    Membership.mem (γ := Submodule A M) (span A X) m →
      ∀ (hm : Membership.mem (γ := Submodule R M) (span R X) m), Membership.mem (γ := Submodule R M) (span R X) (a • m)
⊢ Membership.mem (γ := Submodule R M) (span R X) m

Tactic:
refine span_induction subset_span (zero_mem _) (fun _ _ _ _ => add_mem) (fun a m _ hm => ?_) hm
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hsur : Function.Surjective.{u + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
X : Set M
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (restrictScalars R (span A X)) m_1
a : A
m : M
h : Membership.mem (γ := Submodule A M) (span A X) m
hm : Membership.mem (γ := Submodule R M) (span R X) m
obtain :
  ∀ (r : R),
    Membership.mem (γ := Submodule R M) (span R X)
      (HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) m)
⊢ Membership.mem (γ := Submodule R M) (span R X) (a • m)

Tactic:
obtain ⟨r, rfl⟩ := hsur a

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hsur : Function.Surjective.{u + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
X : Set M
m_1 : M
hm_1 : Membership.mem (γ := Submodule R M) (restrictScalars R (span A X)) m_1
m : M
h : Membership.mem (γ := Submodule A M) (span A X) m
hm : Membership.mem (γ := Submodule R M) (span R X) m
r : R
⊢ Membership.mem (γ := Submodule R M) (span R X)
    (HSMul.hSMul.{w, v₁, v₁} (α := A) ((algebraMap R A : (a : R) → A) r : A) m)

Tactic:
simpa [algebraMap_smul] using smul_mem _ r hm

Premises used: algebraMap_smul, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
A : Type w
M : Type v₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
h : Function.Surjective.{u + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
s : Set M
⊢ (↑(span A s) : Set M) = (↑(span R s) : Set M)

Tactic:
congr_arg ((↑) : Submodule R M → Set M) (Submodule.restrictScalars_span R A h s)

Premises used: iInf, Set.iInter, setOf, congr_arg, SetLike.coe, Submodule.restrictScalars_span
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R_1 : Type u
S_1 : Type v
A : Type w
B : Type u₁
M_1 : Type v₁
inst : CommSemiring R_1
inst_1 : Semiring A
inst_2 : Algebra R_1 A
inst_3 : AddCommMonoid M_1
inst_4 : Module R_1 M_1
inst_5 : Module A M_1
inst_6 : IsScalarTower R_1 A M_1
R : Type u_1
S : Type u_2
M : Type u_3
inst_7 : CommRing R
inst_8 : Ring S
inst_9 : AddCommGroup M
inst_10 : Algebra R S
inst_11 : Module R M
inst_12 : Module S M
inst_13 : IsScalarTower R S M
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
N : Submodule R M
⊢ ∀ (c : S) {x : M}, x ∈ N.carrier → c • x ∈ N.carrier

Tactic:
simpa [h.forall] using N.2

Premises used: Function.Surjective.forall, Submodule.smul_mem'
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
rw : Membership.mem (γ := Submodule R A) (span R (s • t)) 0
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (HSMul.hSMul.{v, w, w} (α := S) 0 x)

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
c₁ c₂ : S
h : Membership.mem (γ := Submodule R S) (span R s) c₁
h_1 : Membership.mem (γ := Submodule R S) (span R s) c₂
ih₁ : Membership.mem (γ := Submodule R A) (span R (s • t)) (c₁ • x)
ih₂ : Membership.mem (γ := Submodule R A) (span R (s • t)) (c₂ • x)
rw : Membership.mem (γ := Submodule R A) (span R (s • t)) (c₁ • x + c₂ • x)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) ((c₁ + c₂) • x)

Tactic:
rw [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
c₁ c₂ : S
h : Membership.mem (γ := Submodule R S) (span R s) c₁
h_1 : Membership.mem (γ := Submodule R S) (span R s) c₂
ih₁ : Membership.mem (γ := Submodule R A) (span R (s • t)) (c₁ • x)
ih₂ : Membership.mem (γ := Submodule R A) (span R (s • t)) (c₂ • x)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (c₁ • x + c₂ • x)

Tactic:
add_mem ih₁ ih₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
c₁ c₂ : S
h : Membership.mem (γ := Submodule R S) (span R s) c₁
h_1 : Membership.mem (γ := Submodule R S) (span R s) c₂
ih₁ : Membership.mem (γ := Submodule R A) (span R (s • t)) (c₁ • x)
ih₂ : Membership.mem (γ := Submodule R A) (span R (s • t)) (c₂ • x)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (c₁ • x + c₂ • x)

Tactic:
exact add_mem ih₁ ih₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
b : R
c : S
h : Membership.mem (γ := Submodule R S) (span R s) c
hc : Membership.mem (γ := Submodule R A) (span R (s • t)) (c • x)
rw : Membership.mem (γ := Submodule R A) (span R (s • t)) (b • c • x)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) ((b • c) • x)

Tactic:
rw [IsScalarTower.smul_assoc]

Premises used: IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
b : R
c : S
h : Membership.mem (γ := Submodule R S) (span R s) c
hc : Membership.mem (γ := Submodule R A) (span R (s • t)) (c • x)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (b • c • x)

Tactic:
smul_mem _ _ hc

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : Membership.mem (γ := Submodule R S) (span R s) k
x : A
hx : x ∈ t
b : R
c : S
h : Membership.mem (γ := Submodule R S) (span R s) c
hc : Membership.mem (γ := Submodule R A) (span R (s • t)) (c • x)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (b • c • x)

Tactic:
exact smul_mem _ _ hc

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x_1 : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x_1
s0 : S
y : A
hy : y ∈ t
x : S
hx : x ∈ s
⊢ x • y ∈ s • t

Tactic:
⟨x, hx, y, hy, rfl⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x_1 : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x_1
s0 : S
y : A
hy : y ∈ t
x : S
hx : x ∈ s
⊢ x • y ∈ s • t

Tactic:
exact ⟨x, hx, y, hy, rfl⟩
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
refine_1 : Membership.mem (γ := Submodule R A) (span R (s • t)) (HSMul.hSMul.{v, w, w} (α := S) 0 y)
refine_2 :
  ∀ (x y_1 : S) (hx : Membership.mem (γ := Submodule R S) (span R s) x)
    (hy : Membership.mem (γ := Submodule R S) (span R s) y_1),
    Membership.mem (γ := Submodule R A) (span R (s • t)) (x • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
        Membership.mem (γ := Submodule R A) (span R (s • t)) ((x + y_1) • y)
refine_3 :
  ∀ (a : R) (x : S) (hx : Membership.mem (γ := Submodule R S) (span R s) x),
    Membership.mem (γ := Submodule R A) (span R (s • t)) (x • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) ((a • x) • y)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (s0 • y)

Tactic:
refine span_induction (fun x hx ↦ subset_span <| by exact ⟨x, hx, y, hy, rfl⟩) ?_ ?_ ?_
        (hs ▸ mem_top : s0 ∈ span R s)
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
refine_1 : Membership.mem (γ := Submodule R A) (span R (s • t)) 0
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (HSMul.hSMul.{v, w, w} (α := S) 0 y)

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) 0

Tactic:
apply zero_mem

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
x_1 : S
refine_2 :
  ∀ (y_1 : S) (hx : Membership.mem (γ := Submodule R S) (span R s) x_1)
    (hy : Membership.mem (γ := Submodule R S) (span R s) y_1),
    Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
        Membership.mem (γ := Submodule R A) (span R (s • t)) ((x_1 + y_1) • y)
⊢ ∀ (y_1 : S) (hx : Membership.mem (γ := Submodule R S) (span R s) x_1)
    (hy : Membership.mem (γ := Submodule R S) (span R s) y_1),
    Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
        Membership.mem (γ := Submodule R A) (span R (s • t)) ((x_1 + y_1) • y)

Tactic:
_
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
x_1 y_1 : S
refine_2 :
  Membership.mem (γ := Submodule R S) (span R s) x_1 →
    ∀ (hy : Membership.mem (γ := Submodule R S) (span R s) y_1),
      Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
        Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
          Membership.mem (γ := Submodule R A) (span R (s • t)) ((x_1 + y_1) • y)
⊢ ∀ (hx : Membership.mem (γ := Submodule R S) (span R s) x_1) (hy : Membership.mem (γ := Submodule R S) (span R s) y_1),
    Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
        Membership.mem (γ := Submodule R A) (span R (s • t)) ((x_1 + y_1) • y)

Tactic:
_
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
x_1 y_1 : S
hx : Membership.mem (γ := Submodule R S) (span R s) x_1
refine_2 :
  Membership.mem (γ := Submodule R S) (span R s) y_1 →
    Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
        Membership.mem (γ := Submodule R A) (span R (s • t)) ((x_1 + y_1) • y)
⊢ ∀ (hy : Membership.mem (γ := Submodule R S) (span R s) y_1),
    Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
        Membership.mem (γ := Submodule R A) (span R (s • t)) ((x_1 + y_1) • y)

Tactic:
_
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
x_1 y_1 : S
hx : Membership.mem (γ := Submodule R S) (span R s) x_1
hy_1 : Membership.mem (γ := Submodule R S) (span R s) y_1
refine_2 :
  Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
    Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y + y_1 • y)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
    Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) ((x_1 + y_1) • y)

Tactic:
rw [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0 : S
y : A
hy : y ∈ t
x_1 y_1 : S
hx : Membership.mem (γ := Submodule R S) (span R s) x_1
hy_1 : Membership.mem (γ := Submodule R S) (span R s) y_1
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y) →
    Membership.mem (γ := Submodule R A) (span R (s • t)) (y_1 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) (x_1 • y + y_1 • y)

Tactic:
apply add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0_1 : S
y : A
hy : y ∈ t
r : R
s0 : S
refine_3 :
  Membership.mem (γ := Submodule R S) (span R s) s0 →
    Membership.mem (γ := Submodule R A) (span R (s • t)) (s0 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) ((r • s0) • y)
⊢ ∀ (hx : Membership.mem (γ := Submodule R S) (span R s) s0),
    Membership.mem (γ := Submodule R A) (span R (s • t)) (s0 • y) →
      Membership.mem (γ := Submodule R A) (span R (s • t)) ((r • s0) • y)

Tactic:
_
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0_1 : S
y : A
hy_1 : y ∈ t
r : R
s0 : S
hx : Membership.mem (γ := Submodule R S) (span R s) s0
hy : Membership.mem (γ := Submodule R A) (span R (s • t)) (s0 • y)
refine_3 : Membership.mem (γ := Submodule R A) (span R (s • t)) (r • s0 • y)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) ((r • s0) • y)

Tactic:
rw [IsScalarTower.smul_assoc]

Premises used: IsScalarTower.smul_assoc
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0_1 : S
y : A
hy_1 : y ∈ t
r : R
s0 : S
hx : Membership.mem (γ := Submodule R S) (span R s) s0
hy : Membership.mem (γ := Submodule R A) (span R (s • t)) (s0 • y)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (r • s0 • y)

Tactic:
smul_mem _ r hy

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
x : A
hp : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
s0_1 : S
y : A
hy_1 : y ∈ t
r : R
s0 : S
hx : Membership.mem (γ := Submodule R S) (span R s) s0
hy : Membership.mem (γ := Submodule R A) (span R (s • t)) (s0 • y)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (r • s0 • y)

Tactic:
exact smul_mem _ r hy

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
k : S
x : A
hx : Membership.mem (γ := Submodule R A) (span R (s • t)) x
rw :
  ∀ (hx : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x),
    Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) (k • x)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (k • x)

Tactic:
rw [span_smul_of_span_eq_top hs] at hx ⊢

Premises used: Submodule.span_smul_of_span_eq_top
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
k : S
x : A
hx : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
⊢ Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) (k • x)

Tactic:
(span S t).smul_mem k hx

Premises used: iInf, Set.Mem, Set.iInter, setOf, Submodule.span, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
k : S
x : A
hx : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) x
⊢ Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) (k • x)

Tactic:
exact (span S t).smul_mem k hx

Premises used: Submodule.span, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Tower
Goal:
R : Type u
S : Type v
A : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
s : Set S
hs : Eq (α := Submodule R S) (span R s) ⊤
t : Set A
k : S
x : A
hx : Membership.mem (γ := Submodule R A) (span R t) x
rw : Membership.mem (γ := Submodule R A) (restrictScalars R (span S t)) (k • x)
⊢ Membership.mem (γ := Submodule R A) (span R (s • t)) (k • x)

Tactic:
rw [span_smul_of_span_eq_top hs]

Premises used: Submodule.span_smul_of_span_eq_top