-- Mathlib/LinearAlgebra/TensorProduct/Tower.lean
@[simp]
lemma baseChange_top : (⊤ : Submodule R M).baseChange A = ⊤

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
x : A ⊗[R] M
a : A
y : M
⊢ a ⊗ₜ[R] y ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))

Tactic:
rw [← mul_one a, ← smul_eq_mul, ← smul_tmul']

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
x : A ⊗[R] M
a : A
y : M
⊢ a • 1 ⊗ₜ[R] y ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))

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
⊢ ∀ (x : A ⊗[R] M), x ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))

Tactic:
intro x

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
x : A ⊗[R] M
⊢ x ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))

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
⊢ baseChange A ⊤ = ⊤

Tactic:
rw [baseChange, map_top, eq_top_iff']

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
⊢ ∀ (x : A ⊗[R] M), x ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))

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
x : A ⊗[R] M
a : A
y : M
⊢ 1 ⊗ₜ[R] y ∈ ↑(LinearMap.range ((TensorProduct.mk R A M) 1))

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
x : A ⊗[R] M
a : A
y : M
⊢ a • 1 ⊗ₜ[R] y ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))

Tactic:
refine smul_mem _ _ (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
x : A ⊗[R] M
a : A
y : M
⊢ 1 ⊗ₜ[R] y ∈ ↑(LinearMap.range ((TensorProduct.mk R A M) 1))

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
x : A ⊗[R] M
⊢ 0 ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))

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
x : A ⊗[R] M
⊢ x ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))

Tactic:
refine x.induction_on (by simp) (fun a y ↦ ?_) (fun _ _ ↦ Submodule.add_mem _)

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
x : A ⊗[R] M
a : A
y : M
⊢ a ⊗ₜ[R] y ∈ span A ↑(LinearMap.range ((TensorProduct.mk R A M) 1))