awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N), M'.FG ∧ N'.FG ∧ s ⊆ (↑(mapIncl M' N').range : Set (M ⊗[R] N))
have 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 a 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))
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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),
    Module.Finite.{u_1, u_2} R ↥M' ∧ s ⊆ (↑(LinearMap.range (LinearMap.rTensor N M'.subtype)) : Set (M ⊗[R] N))
have 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))
Tactic: obtain ⟨M', _, hfin, _, h⟩ := exists_finite_submodule_of_setFinite s hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
have refine : s ⊆ (↑(LinearMap.range (LinearMap.rTensor N M'.subtype)) : Set (M ⊗[R] N))
Tactic: refine ⟨M', hfin, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (hypothesis)
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.range (LinearMap.rTensor N M'.subtype)) : Set (M ⊗[R] N))
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
⊢ ∃ (N' : Submodule R N),
    Module.Finite.{u_1, u_3} R ↥N' ∧ s ⊆ (↑(LinearMap.range (LinearMap.lTensor M N'.subtype)) : Set (M ⊗[R] N))
have 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))
Tactic: obtain ⟨_, N', _, hfin, h⟩ := exists_finite_submodule_of_setFinite s hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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))
have refine : s ⊆ (↑(LinearMap.range (LinearMap.lTensor M N'.subtype)) : Set (M ⊗[R] N))
Tactic: refine ⟨N', hfin, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (hypothesis)
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.range (LinearMap.lTensor M N'.subtype)) : Set (M ⊗[R] N))
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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) (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₁))
have 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₁))
Tactic: obtain ⟨M', N', _, _, h⟩ := exists_finite_submodule_of_setFinite s hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (hypothesis)
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₁))
⊢ ∃ (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₁))
have hM : Submodule.map M₁.subtype M' ≤ M₁
Tactic: have hM := map_subtype_le M₁ M'
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (hypothesis)
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₁
⊢ ∃ (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₁))
have hN : Submodule.map N₁.subtype N' ≤ N₁
Tactic: have hN := map_subtype_le N₁ N'
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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₁))
have refine : s ⊆ (↑(map (inclusion hM) (inclusion hN)).range : Set (↥M₁ ⊗[R] ↥N₁))
Tactic: refine ⟨_, _, hM, hN, .map _ _, .map _ _, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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₁
⊢ M'.subtype = inclusion hM ∘ₗ M₁.subtype.submoduleMap M'
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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₁
⊢ N'.subtype = inclusion hN ∘ₗ N₁.subtype.submoduleMap N'
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (hypothesis)
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₁
hM₁ : Submodule.map M₁.subtype M' ≤ M₁
hN₁ : Submodule.map N₁.subtype N' ≤ N₁
⊢ s ⊆ (↑(map (inclusion hM) (inclusion hN)).range : Set (↥M₁ ⊗[R] ↥N₁))
have h₁ : s ⊆
  (↑(map (inclusion hM₁) (inclusion hN₁) ∘ₗ map (M₁.subtype.submoduleMap M') (N₁.subtype.submoduleMap N')).range :
    Set (↥M₁ ⊗[R] ↥N₁))
Tactic: rw [mapIncl,
    show M'.subtype = inclusion hM ∘ₗ M₁.subtype.submoduleMap M' by ext; simp,
    show N'.subtype = inclusion hN ∘ₗ N₁.subtype.submoduleMap N' by ext; simp,
    map_comp] at h
Cleared hypotheses: h, hM, hN
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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) (hM : M' ≤ M₁),
    Module.Finite.{u_1, u_2} R ↥M' ∧
      s ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM))) : Set (↥M₁ ⊗[R] ↥N₁))
have obtain : ∀ (M' : Submodule R M) (w : Submodule R N) (hM : M' ≤ M₁) (w_1 : w ≤ N₁) (hfin : Module.Finite.{u_1, u_2} R ↥M'),
  Module.Finite.{u_1, u_3} R ↥w →
    ∀ (h : s ⊆ (↑(map (inclusion hM) (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))),
      ∃ (M' : Submodule R M) (hM : M' ≤ M₁),
        Module.Finite.{u_1, u_2} R ↥M' ∧
          s ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM))) : Set (↥M₁ ⊗[R] ↥N₁))
