awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
i : ι
m : M
g : G i
⊢ Eq (α :=
    Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_4, u_3} R M (G x)) fun (i j : ι) (h : i ≤ j) ↦
      LinearMap.lTensor M (f i j h))
    ((directLimitRight (G := G) f M :
          (a : M ⊗[R] Module.DirectLimit G f) →
            Module.DirectLimit (fun (x : ι) ↦ M ⊗[R] G x) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.lTensor M (f i j h))
        (m ⊗ₜ[R] (of R ι G f i : (a : G i) → Module.DirectLimit G f) g) :
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_4, u_3} R M (G x)) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.lTensor M (f i j h))
    (((of R ι (fun (x : ι) ↦ TensorProduct.{u_1, u_4, u_3} R M (G x))
              (fun (i j : ι) (h : i ≤ j) ↦ LinearMap.lTensor M (f i j h)) i :
            TensorProduct.{u_1, u_4, u_3} R M (G i) →ₗ[R]
              Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_4, u_3} R M (G x))
                fun (i j : ι) (h : i ≤ j) ↦ LinearMap.lTensor M (f i j h)) :
          (a : M ⊗[R] G i) →
            Module.DirectLimit (fun (x : ι) ↦ M ⊗[R] G x) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.lTensor M (f i j h))
        (m ⊗ₜ[R] g) :
      Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_4, u_3} R M (G x)) fun (i j : ι) (h : i ≤ j) ↦
        LinearMap.lTensor M (f i j h))

Tactic:
simp [directLimitRight, congr_apply_of]

Premises used: Module.DirectLimit.congr_apply_of, TensorProduct.directLimitRight
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
i : ι
m : M
g : G i
⊢ Eq (α := M ⊗[R] Module.DirectLimit G f)
    ((LinearEquiv.symm (directLimitRight (G := G) f M) :
          (a :
              Module.DirectLimit (fun (x : ι) ↦ M ⊗[R] G x) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.lTensor M (f i j h)) →
            M ⊗[R] Module.DirectLimit G f)
        (((of R ι (fun (x : ι) ↦ TensorProduct.{u_1, u_4, u_3} R M (G x))
                (fun (i j : ι) (h : i ≤ j) ↦ LinearMap.lTensor M (f i j h)) i :
              TensorProduct.{u_1, u_4, u_3} R M (G i) →ₗ[R]
                Module.DirectLimit (R := R) (fun (x : ι) ↦ TensorProduct.{u_1, u_4, u_3} R M (G x))
                  fun (i j : ι) (h : i ≤ j) ↦ LinearMap.lTensor M (f i j h)) :
            (a : M ⊗[R] G i) →
              Module.DirectLimit (fun (x : ι) ↦ M ⊗[R] G x) fun (i j : ι) (h : i ≤ j) ↦ LinearMap.lTensor M (f i j h))
          (m ⊗ₜ[R] g)) :
      M ⊗[R] Module.DirectLimit G f)
    (m ⊗ₜ[R] (of R ι G f i : (a : G i) → Module.DirectLimit G f) g : M ⊗[R] Module.DirectLimit G f)

Tactic:
simp [directLimitRight, congr_symm_apply_of]

Premises used: Module.DirectLimit.congr_symm_apply_of, TensorProduct.directLimitRight
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_3, u_4} R (G i) M
⊢ (LinearMap.rTensor M LinearMap.id : (a : G i ⊗[R] M) → G i ⊗[R] M) x = x

Tactic:
LinearMap.rTensor_id_apply M (G i) x

Premises used: LinearMap.rTensor_id_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_3, u_4} R (G i) M
h : f i i ⋯ = LinearMap.id
⊢ (LinearMap.rTensor M (f i i ⋯) : (a : G i ⊗[R] M) → G i ⊗[R] M) x = x

Tactic:
convert! LinearMap.rTensor_id_apply M (G i) x

Premises used: LinearMap.rTensor_id_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_3, u_4} R (G i) M
h : ∀ (x : G i), Eq (α := G i) ((f i i ⋯ : (a : G i) → G i) x : G i) ((LinearMap.id : (a : G i) → G i) x : G i)
⊢ f i i ⋯ = LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_3, u_4} R (G i) M
x_1 : G i
⊢ Eq (α := G i) ((f i i ⋯ : (a : G i) → G i) x_1 : G i) ((LinearMap.id : (a : G i) → G i) x_1 : G i)

