awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : 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 : Set (M ⊗[R] N))
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 : Set (M ⊗[R] N))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

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

Premises used: And.intro, Exists.intro, AddMemClass.add_mem, Submodule.FG.sup, Set.insert_subset
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : 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 : Set (M ⊗[R] N))
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : Insert.insert x s ⊆ (↑(mapIncl M₁' N₁').range : Set (M ⊗[R] N))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : Insert.insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
insert : x ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range
insert₁ : y ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range
insert₂ : ∀ (z : M ⊗[R] N) (hz : z ∈ s), z ∈ (↑(mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N),
    M'.FG ∧ N'.FG ∧ Insert.insert (x + y) s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : 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 : Set (M ⊗[R] N))
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 : Set (M ⊗[R] N))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
⊢ x ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range

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

Premises used: le_sup_left, Set.Mem, Set.mem_insert, TensorProduct.range_mapIncl_mono
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : 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 : Set (M ⊗[R] N))
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 : Set (M ⊗[R] N))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
⊢ x ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range

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

Premises used: le_sup_left, Set.mem_insert, TensorProduct.range_mapIncl_mono
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : 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 : Set (M ⊗[R] N))
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 : Set (M ⊗[R] N))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
⊢ y ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range

Tactic:
range_mapIncl_mono le_sup_right le_sup_right (h₂ (Set.mem_insert y s))

Premises used: Set.Mem, le_sup_right, Set.mem_insert, TensorProduct.range_mapIncl_mono
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : 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 : Set (M ⊗[R] N))
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 : Set (M ⊗[R] N))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
⊢ y ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range

Tactic:
exact range_mapIncl_mono le_sup_right le_sup_right (h₂ (Set.mem_insert y s))

Premises used: le_sup_right, Set.mem_insert, TensorProduct.range_mapIncl_mono
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : 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 : Set (M ⊗[R] N))
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 : Set (M ⊗[R] N))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ (↑(mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range : Set (M ⊗[R] N))

Tactic:
range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.subset_insert x s hz))

Premises used: le_sup_left, Set.Mem, Set.subset_insert, TensorProduct.range_mapIncl_mono
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s_1 : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
h_1 : 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 : Set (M ⊗[R] N))
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 : Set (M ⊗[R] N))
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ (↑(mapIncl M₂' N₂').range : Set (M ⊗[R] N))
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ (↑(mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range : Set (M ⊗[R] N))

Tactic:
exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.subset_insert x s hz))

Premises used: le_sup_left, Set.subset_insert, TensorProduct.range_mapIncl_mono
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
empty : ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ ∅ ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
insert :
  ∀ {a : M ⊗[R] N} {s : Set (M ⊗[R] N)},
    a ∉ s →
      s.Finite →
        ∀
          (ih :
            ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))),
          ∃ (M' : Submodule R M) (N' : Submodule R N),
            M'.FG ∧ N'.FG ∧ Insert.insert a s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))

Tactic:
induction s, hs using Set.Finite.induction_on with
  | empty => exact ⟨_, _, fg_bot, fg_bot, Set.empty_subset _⟩
  | @insert a s _ _ ih =>
  obtain ⟨M', N', hM', hN', h⟩ := ih
  refine TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_
  · exact ⟨M', N', hM', hN', Set.insert_subset (zero_mem _) h⟩
  · refine ⟨_, _, hM'.sup (fg_span_singleton x),
      hN'.sup (fg_span_singleton y), Set.insert_subset ?_ fun z hz ↦ ?_⟩
    · exact ⟨⟨x, mem_sup_right (mem_span_singleton_self x)⟩ ⊗ₜ
        ⟨y, mem_sup_right (mem_span_singleton_self y)⟩, rfl⟩
    · exact range_mapIncl_mono le_sup_left le_sup_left (h hz)
  · obtain ⟨M₁', N₁', hM₁', hN₁', h₁⟩ := hx
    obtain ⟨M₂', N₂', hM₂', hN₂', h₂⟩ := hy
    refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩
    · exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.mem_insert x s))
    · exact range_mapIncl_mono le_sup_right le_sup_right (h₂ (Set.mem_insert y s))
    · exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.subset_insert x s hz))

