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

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

Premises used: TensorProduct.mapIncl, TensorProduct.map_comp
-- 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₁
hM₁ : Submodule.map M₁.subtype M' ≤ M₁
⊢ Submodule.map N₁.subtype N' ≤ 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

Premises used: TensorProduct.mapIncl, TensorProduct.map_comp
-- 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₁
hM₁ : Submodule.map M₁.subtype M' ≤ M₁
hN₁ : Submodule.map N₁.subtype N' ≤ N₁
⊢ 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

Premises used: TensorProduct.mapIncl, TensorProduct.map_comp
-- 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₁
hN : Submodule.map N₁.subtype N' ≤ N₁
h :
  s ⊆
    (↑(map (inclusion hM) (inclusion hN) ∘ₗ map (M₁.subtype.submoduleMap M') (N₁.subtype.submoduleMap N')).range :
      Set (↥M₁ ⊗[R] ↥N₁))
⊢ s ⊆ (↑(map (inclusion hM) (inclusion hN)).range : 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
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₁
hN : Submodule.map N₁.subtype N' ≤ N₁
h :
  s ⊆
    (↑(map (inclusion hM) (inclusion hN) ∘ₗ map (M₁.subtype.submoduleMap M') (N₁.subtype.submoduleMap N')).range :
      Set (↥M₁ ⊗[R] ↥N₁))
⊢ s ⊆ (↑(map (inclusion hM) (inclusion hN)).range : 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) (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₁))
⊢ ∃ (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

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
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₁))

Tactic:
⟨M', hM, 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
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₁))
refine : s ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM))) : 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:
refine ⟨M', hM, 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
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.rTensor (↥N₁) (inclusion hM) ∘ₗ LinearMap.lTensor (↥M') (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))

Tactic:
rw [← LinearMap.rTensor_comp_lTensor] at h

Premises used: 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
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 ⊆ (↑(LinearMap.rTensor (↥N₁) (inclusion hM) ∘ₗ LinearMap.lTensor (↥M') (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ s ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM))) : 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
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 ⊆ (↑(LinearMap.rTensor (↥N₁) (inclusion hM) ∘ₗ LinearMap.lTensor (↥M') (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ s ⊆ (↑(LinearMap.range (LinearMap.rTensor (↥N₁) (inclusion hM))) : 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 :
  ∀ (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₁))
⊢ ∃ (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

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
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₁))

Tactic:
⟨N', hN, 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
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₁))
refine : s ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN))) : 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:
refine ⟨N', hN, 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
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.lTensor (↥M₁) (inclusion hN) ∘ₗ LinearMap.rTensor (↥N') (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))

Tactic:
rw [← LinearMap.lTensor_comp_rTensor] at h

Premises used: 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
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 ⊆ (↑(LinearMap.lTensor (↥M₁) (inclusion hN) ∘ₗ LinearMap.rTensor (↥N') (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ s ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN))) : 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
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 ⊆ (↑(LinearMap.lTensor (↥M₁) (inclusion hN) ∘ₗ LinearMap.rTensor (↥N') (inclusion w_1)).range : Set (↥M₁ ⊗[R] ↥N₁))
⊢ s ⊆ (↑(LinearMap.range (LinearMap.lTensor (↥M₁) (inclusion hN))) : 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
⊢ Eq (α := M ⊗[R] N) 0
    (∑ j : Fin 0,
      (fun (a : Fin 0) ↦ (IsEmpty.elim ⋯ (p := fun (x : Fin 0) ↦ M) a : M)) j ⊗ₜ[R]
        (fun (a : Fin 0) ↦ (IsEmpty.elim ⋯ (p := fun (x : Fin 0) ↦ N) a : N)) j)

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
⊢ ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), Eq (α := M ⊗[R] N) 0 (∑ j : Fin k, m j ⊗ₜ[R] n j)

Tactic:
exact ⟨0, IsEmpty.elim inferInstance, IsEmpty.elim inferInstance, by 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
x : M
y : N
⊢ Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) (∑ j : Fin 1, (fun (x_1 : Fin 1) ↦ x) j ⊗ₜ[R] (fun (x : Fin 1) ↦ y) j)

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
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:
exact ⟨1, fun _ ↦ x, fun _ ↦ y, by 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
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
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
⊢ ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), x + y = ∑ j : Fin k, m j ⊗ₜ[R] n j

Tactic:
obtain ⟨kx, mx, nx, rfl⟩ := hx

Premises used: rfl
-- 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
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
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
⊢ ∃ (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 ⟨ky, my, ny, rfl⟩ := hy

Premises used: rfl
-- 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
kx : ℕ
mx : Fin kx → M
nx : Fin kx → N
ky : ℕ
my : Fin ky → M
ny : Fin ky → N
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
⊢ ∃ (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:
use kx + ky, Fin.addCases mx my, Fin.addCases nx ny
-- 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
kx : ℕ
mx : Fin kx → M
nx : Fin kx → N
ky : ℕ
my : Fin ky → M
ny : Fin ky → N
⊢ 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:
simp [Fin.sum_univ_add]

Premises used: Fin.sum_univ_add
-- 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
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)
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
⊢ ∃ (k : ℕ) (m : Fin k → M) (n : Fin k → N), x = ∑ 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]

Premises used: Fin.sum_univ_add, Submodule.zero, TensorProduct.tmul, Submodule.add, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
refine :
  (⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) ≃ₗ[R]
    ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)
⊢ ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i) ≃ₗ[R] (⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i

Tactic:
refine TensorProduct.directSum R R 𝒜 ℬ ≪≫ₗ ?_ ≪≫ₗ (TensorProduct.directSum R R ℬ 𝒜).symm

Premises used: LinearEquiv.symm, TensorProduct.directSum
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
⊢ (⨁ (i : ι × ι), TensorProduct.{u_1, u_3, u_4} R (𝒜 i.1) (ℬ i.2)) ≃ₗ[R]
    ⨁ (i : ι × ι), TensorProduct.{u_1, u_4, u_3} R (ℬ i.1) (𝒜 i.2)

Tactic:
exact LinearEquiv.ofLinear (gradedCommAux _ _ _) (gradedCommAux _ _ _)
    (gradedCommAux_comp_gradedCommAux _ _ _) (gradedCommAux_comp_gradedCommAux _ _ _)

Premises used: LinearEquiv.ofLinear, TensorProduct.gradedCommAux, TensorProduct.gradedCommAux_comp_gradedCommAux
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External
Goal:
R : Type u_1
ι : Type u_2
inst : CommSemiring ι
inst_1 : Module ι (Additive ℤˣ)
inst_2 : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst_3 : CommRing R
inst_4 : (i : ι) → AddCommGroup (𝒜 i)
inst_5 : (i : ι) → AddCommGroup (ℬ i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (𝒜 i)
inst_7 : (i : ι) → Module.{u_1, u_4} R (ℬ i)
⊢ Eq (α := ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i) ≃ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)
    (LinearEquiv.symm (gradedComm R 𝒜 ℬ)) (gradedComm R ℬ 𝒜)

Tactic:
rfl