Tactic:
apply DirectedSystem.map_self'

Premises used: DirectedSystem.map_self'
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h : x_3 ≤ x_2
h_1 : x_2 ≤ x_1
x : TensorProduct.{u_1, u_3, u_4} R (G x_3) M
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R (G x_1) M)
    ((LinearMap.rTensor M (f x_2 x_1 h_1) : (a : G x_2 ⊗[R] M) → G x_1 ⊗[R] M)
        ((LinearMap.rTensor M (f x_3 x_2 h) : (a : G x_3 ⊗[R] M) → G x_2 ⊗[R] M) x) :
      TensorProduct.{u_1, u_3, u_4} R (G x_1) M)
    ((LinearMap.rTensor M (f x_2 x_1 h_1 ∘ₗ f x_3 x_2 h) : (a : G x_3 ⊗[R] M) → G x_1 ⊗[R] M) x :
      TensorProduct.{u_1, u_3, u_4} R (G x_1) M)

Tactic:
(LinearMap.rTensor_comp_apply M _ _ x).symm

Premises used: LinearMap.rTensor_comp_apply, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h_1 : x_3 ≤ x_2
h_2 : x_2 ≤ x_1
x : TensorProduct.{u_1, u_3, u_4} R (G x_3) M
h : f x_2 x_1 h_2 ∘ₗ f x_3 x_2 h_1 = f x_3 x_1 ⋯
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R (G x_1) M)
    ((LinearMap.rTensor M (f x_2 x_1 h_2) : (a : G x_2 ⊗[R] M) → G x_1 ⊗[R] M)
        ((LinearMap.rTensor M (f x_3 x_2 h_1) : (a : G x_3 ⊗[R] M) → G x_2 ⊗[R] M) x) :
      TensorProduct.{u_1, u_3, u_4} R (G x_1) M)
    ((LinearMap.rTensor M (f x_3 x_1 ⋯) : (a : G x_3 ⊗[R] M) → G x_1 ⊗[R] M) x :
      TensorProduct.{u_1, u_3, u_4} R (G x_1) M)

Tactic:
convert! ← (LinearMap.rTensor_comp_apply M _ _ x).symm

Premises used: LinearMap.rTensor_comp_apply, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h_1 : x_3 ≤ x_2
h_2 : x_2 ≤ x_1
x : TensorProduct.{u_1, u_3, u_4} R (G x_3) M
h :
  ∀ (x : G x_3),
    Eq (α := G x_1) ((f x_2 x_1 h_2 ∘ₗ f x_3 x_2 h_1 : (a : G x_3) → G x_1) x : G x_1)
      ((f x_3 x_1 ⋯ : (a : G x_3) → G x_1) x : G x_1)
⊢ f x_2 x_1 h_2 ∘ₗ f x_3 x_2 h_1 = f x_3 x_1 ⋯

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h : x_3 ≤ x_2
h_1 : x_2 ≤ x_1
x : TensorProduct.{u_1, u_3, u_4} R (G x_3) M
x_4 : G x_3
⊢ Eq (α := G x_1) ((f x_2 x_1 h_1 ∘ₗ f x_3 x_2 h : (a : G x_3) → G x_1) x_4 : G x_1)
    ((f x_3 x_1 ⋯ : (a : G x_3) → G x_1) x_4 : G x_1)

Tactic:
apply DirectedSystem.map_map' f

Premises used: DirectedSystem.map_map'
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_4, u_3} R M (G i)
⊢ (LinearMap.lTensor M LinearMap.id : (a : M ⊗[R] G i) → M ⊗[R] G i) x = x

Tactic:
LinearMap.lTensor_id_apply M _ x

Premises used: LinearMap.lTensor_id_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_4, u_3} R M (G i)
h : f i i ⋯ = LinearMap.id
⊢ (LinearMap.lTensor M (f i i ⋯) : (a : M ⊗[R] G i) → M ⊗[R] G i) x = x

Tactic:
convert! LinearMap.lTensor_id_apply M _ x