Premises used: Insert.insert
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
obtain :
  ∀ (M' : Submodule R M) (w : Submodule R N) (hfin : Module.Finite.{u_1, u_2} R ↥M'),
    Module.Finite.{u_1, u_3} R ↥w →
      ∀ (h : s ⊆ (↑(mapIncl M' w).range : Set (M ⊗[R] N))),
        ∃ (M' : Submodule R M),
          Module.Finite.{u_1, u_2} R ↥M' ∧ s ⊆ (↑(LinearMap.range (LinearMap.rTensor N M'.subtype)) : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M),
    Module.Finite.{u_1, u_2} R ↥M' ∧ s ⊆ (↑(LinearMap.range (LinearMap.rTensor N M'.subtype)) : Set (M ⊗[R] N))

Tactic:
obtain ⟨M', _, hfin, _, h⟩ := exists_finite_submodule_of_setFinite s hs

Premises used: TensorProduct.exists_finite_submodule_of_setFinite
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w : Submodule R N
hfin : Module.Finite.{u_1, u_2} R ↥M'
left : Module.Finite.{u_1, u_3} R ↥w
h : s ⊆ (↑(mapIncl M' w).range : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M),
    Module.Finite.{u_1, u_2} R ↥M' ∧ s ⊆ (↑(LinearMap.range (LinearMap.rTensor N M'.subtype)) : Set (M ⊗[R] N))

