Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case insert.refine_3.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)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(mapIncl M₁' N₁').range
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(mapIncl M₂' N₂').range
⊢ x ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range

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

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

Tactic:
· exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.mem_insert x s))

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

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