Premises used: LinearMap.lTensor_id_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_4, u_3} R M (G i)
h : ∀ (x : G i), Eq (α := G i) ((f i i ⋯ : (a : G i) → G i) x : G i) ((LinearMap.id : (a : G i) → G i) x : G i)
⊢ f i i ⋯ = LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
i : ι
x : TensorProduct.{u_1, u_4, u_3} R M (G i)
x_1 : G i
⊢ Eq (α := G i) ((f i i ⋯ : (a : G i) → G i) x_1 : G i) ((LinearMap.id : (a : G i) → G i) x_1 : G i)

Tactic:
apply DirectedSystem.map_self'

Premises used: DirectedSystem.map_self'
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h₁ : x_3 ≤ x_2
h₂ : x_2 ≤ x_1
x : TensorProduct.{u_1, u_4, u_3} R M (G x_3)
⊢ Eq (α := TensorProduct.{u_1, u_4, u_3} R M (G x_1))
    ((LinearMap.lTensor M (f x_2 x_1 h₂) : (a : M ⊗[R] G x_2) → M ⊗[R] G x_1)
        ((LinearMap.lTensor M (f x_3 x_2 h₁) : (a : M ⊗[R] G x_3) → M ⊗[R] G x_2) x) :
      TensorProduct.{u_1, u_4, u_3} R M (G x_1))
    ((LinearMap.lTensor M (f x_2 x_1 h₂ ∘ₗ f x_3 x_2 h₁) : (a : M ⊗[R] G x_3) → M ⊗[R] G x_1) x :
      TensorProduct.{u_1, u_4, u_3} R M (G x_1))

Tactic:
(LinearMap.lTensor_comp_apply M _ _ x).symm

Premises used: LinearMap.lTensor_comp_apply, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h₁ : x_3 ≤ x_2
h₂ : x_2 ≤ x_1
x : TensorProduct.{u_1, u_4, u_3} R M (G x_3)
h : f x_2 x_1 h₂ ∘ₗ f x_3 x_2 h₁ = f x_3 x_1 ⋯
⊢ Eq (α := TensorProduct.{u_1, u_4, u_3} R M (G x_1))
    ((LinearMap.lTensor M (f x_2 x_1 h₂) : (a : M ⊗[R] G x_2) → M ⊗[R] G x_1)
        ((LinearMap.lTensor M (f x_3 x_2 h₁) : (a : M ⊗[R] G x_3) → M ⊗[R] G x_2) x) :
      TensorProduct.{u_1, u_4, u_3} R M (G x_1))
    ((LinearMap.lTensor M (f x_3 x_1 ⋯) : (a : M ⊗[R] G x_3) → M ⊗[R] G x_1) x :
      TensorProduct.{u_1, u_4, u_3} R M (G x_1))

Tactic:
convert! ← (LinearMap.lTensor_comp_apply M _ _ x).symm

Premises used: LinearMap.lTensor_comp_apply, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h₁ : x_3 ≤ x_2
h₂ : x_2 ≤ x_1
x : TensorProduct.{u_1, u_4, u_3} R M (G x_3)
h :
  ∀ (x : G x_3),
    Eq (α := G x_1) ((f x_2 x_1 h₂ ∘ₗ f x_3 x_2 h₁ : (a : G x_3) → G x_1) x : G x_1)
      ((f x_3 x_1 ⋯ : (a : G x_3) → G x_1) x : G x_1)
⊢ f x_2 x_1 h₂ ∘ₗ f x_3 x_2 h₁ = f x_3 x_1 ⋯

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Preorder ι
G : ι → Type u_3
inst_3 : (i : ι) → AddCommMonoid (G i)
inst_4 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
x_1 x_2 x_3 : ι
h₁ : x_3 ≤ x_2
h₂ : x_2 ≤ x_1
x : TensorProduct.{u_1, u_4, u_3} R M (G x_3)
x_4 : G x_3
⊢ Eq (α := G x_1) ((f x_2 x_1 h₂ ∘ₗ f x_3 x_2 h₁ : (a : G x_3) → G x_1) x_4 : G x_1)
    ((f x_3 x_1 ⋯ : (a : G x_3) → G x_1) x_4 : G x_1)

Tactic:
apply DirectedSystem.map_map' f

