-- Mathlib/RingTheory/Finiteness/TensorProduct.lean
theorem exists_fg_le_subset_range_rTensor_subtype (s : Set (N ⊗[R] M)) (hs : s.Finite) :
    ∃ (J : Submodule R N) (_ : J.FG), s ⊆ LinearMap.range (rTensor M J.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 (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
x : N ⊗[R] M
hx : x ∈ s
⊢ (rTensor M ((⨆ x, J ↑x).subtype ∘ₗ inclusion ⋯)) (y x) = (rTensor M (J x).subtype) (y x)

Tactic:
rfl

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 (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
⊢ ∃ J, ∃ (_ : J.FG), s ⊆ ↑(range (rTensor M J.subtype))

Tactic:
refine ⟨⨆ x : s, J x, fg_iSup _ fun _ ↦ fg _, fun x hx ↦
  ⟨rTensor M (inclusion <| le_iSup _ ⟨x, hx⟩) (y x), .trans ?_ (eq x).symm⟩⟩

Result:
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 (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
x : N ⊗[R] M
hx : x ∈ s
⊢ (rTensor M (⨆ x, J ↑x).subtype) ((rTensor M (inclusion ⋯)) (y x)) = (rTensor M (J x).subtype) (y x)

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 (N ⊗[R] M)
hs : s.Finite
⊢ ∃ J, ∃ (_ : J.FG), s ⊆ ↑(range (rTensor M J.subtype))

Tactic:
choose J fg y eq using exists_fg_le_eq_rTensor_subtype (R := R) (M := M) (N := N)

Result:
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 (N ⊗[R] M)
hs : s.Finite
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
⊢ ∃ J, ∃ (_ : J.FG), s ⊆ ↑(range (rTensor M J.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 (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
x : N ⊗[R] M
hx : x ∈ s
⊢ (rTensor M (⨆ x, J ↑x).subtype) ((rTensor M (inclusion ⋯)) (y x)) = (rTensor M (J x).subtype) (y x)

Tactic:
rw [← comp_apply, ← rTensor_comp]

Result:
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 (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
x : N ⊗[R] M
hx : x ∈ s
⊢ (rTensor M ((⨆ x, J ↑x).subtype ∘ₗ inclusion ⋯)) (y x) = (rTensor M (J x).subtype) (y x)

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 (N ⊗[R] M)
hs : s.Finite
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
⊢ ∃ J, ∃ (_ : J.FG), s ⊆ ↑(range (rTensor M J.subtype))

Tactic:
rw [← Set.finite_coe_iff] at hs

Result:
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 (N ⊗[R] M)
hs : Finite ↑s
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
⊢ ∃ J, ∃ (_ : J.FG), s ⊆ ↑(range (rTensor M J.subtype))