Tactic:
⟨M', hfin, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w : Submodule R N
hfin : Module.Finite.{u_1, u_2} R ↥M'
left : Module.Finite.{u_1, u_3} R ↥w
h : s ⊆ (↑(mapIncl M' w).range : Set (M ⊗[R] N))
refine : s ⊆ (↑(LinearMap.range (LinearMap.rTensor N M'.subtype)) : Set (M ⊗[R] N))
⊢ ∃ (M' : Submodule R M),
    Module.Finite.{u_1, u_2} R ↥M' ∧ s ⊆ (↑(LinearMap.range (LinearMap.rTensor N M'.subtype)) : Set (M ⊗[R] N))

Tactic:
refine ⟨M', hfin, ?_⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w : Submodule R N
hfin : Module.Finite.{u_1, u_2} R ↥M'
left : Module.Finite.{u_1, u_3} R ↥w
h : s ⊆ (↑(mapIncl M' w).range : Set (M ⊗[R] N))
⊢ s ⊆ (↑(LinearMap.rTensor N M'.subtype ∘ₗ LinearMap.lTensor (↥M') w.subtype).range : Set (M ⊗[R] N))

Tactic:
rw [mapIncl, ← LinearMap.rTensor_comp_lTensor] at h

Premises used: TensorProduct.mapIncl, LinearMap.rTensor_comp_lTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w : Submodule R N
hfin : Module.Finite.{u_1, u_2} R ↥M'
left : Module.Finite.{u_1, u_3} R ↥w
h : s ⊆ (↑(LinearMap.rTensor N M'.subtype ∘ₗ LinearMap.lTensor (↥M') w.subtype).range : Set (M ⊗[R] N))
⊢ s ⊆ (↑(LinearMap.range (LinearMap.rTensor N M'.subtype)) : Set (M ⊗[R] N))

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

Premises used: HasSubset.Subset.trans, LinearMap.range_comp_le_range
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
M' : Submodule R M
w : Submodule R N
hfin : Module.Finite.{u_1, u_2} R ↥M'
left : Module.Finite.{u_1, u_3} R ↥w
h : s ⊆ (↑(LinearMap.rTensor N M'.subtype ∘ₗ LinearMap.lTensor (↥M') w.subtype).range : Set (M ⊗[R] N))
⊢ s ⊆ (↑(LinearMap.range (LinearMap.rTensor N M'.subtype)) : Set (M ⊗[R] N))

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

Premises used: HasSubset.Subset.trans, LinearMap.range_comp_le_range
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
obtain :
  ∀ (w : Submodule R M) (N' : Submodule R N),
    Module.Finite.{u_1, u_2} R ↥w →
      ∀ (hfin : Module.Finite.{u_1, u_3} R ↥N') (h : s ⊆ (↑(mapIncl w N').range : Set (M ⊗[R] N))),
        ∃ (N' : Submodule R N),
          Module.Finite.{u_1, u_3} R ↥N' ∧ s ⊆ (↑(LinearMap.range (LinearMap.lTensor M N'.subtype)) : Set (M ⊗[R] N))
⊢ ∃ (N' : Submodule R N),
    Module.Finite.{u_1, u_3} R ↥N' ∧ s ⊆ (↑(LinearMap.range (LinearMap.lTensor M N'.subtype)) : Set (M ⊗[R] N))

Tactic:
obtain ⟨_, N', _, hfin, h⟩ := exists_finite_submodule_of_setFinite s hs

Premises used: TensorProduct.exists_finite_submodule_of_setFinite
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
w : Submodule R M
N' : Submodule R N
left : Module.Finite.{u_1, u_2} R ↥w
hfin : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(mapIncl w N').range : Set (M ⊗[R] N))
⊢ ∃ (N' : Submodule R N),
    Module.Finite.{u_1, u_3} R ↥N' ∧ s ⊆ (↑(LinearMap.range (LinearMap.lTensor M N'.subtype)) : Set (M ⊗[R] N))

Tactic:
⟨N', hfin, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
w : Submodule R M
N' : Submodule R N
left : Module.Finite.{u_1, u_2} R ↥w
hfin : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(mapIncl w N').range : Set (M ⊗[R] N))
refine : s ⊆ (↑(LinearMap.range (LinearMap.lTensor M N'.subtype)) : Set (M ⊗[R] N))
⊢ ∃ (N' : Submodule R N),
    Module.Finite.{u_1, u_3} R ↥N' ∧ s ⊆ (↑(LinearMap.range (LinearMap.lTensor M N'.subtype)) : Set (M ⊗[R] N))

Tactic:
refine ⟨N', hfin, ?_⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
w : Submodule R M
N' : Submodule R N
left : Module.Finite.{u_1, u_2} R ↥w
hfin : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(mapIncl w N').range : Set (M ⊗[R] N))
⊢ s ⊆ (↑(LinearMap.lTensor M N'.subtype ∘ₗ LinearMap.rTensor (↥N') w.subtype).range : Set (M ⊗[R] N))

Tactic:
rw [mapIncl, ← LinearMap.lTensor_comp_rTensor] at h

Premises used: TensorProduct.mapIncl, LinearMap.lTensor_comp_rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
w : Submodule R M
N' : Submodule R N
left : Module.Finite.{u_1, u_2} R ↥w
hfin : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(LinearMap.lTensor M N'.subtype ∘ₗ LinearMap.rTensor (↥N') w.subtype).range : Set (M ⊗[R] N))
⊢ s ⊆ (↑(LinearMap.range (LinearMap.lTensor M N'.subtype)) : Set (M ⊗[R] N))

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

Premises used: HasSubset.Subset.trans, LinearMap.range_comp_le_range
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
w : Submodule R M
N' : Submodule R N
left : Module.Finite.{u_1, u_2} R ↥w
hfin : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(LinearMap.lTensor M N'.subtype ∘ₗ LinearMap.rTensor (↥N') w.subtype).range : Set (M ⊗[R] N))
⊢ s ⊆ (↑(LinearMap.range (LinearMap.lTensor M N'.subtype)) : Set (M ⊗[R] N))

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

Premises used: HasSubset.Subset.trans, LinearMap.range_comp_le_range
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (TensorProduct.{u_1, u_2, u_3} R ↥M₁ ↥N₁)
hs : s.Finite
obtain :
  ∀ (M' : Submodule R ↥M₁) (N' : Submodule R ↥N₁),
    Module.Finite.{u_1, u_2} R ↥M' →
      Module.Finite.{u_1, u_3} R ↥N' →
        ∀ (h : s ⊆ (↑(mapIncl M' N').range : Set (↥M₁ ⊗[R] ↥N₁))),
          ∃ (M' : Submodule R M) (N' : Submodule R N) (hM : M' ≤ M₁) (hN : N' ≤ N₁),
            Module.Finite.{u_1, u_2} R ↥M' ∧
              Module.Finite.{u_1, u_3} R ↥N' ∧ s ⊆ (↑(map (inclusion hM) (inclusion hN)).range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N) (hM : M' ≤ M₁) (hN : N' ≤ N₁),
    Module.Finite.{u_1, u_2} R ↥M' ∧
      Module.Finite.{u_1, u_3} R ↥N' ∧ s ⊆ (↑(map (inclusion hM) (inclusion hN)).range : Set (↥M₁ ⊗[R] ↥N₁))

Tactic:
obtain ⟨M', N', _, _, h⟩ := exists_finite_submodule_of_setFinite s hs

Premises used: TensorProduct.exists_finite_submodule_of_setFinite
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (TensorProduct.{u_1, u_2, u_3} R ↥M₁ ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left : Module.Finite.{u_1, u_2} R ↥M'
left_1 : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(mapIncl M' N').range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ Submodule.map M₁.subtype M' ≤ M₁

Tactic:
have hM := map_subtype_le M₁ M'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (TensorProduct.{u_1, u_2, u_3} R ↥M₁ ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left : Module.Finite.{u_1, u_2} R ↥M'
left_1 : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(mapIncl M' N').range : Set (↥M₁ ⊗[R] ↥N₁))
hM : Submodule.map M₁.subtype M' ≤ M₁
⊢ Submodule.map N₁.subtype N' ≤ N₁

Tactic:
have hN := map_subtype_le N₁ N'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (TensorProduct.{u_1, u_2, u_3} R ↥M₁ ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left : Module.Finite.{u_1, u_2} R ↥M'
left_1 : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(mapIncl M' N').range : Set (↥M₁ ⊗[R] ↥N₁))
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N) (hM : M' ≤ M₁) (hN : N' ≤ N₁),
    Module.Finite.{u_1, u_2} R ↥M' ∧
      Module.Finite.{u_1, u_3} R ↥N' ∧ s ⊆ (↑(map (inclusion hM) (inclusion hN)).range : Set (↥M₁ ⊗[R] ↥N₁))

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

Premises used: And.intro, Exists.intro, Module.Finite.map
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (TensorProduct.{u_1, u_2, u_3} R ↥M₁ ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left : Module.Finite.{u_1, u_2} R ↥M'
left_1 : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(mapIncl M' N').range : Set (↥M₁ ⊗[R] ↥N₁))
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
refine : s ⊆ (↑(map (inclusion hM) (inclusion hN)).range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N) (hM : M' ≤ M₁) (hN : N' ≤ N₁),
    Module.Finite.{u_1, u_2} R ↥M' ∧
      Module.Finite.{u_1, u_3} R ↥N' ∧ s ⊆ (↑(map (inclusion hM) (inclusion hN)).range : Set (↥M₁ ⊗[R] ↥N₁))

Tactic:
refine ⟨_, _, hM, hN, .map _ _, .map _ _, ?_⟩
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (TensorProduct.{u_1, u_2, u_3} R ↥M₁ ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left : Module.Finite.{u_1, u_2} R ↥M'
left_1 : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(map M'.subtype N'.subtype).range : Set (↥M₁ ⊗[R] ↥N₁))
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
h₁ :
  ∀ (x : ↥M'),
    Eq.{u_2 + 1} (α := M) (↑((M'.subtype : (a : ↥M') → ↥M₁) x) : M)
      (↑((inclusion hM ∘ₗ M₁.subtype.submoduleMap M' : (a : ↥M') → ↥M₁) x) : M)
⊢ M'.subtype = inclusion hM ∘ₗ M₁.subtype.submoduleMap M'

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (TensorProduct.{u_1, u_2, u_3} R ↥M₁ ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left : Module.Finite.{u_1, u_2} R ↥M'
left_1 : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(map M'.subtype N'.subtype).range : Set (↥M₁ ⊗[R] ↥N₁))
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
x : ↥M'
⊢ Eq.{u_2 + 1} (α := M) (↑((M'.subtype : (a : ↥M') → ↥M₁) x) : M)
    (↑((inclusion hM ∘ₗ M₁.subtype.submoduleMap M' : (a : ↥M') → ↥M₁) x) : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (TensorProduct.{u_1, u_2, u_3} R ↥M₁ ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left : Module.Finite.{u_1, u_2} R ↥M'
left_1 : Module.Finite.{u_1, u_3} R ↥N'
hM : Submodule.map M₁.subtype M' ≤ M₁
h : s ⊆ (↑(map (inclusion hM ∘ₗ M₁.subtype.submoduleMap M') N'.subtype).range : Set (↥M₁ ⊗[R] ↥N₁))
hN : Submodule.map N₁.subtype N' ≤ N₁
h₁ :
  ∀ (x : ↥N'),
    Eq.{u_3 + 1} (α := N) (↑((N'.subtype : (a : ↥N') → ↥N₁) x) : N)
      (↑((inclusion hN ∘ₗ N₁.subtype.submoduleMap N' : (a : ↥N') → ↥N₁) x) : N)
⊢ N'.subtype = inclusion hN ∘ₗ N₁.subtype.submoduleMap N'

Tactic:
ext