-- Mathlib/LinearAlgebra/TensorProduct/Tower.lean
@[simp]
lemma baseChange_span (s : Set M) :
    (span R s).baseChange A = span A (TensorProduct.mk R A M 1 '' s)

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
⊢ ((TensorProduct.mk R A M) 1) m ∈ ↑(span A (⇑((TensorProduct.mk R A M) 1) '' s))

Tactic:
apply span_induction (p := fun m' _ ↦ (1 : A) ⊗ₜ[R] m' ∈ span A (TensorProduct.mk R A M 1 '' s))
  (hx := hm)

Result:
case intro.intro.mem
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
⊢ ∀ (x : M) (h : x ∈ s), (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) x ⋯

case intro.intro.zero
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
⊢ 1 ⊗ₜ[R] 0 ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

case intro.intro.add
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
⊢ ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s),
    (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) x hx →
      (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) y hy →
        (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) (x + y) ⋯

case intro.intro.smul
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
⊢ ∀ (a : R) (x : M) (hx : x ∈ span R s),
    (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) x hx →
      (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) (a • x) ⋯

Proof state:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ baseChange A (span R s) = span A (⇑((TensorProduct.mk R A M) 1) '' s)

Tactic:
simp only [baseChange, map_coe]

Result:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span A (⇑((TensorProduct.mk R A M) 1) '' ↑(span R s)) = span A (⇑((TensorProduct.mk R A M) 1) '' s)

Proof state:
case intro.intro.add
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
⊢ ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s),
    (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) x hx →
      (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) y hy →
        (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) (x + y) ⋯

Tactic:
intro m₁ m₂ _ _ hm₁ hm₂

Result:
case intro.intro.add
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
m₁ m₂ : M
hx✝ : m₁ ∈ span R s
hy✝ : m₂ ∈ span R s
hm₁ : 1 ⊗ₜ[R] m₁ ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
hm₂ : 1 ⊗ₜ[R] m₂ ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
⊢ 1 ⊗ₜ[R] (m₁ + m₂) ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

Proof state:
case intro.intro.mem
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
⊢ ∀ (x : M) (h : x ∈ s), (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) x ⋯

Tactic:
intro m hm

Result:
case intro.intro.mem
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m✝ : M
hm✝ : m✝ ∈ span R s
m : M
hm : m ∈ s
⊢ 1 ⊗ₜ[R] m ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

Proof state:
case intro.intro.zero
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
⊢ 1 ⊗ₜ[R] 0 ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span A (⇑((TensorProduct.mk R A M) 1) '' ↑(span R s)) = span A (⇑((TensorProduct.mk R A M) 1) '' s)

Tactic:
refine le_antisymm (span_le.mpr ?_) (span_mono <| Set.image_subset _ subset_span)

Result:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ⇑((TensorProduct.mk R A M) 1) '' ↑(span R s) ⊆ ↑(span A (⇑((TensorProduct.mk R A M) 1) '' s))

Proof state:
case intro.intro.smul
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
⊢ ∀ (a : R) (x : M) (hx : x ∈ span R s),
    (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) x hx →
      (fun m' x => 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)) (a • x) ⋯

Tactic:
intro r m' _ hm'

Result:
case intro.intro.smul
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
r : R
m' : M
hx✝ : m' ∈ span R s
hm' : 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
⊢ 1 ⊗ₜ[R] (r • m') ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

Proof state:
case intro.intro.add
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
m₁ m₂ : M
hx✝ : m₁ ∈ span R s
hy✝ : m₂ ∈ span R s
hm₁ : 1 ⊗ₜ[R] m₁ ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
hm₂ : 1 ⊗ₜ[R] m₂ ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
⊢ 1 ⊗ₜ[R] m₁ + 1 ⊗ₜ[R] m₂ ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

Tactic:
exact Submodule.add_mem _ hm₁ hm₂

Result:
no goals

Proof state:
case intro.intro.smul
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
r : R
m' : M
hx✝ : m' ∈ span R s
hm' : 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
⊢ 1 ⊗ₜ[R] (r • m') ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)

Tactic:
rw [tmul_smul, ← one_smul A ((1 : A) ⊗ₜ[R] m'), ← smul_assoc]

Result:
case intro.intro.smul
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
hm : m ∈ span R s
r : R
m' : M
hx✝ : m' ∈ span R s
hm' : 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)
⊢ (r • 1) • 1 ⊗ₜ[R] m' ∈ span A (⇑((TensorProduct.mk R A M) 1) '' s)