Tactic: obtain ⟨M', _, hM, _, hfin, _, h⟩ := exists_finite_submodule_of_setFinite' s hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
w : Submodule R N
hM : M' ≤ M₁
w_1 : w ≤ N₁
hfin : Module.Finite.{u_1, u_2} R ↥M'
left : Module.Finite.{u_1, u_3} R ↥w
h : s ⊆ (↑(map (inclusion hM) (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ ∃ (M' : Submodule R M) (hM : M' ≤ M₁),
    Module.Finite.{u_1, u_2} R ↥M' ∧
      s ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM))) : Set (↥M₁ ⊗[R] ↥N₁))
have refine : s ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM))) : Set (↥M₁ ⊗[R] ↥N₁))
Tactic: refine ⟨M', hM, hfin, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (hypothesis)
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
w : Submodule R N
hM : M' ≤ M₁
w_1 : w ≤ N₁
hfin : Module.Finite.{u_1, u_2} R ↥M'
left : Module.Finite.{u_1, u_3} R ↥w
h : s ⊆ (↑(map (inclusion hM) (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ s ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM))) : Set (↥M₁ ⊗[R] ↥N₁))
have h₁ : s ⊆ (↑(LinearMap.rTensor (↥N₁) (inclusion hM) ∘ₗ LinearMap.lTensor (↥M') (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))
Tactic: rw [← LinearMap.rTensor_comp_lTensor] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
⊢ ∃ (N' : Submodule R N) (hN : N' ≤ N₁),
    Module.Finite.{u_1, u_3} R ↥N' ∧
      s ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN))) : Set (↥M₁ ⊗[R] ↥N₁))
have obtain : ∀ (w : Submodule R M) (N' : Submodule R N) (w_1 : w ≤ M₁) (hN : N' ≤ N₁),
  Module.Finite.{u_1, u_2} R ↥w →
    ∀ (hfin : Module.Finite.{u_1, u_3} R ↥N')
      (h : s ⊆ (↑(map (inclusion w_1) (inclusion hN)).range : Set (↥M₁ ⊗[R] ↥N₁))),
      ∃ (N' : Submodule R N) (hN : N' ≤ N₁),
        Module.Finite.{u_1, u_3} R ↥N' ∧
          s ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN))) : Set (↥M₁ ⊗[R] ↥N₁))
Tactic: obtain ⟨_, N', _, hN, _, hfin, h⟩ := exists_finite_submodule_of_setFinite' s hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
w : Submodule R M
N' : Submodule R N
w_1 : w ≤ M₁
hN : N' ≤ N₁
left : Module.Finite.{u_1, u_2} R ↥w
hfin : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(map (inclusion w_1) (inclusion hN)).range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ ∃ (N' : Submodule R N) (hN : N' ≤ N₁),
    Module.Finite.{u_1, u_3} R ↥N' ∧
      s ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN))) : Set (↥M₁ ⊗[R] ↥N₁))
have refine : s ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN))) : Set (↥M₁ ⊗[R] ↥N₁))
Tactic: refine ⟨N', hN, hfin, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (hypothesis)
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
w : Submodule R M
N' : Submodule R N
w_1 : w ≤ M₁
hN : N' ≤ N₁
left : Module.Finite.{u_1, u_2} R ↥w
hfin : Module.Finite.{u_1, u_3} R ↥N'
h : s ⊆ (↑(map (inclusion w_1) (inclusion hN)).range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ s ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN))) : Set (↥M₁ ⊗[R] ↥N₁))
have h₁ : s ⊆ (↑(LinearMap.lTensor (↥M₁) (inclusion hN) ∘ₗ LinearMap.rTensor (↥N') (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))
Tactic: rw [← LinearMap.lTensor_comp_rTensor] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
x y : M ⊗[R] N
hx : ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), x = ∑ j : Fin k, m j ⊗ₜ[R] n j
hy : ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), y = ∑ j : Fin k, m j ⊗ₜ[R] n j
⊢ ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), x + y = ∑ j : Fin k, m j ⊗ₜ[R] n j
have add : ∀ (kx : ℕ) (mx : Fin kx → M) (nx : Fin kx → N),
  ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), ∑ j : Fin kx, mx j ⊗ₜ[R] nx j + y = ∑ j : Fin k, m j ⊗ₜ[R] n j
Tactic: obtain ⟨kx, mx, nx, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
y : M ⊗[R] N
hy : ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), y = ∑ j : Fin k, m j ⊗ₜ[R] n j
kx : ℕ
mx : Fin kx → M
nx : Fin kx → N
⊢ ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), ∑ j : Fin kx, mx j ⊗ₜ[R] nx j + y = ∑ j : Fin k, m j ⊗ₜ[R] n j
have add : ∀ (ky : ℕ) (my : Fin ky → M) (ny : Fin ky → N),
  ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N),
    HAdd.hAdd (α := M ⊗[R] N) (∑ j : Fin kx, mx j ⊗ₜ[R] nx j) (∑ j : Fin ky, my j ⊗ₜ[R] ny j) =
      ∑ j : Fin k, m j ⊗ₜ[R] n j
