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

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
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype ∘ₗ LinearMap.rTensor (↥N') w✝.subtype))
⊢ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))

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

Result:
no goals

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
⊢ ∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))

Tactic:
obtain ⟨_, N', _, 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
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl w✝ N'))
⊢ ∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.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
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl w✝ N'))
⊢ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))

Tactic:
rw [mapIncl, ← LinearMap.lTensor_comp_rTensor] 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
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype ∘ₗ LinearMap.rTensor (↥N') w✝.subtype))
⊢ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.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
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl w✝ N'))
⊢ ∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))

Tactic:
refine ⟨N', 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
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl w✝ N'))
⊢ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))