Premises used: DirectedSystem.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
⊢ Eq (α := M ⊗[R] N) 0 (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) 0))

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
⊢ ∃ (S : Multiset (M × N)), Eq (α := M ⊗[R] N) 0 (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))

Tactic:
exact ⟨0, 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) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) {(x, y)}))

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
⊢ ∃ (S : Multiset (M × N)),
    Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))

Tactic:
exact ⟨{(x, 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 : ∃ (S : Multiset (M × N)), x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
hy : ∃ (S : Multiset (M × N)), y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
add :
  ∀ (Sx : Multiset (M × N)) (hx : x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)),
    ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
⊢ ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)

Tactic:
obtain ⟨Sx, hx⟩ := hx
-- 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
hy : ∃ (S : Multiset (M × N)), y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
Sx : Multiset (M × N)
hx : x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
add :
  ∀ (Sy : Multiset (M × N)) (hy : y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)),
    ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
⊢ ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)

Tactic:
obtain ⟨Sy, hy⟩ := hy
-- 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
Sx : Multiset (M × N)
hx : x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
Sy : Multiset (M × N)
hy : y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)
rw :
  x + y =
    (HAdd.hAdd (α := Multiset (M ⊗[R] N)) (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
        (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)).sum
rw₁ :
  x + y =
    HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
      (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy))
rw₂ :
  Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx) + y =
    HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
      (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy))
rw₃ rw₄ :
  HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
      (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)) =
    HAdd.hAdd (α := M ⊗[R] N) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx))
      (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy))
⊢ x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) (Sx + Sy))

Tactic:
rw [Multiset.map_add, Multiset.sum_add, hx, hy]

Premises used: Multiset.sum_add, Multiset.map_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 y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sx)
Sy : Multiset (M × N)
hy : y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) Sy)
⊢ ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)

Tactic:
exact ⟨Sx + Sy, by rw [Multiset.map_add, Multiset.sum_add, hx, hy]⟩
-- 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 : ∃ (S : Multiset (M × N)), Eq (α := M ⊗[R] N) 0 (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))
tmul :
  ∀ (x : M) (y : N),
    ∃ (S : Multiset (M × N)),
      Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) (Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))
add :
  ∀ (x y : M ⊗[R] N)
    (hx : ∃ (S : Multiset (M × N)), x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S))
    (hy : ∃ (S : Multiset (M × N)), y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)),
    ∃ (S : Multiset (M × N)), x + y = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)
⊢ ∃ (S : Multiset (M × N)), x = Multiset.sum (Multiset.map (fun (i : M × N) ↦ i.1 ⊗ₜ[R] i.2) S)

Tactic:
induction x with
  | zero => exact ⟨0, by simp⟩
  | tmul x y => exact ⟨{(x, y)}, by simp⟩
  | add x y hx hy =>
    obtain ⟨Sx, hx⟩ := hx
    obtain ⟨Sy, hy⟩ := hy
    exact ⟨Sx + Sy, by rw [Multiset.map_add, Multiset.sum_add, hx, hy]⟩

Premises used: Submodule.zero, TensorProduct.tmul, Submodule.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
⊢ Eq (α := M ⊗[R] N) 0 (Finsupp.sum 0 fun (m : M) (n : N) ↦ m ⊗ₜ[R] 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
⊢ ∃ (S : M →₀ N), Eq (α := M ⊗[R] N) 0 (S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n)

Tactic:
exact ⟨0, 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) (Finsupp.sum (Finsupp.single x y) fun (m : M) (n : N) ↦ m ⊗ₜ[R] 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
x : M
y : N
⊢ ∃ (S : M →₀ N), Eq (α := M ⊗[R] N) (x ⊗ₜ[R] y) (S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n)

Tactic:
exact ⟨Finsupp.single x 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 : ∃ (S : M →₀ N), x = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
hy : ∃ (S : M →₀ N), y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
add :
  ∀ (Sx : M →₀ N) (hx : x = Sx.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n),
    ∃ (S : M →₀ N), x + y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n
⊢ ∃ (S : M →₀ N), x + y = S.sum fun (m : M) (n : N) ↦ m ⊗ₜ[R] n

Tactic:
obtain ⟨Sx, hx⟩ := hx