Tactic: obtain ⟨ky, my, ny, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
kx : ℕ
mx : Fin kx → M
nx : Fin kx → N
ky : ℕ
my : Fin ky → M
ny : Fin ky → N
⊢ ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N),
    HAdd.hAdd (α := M ⊗[R] N) (∑ j : Fin kx, mx j ⊗ₜ[R] nx j) (∑ j : Fin ky, my j ⊗ₜ[R] ny j) =
      ∑ j : Fin k, m j ⊗ₜ[R] n j
have h : HAdd.hAdd (α := M ⊗[R] N) (∑ j : Fin kx, mx j ⊗ₜ[R] nx j) (∑ j : Fin ky, my j ⊗ₜ[R] ny j) =
  ∑ j : Fin (kx + ky),
    Fin.addCases (motive := fun (x : Fin (kx + ky)) ↦ M) mx my j ⊗ₜ[R]
      (fun (i : Fin (kx + ky)) ↦ (Fin.addCases (motive := fun (x : Fin (kx + ky)) ↦ N) nx ny i : N)) j
Tactic: use kx + ky, Fin.addCases mx my, Fin.addCases nx ny
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
x : M ⊗[R] N
⊢ ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), x = ∑ j : Fin k, m j ⊗ₜ[R] n j
have zero : ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), Eq (α := M ⊗[R] N) 0 (∑ j : Fin k, m j ⊗ₜ[R] n j)
Tactic: induction x with
  | zero => exact ⟨0, IsEmpty.elim inferInstance, IsEmpty.elim inferInstance, by simp⟩
  | tmul x y => exact ⟨1, fun _ ↦ x, fun _ ↦ y, by simp⟩
  | add x y hx hy =>
    obtain ⟨kx, mx, nx, rfl⟩ := hx
    obtain ⟨ky, my, ny, rfl⟩ := hy
    use kx + ky, Fin.addCases mx my, Fin.addCases nx ny
    simp [Fin.sum_univ_add]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
x : M ⊗[R] N
zero : ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), Eq (α := M ⊗[R] N) 0 (∑ j : Fin k, m j ⊗ₜ[R] n j)
⊢ ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), x = ∑ j : Fin k, m j ⊗ₜ[R] n j
have tmul : ∀ (x : M) (y : N),
  ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) (∑ j : Fin k, m j ⊗ₜ[R] n j)
Tactic: induction x with
  | zero => exact ⟨0, IsEmpty.elim inferInstance, IsEmpty.elim inferInstance, by simp⟩
  | tmul x y => exact ⟨1, fun _ ↦ x, fun _ ↦ y, by simp⟩
  | add x y hx hy =>
    obtain ⟨kx, mx, nx, rfl⟩ := hx
    obtain ⟨ky, my, ny, rfl⟩ := hy
    use kx + ky, Fin.addCases mx my, Fin.addCases nx ny
    simp [Fin.sum_univ_add]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Finiteness (goal)
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
x : M ⊗[R] N
zero : ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), Eq (α := M ⊗[R] N) 0 (∑ j : Fin k, m j ⊗ₜ[R] n j)
tmul :
  ∀ (x : M) (y : N),
    ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) (∑ j : Fin k, m j ⊗ₜ[R] n j)
⊢ ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), x = ∑ j : Fin k, m j ⊗ₜ[R] n j
have add : ∀ (x y : M ⊗[R] N) (hx : ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), x = ∑ j : Fin k, m j ⊗ₜ[R] n j)
  (hy : ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), y = ∑ j : Fin k, m j ⊗ₜ[R] n j),
  ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), x + y = ∑ j : Fin k, m j ⊗ₜ[R] n j
Tactic: induction x with
  | zero => exact ⟨0, IsEmpty.elim inferInstance, IsEmpty.elim inferInstance, by simp⟩
  | tmul x y => exact ⟨1, fun _ ↦ x, fun _ ↦ y, by simp⟩
  | add x y hx hy =>
    obtain ⟨kx, mx, nx, rfl⟩ := hx
    obtain ⟨ky, my, ny, rfl⟩ := hy
    use kx + ky, Fin.addCases mx my, Fin.addCases nx ny
    simp [Fin.sum_univ_add]
Cleared hypotheses: x