-- Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
theorem exists_finite_submodule_left_of_finite (s : Set (M ⊗[R] N)) (hs : s.Finite) :
    ∃ M' : Submodule R M, Module.Finite R M' ∧ s ⊆ LinearMap.range (M'.subtype.rTensor N)

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w✝ : Submodule R N
hfin : Module.Finite R ↥M'
left✝ : Module.Finite R ↥w✝
h : s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype ∘ₗ LinearMap.lTensor (↥M') w✝.subtype))
⊢ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))

Tactic:
exact h.trans (LinearMap.range_comp_le_range _ _)

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w✝ : Submodule R N
hfin : Module.Finite R ↥M'
left✝ : Module.Finite R ↥w✝
h : s ⊆ ↑(LinearMap.range (mapIncl M' w✝))
⊢ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))

Tactic:
rw [mapIncl, ← LinearMap.rTensor_comp_lTensor] at h

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w✝ : Submodule R N
hfin : Module.Finite R ↥M'
left✝ : Module.Finite R ↥w✝
h : s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype ∘ₗ LinearMap.lTensor (↥M') w✝.subtype))
⊢ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
⊢ ∃ M', Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))

Tactic:
obtain ⟨M', _, hfin, _, h⟩ := exists_finite_submodule_of_finite s hs

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w✝ : Submodule R N
hfin : Module.Finite R ↥M'
left✝ : Module.Finite R ↥w✝
h : s ⊆ ↑(LinearMap.range (mapIncl M' w✝))
⊢ ∃ M', Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w✝ : Submodule R N
hfin : Module.Finite R ↥M'
left✝ : Module.Finite R ↥w✝
h : s ⊆ ↑(LinearMap.range (mapIncl M' w✝))
⊢ ∃ M', Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))

Tactic:
refine ⟨M', hfin, ?_⟩

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w✝ : Submodule R N
hfin : Module.Finite R ↥M'
left✝ : Module.Finite R ↥w✝
h : s ⊆ ↑(LinearMap.range (mapIncl M' w✝))
⊢ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))