-- Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
theorem exists_finite_submodule_of_finite' (s : Set (M₁ ⊗[R] N₁)) (hs : s.Finite) :
    ∃ (M' : Submodule R M) (N' : Submodule R N) (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R M' ∧ Module.Finite R N' ∧
        s ⊆ LinearMap.range (TensorProduct.map (inclusion hM) (inclusion hN))

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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))

Tactic:
have hM := map_subtype_le M₁ M'

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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
hM : Submodule.map M₁.subtype M' ≤ M₁
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))

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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))

Tactic:
obtain ⟨M', N', _, _, 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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))

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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))

Tactic:
refine ⟨_, _, hM, hN, .map _ _, .map _ _, ?_⟩

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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
⊢ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))

Proof state:
case h.a
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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
hM : Submodule.map M₁.subtype M' ≤ M₁
h : s ⊆ ↑(LinearMap.range (map (inclusion hM ∘ₗ M₁.subtype.submoduleMap M') N'.subtype))
hN : Submodule.map N₁.subtype N' ≤ N₁
x✝ : ↥N'
⊢ ↑(N'.subtype x✝) = ↑((inclusion hN ∘ₗ N₁.subtype.submoduleMap N') x✝)

Tactic:
simp

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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
hM : Submodule.map M₁.subtype M' ≤ M₁
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))

Tactic:
have hN := map_subtype_le N₁ N'

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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (map (inclusion hM) (inclusion hN)))

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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (map M'.subtype N'.subtype))
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
⊢ M'.subtype = inclusion hM ∘ₗ M₁.subtype.submoduleMap M'

Tactic:
ext

Result:
case h.a
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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (map M'.subtype N'.subtype))
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
x✝ : ↥M'
⊢ ↑(M'.subtype x✝) = ↑((inclusion hM ∘ₗ M₁.subtype.submoduleMap M') x✝)

Proof state:
case h.a
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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.range (map M'.subtype N'.subtype))
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
x✝ : ↥M'
⊢ ↑(M'.subtype x✝) = ↑((inclusion hM ∘ₗ M₁.subtype.submoduleMap M') x✝)

Tactic:
simp

Result:
no goals