-- 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), Module.Finite R M' ∧ Module.Finite R N' ∧
      s ⊆ LinearMap.range (mapIncl M' N')

Proof state:
case intro.intro.intro.intro.refine_1
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
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert 0 s ⊆ ↑(LinearMap.range (mapIncl M' N'))

Tactic:
exact ⟨M', N', hM', hN', Set.insert_subset (zero_mem _) h⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2.refine_1
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
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x : M
y : N
⊢ x ⊗ₜ[R] y ∈ ↑(LinearMap.range (mapIncl (M' ⊔ span R {x}) (N' ⊔ span R {y})))

Tactic:
exact ⟨⟨x, mem_sup_right (mem_span_singleton_self x)⟩ ⊗ₜ
  ⟨y, mem_sup_right (mem_span_singleton_self y)⟩, rfl⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_3
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
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x y : M ⊗[R] N
hx : ∃ M' N', M'.FG ∧ N'.FG ∧ insert x s ⊆ ↑(LinearMap.range (mapIncl M' N'))
hy : ∃ M' N', M'.FG ∧ N'.FG ∧ insert y s ⊆ ↑(LinearMap.range (mapIncl M' N'))
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(LinearMap.range (mapIncl M' N'))

Tactic:
obtain ⟨M₁', N₁', hM₁', hN₁', h₁⟩ := hx

Result:
case intro.intro.intro.intro.refine_3.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
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x y : M ⊗[R] N
hy : ∃ M' N', M'.FG ∧ N'.FG ∧ insert y s ⊆ ↑(LinearMap.range (mapIncl M' N'))
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(LinearMap.range (mapIncl M₁' N₁'))
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(LinearMap.range (mapIncl M' N'))

Proof state:
case intro.intro.intro.intro.refine_3.intro.intro.intro.intro.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
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(LinearMap.range (mapIncl M₁' N₁'))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(LinearMap.range (mapIncl M₂' N₂'))
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(LinearMap.range (mapIncl M' N'))

Tactic:
refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩

Result:
case intro.intro.intro.intro.refine_3.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
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
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(LinearMap.range (mapIncl M₁' N₁'))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(LinearMap.range (mapIncl M₂' N₂'))
⊢ x ∈ LinearMap.range (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂'))

case intro.intro.intro.intro.refine_3.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
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
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(LinearMap.range (mapIncl M₁' N₁'))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(LinearMap.range (mapIncl M₂' N₂'))
⊢ y ∈ LinearMap.range (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂'))

case intro.intro.intro.intro.refine_3.intro.intro.intro.intro.intro.intro.intro.intro.refine_3
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
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(LinearMap.range (mapIncl M₁' N₁'))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(LinearMap.range (mapIncl M₂' N₂'))
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ ↑(LinearMap.range (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')))

Proof state:
case intro.intro.intro.intro.refine_3.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
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x y : M ⊗[R] N
hy : ∃ M' N', M'.FG ∧ N'.FG ∧ insert y s ⊆ ↑(LinearMap.range (mapIncl M' N'))
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(LinearMap.range (mapIncl M₁' N₁'))
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(LinearMap.range (mapIncl M' N'))

Tactic:
obtain ⟨M₂', N₂', hM₂', hN₂', h₂⟩ := hy

Result:
case intro.intro.intro.intro.refine_3.intro.intro.intro.intro.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
a : M ⊗[R] N
s : Set (M ⊗[R] N)
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(LinearMap.range (mapIncl M' N'))
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(LinearMap.range (mapIncl M₁' N₁'))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(LinearMap.range (mapIncl M₂' N₂'))
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(LinearMap.range (mapIncl M' N'))