-- Mathlib/RingTheory/TensorProduct/Basic.lean
@[simp]
lemma range_liftBaseChange (l : M →ₗ[R] N) :
    LinearMap.range (l.liftBaseChange A) = Submodule.span A (LinearMap.range l)

Proof state:
case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ range (liftBaseChange A l) ≤ Submodule.span A ↑(range l)

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case a.intro
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x : A ⊗[R] M
⊢ (liftBaseChange A l) x ∈ Submodule.span A ↑(range l)

Proof state:
case a.intro.tmul
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ : A
y✝ : M
⊢ x✝ • l y✝ ∈ Submodule.span A ↑(range l)

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨_, rfl⟩)

Result:
no goals

Proof state:
case a.intro
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x : A ⊗[R] M
⊢ (liftBaseChange A l) x ∈ Submodule.span A ↑(range l)

Tactic:
induction x using TensorProduct.induction_on

Result:
case a.intro.zero
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ (liftBaseChange A l) 0 ∈ Submodule.span A ↑(range l)

case a.intro.tmul
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ : A
y✝ : M
⊢ (liftBaseChange A l) (x✝ ⊗ₜ[R] y✝) ∈ Submodule.span A ↑(range l)

case a.intro.add
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ y✝ : A ⊗[R] M
a✝¹ : (liftBaseChange A l) x✝ ∈ Submodule.span A ↑(range l)
a✝ : (liftBaseChange A l) y✝ ∈ Submodule.span A ↑(range l)
⊢ (liftBaseChange A l) (x✝ + y✝) ∈ Submodule.span A ↑(range l)

Proof state:
case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ Submodule.span A ↑(range l) ≤ range (liftBaseChange A l)

Tactic:
rw [Submodule.span_le]

Result:
case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ ↑(range l) ⊆ ↑(range (liftBaseChange A l))

Proof state:
case a.intro
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x : M
⊢ l x ∈ ↑(range (liftBaseChange A l))

Tactic:
exact ⟨1 ⊗ₜ x, by simp⟩

Result:
no goals

Proof state:
case a.intro.add
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ y✝ : A ⊗[R] M
a✝¹ : (liftBaseChange A l) x✝ ∈ Submodule.span A ↑(range l)
a✝ : (liftBaseChange A l) y✝ ∈ Submodule.span A ↑(range l)
⊢ (liftBaseChange A l) (x✝ + y✝) ∈ Submodule.span A ↑(range l)

Tactic:
rw [map_add]

Result:
case a.intro.add
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ y✝ : A ⊗[R] M
a✝¹ : (liftBaseChange A l) x✝ ∈ Submodule.span A ↑(range l)
a✝ : (liftBaseChange A l) y✝ ∈ Submodule.span A ↑(range l)
⊢ (liftBaseChange A l) x✝ + (liftBaseChange A l) y✝ ∈ Submodule.span A ↑(range l)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ range (liftBaseChange A l) = Submodule.span A ↑(range l)

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ range (liftBaseChange A l) ≤ Submodule.span A ↑(range l)

case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ Submodule.span A ↑(range l) ≤ range (liftBaseChange A l)

Proof state:
case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ ↑(range l) ⊆ ↑(range (liftBaseChange A l))

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case a.intro
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x : M
⊢ l x ∈ ↑(range (liftBaseChange A l))

Proof state:
case a.intro.add
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ y✝ : A ⊗[R] M
a✝¹ : (liftBaseChange A l) x✝ ∈ Submodule.span A ↑(range l)
a✝ : (liftBaseChange A l) y✝ ∈ Submodule.span A ↑(range l)
⊢ (liftBaseChange A l) x✝ + (liftBaseChange A l) y✝ ∈ Submodule.span A ↑(range l)

Tactic:
exact add_mem ‹_› ‹_›

Result:
no goals