awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Basis
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Finite ι
b : (i : ι) → Basis.{u_4, u_2, u_3} (κ i) R (M i)
p : (i : ι) → κ i
haveI :
  ∀ (this : Fintype ι),
    Eq (α := ⨂[R] (i : ι), M i)
      ((piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) p : ⨂[R] (i : ι), M i)
      (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i) : ⨂[R] (i : ι), M i)
⊢ Eq (α := ⨂[R] (i : ι), M i)
    ((piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) p : ⨂[R] (i : ι), M i)
    (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i) : ⨂[R] (i : ι), M i)

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Basis
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Finite ι
b : (i : ι) → Basis.{u_4, u_2, u_3} (κ i) R (M i)
p : (i : ι) → κ i
this : Fintype ι
⊢ Eq (α := ⨂[R] (i : ι), M i)
    ((piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) p : ⨂[R] (i : ι), M i)
    (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i) : ⨂[R] (i : ι), M i)

Tactic:
(Basis.piTensorProduct b).ext_elem (fun q ↦ ?_)

Premises used: Module.Basis.ext_elem, Basis.piTensorProduct
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Basis
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Finite ι
b : (i : ι) → Basis.{u_4, u_2, u_3} (κ i) R (M i)
p : (i : ι) → κ i
this : Fintype ι
refine :
  ∀ (q : (i : ι) → κ i),
    Eq.{u_2 + 1} (α := R)
      (((((piTensorProduct (M := M) (κ := κ) b).repr : (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
                ((piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) p) :
              ((i : ι) → κ i) →₀ R) :
            (a : (i : ι) → κ i) → R)
          q :
        R)
      ((((piTensorProduct (M := M) (κ := κ) b).repr : (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
              (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i)) :
            (a : (i : ι) → κ i) → R)
          q :
        R)
⊢ Eq (α := ⨂[R] (i : ι), M i)
    ((piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) p : ⨂[R] (i : ι), M i)
    (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i) : ⨂[R] (i : ι), M i)

Tactic:
refine (Basis.piTensorProduct b).ext_elem (fun q ↦ ?_)

Premises used: Module.Basis.ext_elem, Basis.piTensorProduct
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Basis
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Finite ι
b : (i : ι) → Basis.{u_4, u_2, u_3} (κ i) R (M i)
p : (i : ι) → κ i
this : Fintype ι
q : (i : ι) → κ i
⊢ Eq.{u_2 + 1} (α := R)
    (((((piTensorProduct (M := M) (κ := κ) b).repr : (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
              ((piTensorProduct (M := M) (κ := κ) b : (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i) p) :
            ((i : ι) → κ i) →₀ R) :
          (a : (i : ι) → κ i) → R)
        q :
      R)
    ((((piTensorProduct (M := M) (κ := κ) b).repr : (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
            (⨂ₜ[R] (i : ι), (b i : (a : κ i) → M i) (p i)) :
          (a : (i : ι) → κ i) → R)
        q :
      R)

Tactic:
simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]

Premises used: funext_iff, Fintype.prod_ite_zero, Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ Eq (α := Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    ((ofDFinsuppEquiv (κ := κ) (M := M) :
          (a : ⨂[R] (i : ι), Π₀ (j : κ i), M i j) → Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
        ((tprod R (s := fun (i : ι) ↦ Π₀ (j : κ i), M i j) :
            (a : (i : ι) → Π₀ (j : κ i), M i j) → ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (x i)) :
      Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    (DFinsupp.single (β := fun (i : (i : ι) → κ i) ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p
        ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
          x i) :
      Π₀ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))

Tactic:
simp [ofDFinsuppEquiv]

Premises used: PiTensorProduct.ofDFinsuppEquiv
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ Eq (α := ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
    ((LinearEquiv.symm (ofDFinsuppEquiv (κ := κ) (M := M)) :
          (a : Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) → ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
        (DFinsupp.single (β := fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) p
          ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) x)) :
      ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
    ((tprod R (s := fun (i : ι) ↦ Π₀ (i_1 : κ i), M i i_1) :
          (a : (i : ι) → Π₀ (i_1 : κ i), M i i_1) → ⨂[R] (i : ι), Π₀ (i_1 : κ i), M i i_1)
        fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (x i) :
      ⨂[R] (i : ι), Π₀ (i_1 : κ i), M i i_1)

Tactic:
simp [ofDFinsuppEquiv]

Premises used: PiTensorProduct.ofDFinsuppEquiv
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : (i : ι) → DecidableEq (κ i)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ (((ofDFinsuppEquiv (κ := κ) (M := M) :
              (a : ⨂[R] (i : ι), Π₀ (j : κ i), M i j) → Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
            ((tprod R (s := fun (i : ι) ↦ Π₀ (j : κ i), M i j) :
                (a : (i : ι) → Π₀ (j : κ i), M i j) → ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
              x) :
          Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) :
        (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i (a i))
      p =
    (tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
      (x i : (a : κ i) → M i a) (p i)

Tactic:
simpa [ofDFinsuppEquiv, MultilinearMap.fromDFinsuppEquiv_apply] using fun i hi ↦
    ((tprod R).map_coord_zero (m := fun i ↦ x i (p i)) i hi).symm

Premises used: MultilinearMap.fromDFinsuppEquiv_apply, PiTensorProduct.tprod, MultilinearMap.map_coord_zero, PiTensorProduct.ofDFinsuppEquiv, Eq.symm
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : (i : ι) → DecidableEq (κ i)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ (((ofDFinsuppEquiv (κ := κ) (M := M) :
              (a : ⨂[R] (i : ι), Π₀ (j : κ i), M i j) → Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
            ((tprod R (s := fun (i : ι) ↦ Π₀ (j : κ i), M i j) :
                (a : (i : ι) → Π₀ (j : κ i), M i j) → ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
              x) :
          Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) :
        (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i (a i))
      p =
    (tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
      (x i : (a : κ i) → M i a) (p i)

Tactic:
classical
  simpa [ofDFinsuppEquiv, MultilinearMap.fromDFinsuppEquiv_apply] using fun i hi ↦
    ((tprod R).map_coord_zero (m := fun i ↦ x i (p i)) i hi).symm

Premises used: MultilinearMap.fromDFinsuppEquiv_apply, PiTensorProduct.tprod, MultilinearMap.map_coord_zero, PiTensorProduct.ofDFinsuppEquiv, Eq.symm
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ Eq (α := Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    ((ofDFinsuppEquiv (κ := κ) (M := M) :
          (a : ⨂[R] (i : ι), Π₀ (j : κ i), M i j) → Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
        ((tprod R (s := fun (i : ι) ↦ Π₀ (j : κ i), M i j) :
            (a : (i : ι) → Π₀ (j : κ i), M i j) → ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
          fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (x i)) :
      Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    (DFinsupp.single (β := fun (i : (i : ι) → κ i) ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p
        ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
          x i) :
      Π₀ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))

Tactic:
ofDFinsuppEquiv_tprod_single p x

Premises used: PiTensorProduct.ofDFinsuppEquiv_tprod_single
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ Eq (α := ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    ((ofDFinsuppEquiv (κ := κ) (M := fun (i : ι) (j : κ i) ↦ M i j) :
          (a : ⨂[R] (i : ι), ⨁ (j : κ i), M i j) → ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
        ((tprod R (s := fun (i : ι) ↦ ⨁ (j : κ i), M i j) :
            (a : (i : ι) → ⨁ (j : κ i), M i j) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
          fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i)) :
      ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    (((lof R ((i : ι) → κ i) (fun (i : (i : ι) → κ i) ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p :
            (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) :
          (a : ⨂[R] (i : ι), M i (p i)) → ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
        ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
          x i) :
      ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))

Tactic:
convert! ofDFinsuppEquiv_tprod_single p x

Premises used: PiTensorProduct.ofDFinsuppEquiv_tprod_single
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
rw rw₁ rw₂ :
  Eq (α := ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    ((ofDFinsuppEquiv (κ := κ) (M := fun (i : ι) (j : κ i) ↦ M i j) :
          (a : ⨂[R] (i : ι), ⨁ (j : κ i), M i j) → ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
        ((tprod R (s := fun (i : ι) ↦ ⨁ (j : κ i), M i j) :
            (a : (i : ι) → ⨁ (j : κ i), M i j) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
          fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i)) :
      ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    (((lof R ((i : ι) → κ i) (fun (i : (i : ι) → κ i) ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p :
            (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) :
          (a : ⨂[R] (i : ι), M i (p i)) → ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
        ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
          x i) :
      ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
⊢ Eq (α := ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    ((ofDirectSumEquiv (κ := κ) (M := M) :
          (a : ⨂[R] (i : ι), ⨁ (j : κ i), M i j) → ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
        ((tprod R (s := fun (i : ι) ↦ ⨁ (j : κ i), M i j) :
            (a : (i : ι) → ⨁ (j : κ i), M i j) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
          fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i)) :
      ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
    (((lof R ((i : ι) → κ i) (fun (i : (i : ι) → κ i) ↦ ⨂[R] (i_1 : ι), M i_1 (i i_1)) p :
            (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) :
          (a : ⨂[R] (i : ι), M i (p i)) → ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
        ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
          x i) :
      ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))

Tactic:
classical
  rw [ofDirectSumEquiv]
  convert! ofDFinsuppEquiv_tprod_single p x

Premises used: PiTensorProduct.ofDirectSumEquiv
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ Eq (α := ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
    ((LinearEquiv.symm (ofDFinsuppEquiv (κ := κ) (M := M)) :
          (a : Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) → ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
        (DFinsupp.single (β := fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) p
          ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) x)) :
      ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
    ((tprod R (s := fun (i : ι) ↦ Π₀ (i_1 : κ i), M i i_1) :
          (a : (i : ι) → Π₀ (i_1 : κ i), M i i_1) → ⨂[R] (i : ι), Π₀ (i_1 : κ i), M i i_1)
        fun (i : ι) ↦ DFinsupp.single (β := M i) (p i) (x i) :
      ⨂[R] (i : ι), Π₀ (i_1 : κ i), M i i_1)

Tactic:
ofDFinsuppEquiv_symm_single_tprod p x

Premises used: PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ Eq (α := ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
    ((LinearEquiv.symm (ofDFinsuppEquiv (κ := κ) (M := fun (i : ι) (j : κ i) ↦ M i j)) :
          (a : ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
        (((lof R ((i : ι) → κ i) (fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) p :
              (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) :
            (a : ⨂[R] (i : ι), M i (p i)) → ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
          ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) x)) :
      ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
    ((tprod R (s := fun (i : ι) ↦ ⨁ (i_1 : κ i), M i i_1) :
          (a : (i : ι) → ⨁ (i_1 : κ i), M i i_1) → ⨂[R] (i : ι), ⨁ (i_1 : κ i), M i i_1)
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
      ⨂[R] (i : ι), ⨁ (i_1 : κ i), M i i_1)

Tactic:
convert! ofDFinsuppEquiv_symm_single_tprod p x

Premises used: PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Fintype ι
inst_4 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
rw rw₁ rw₂ :
  Eq (α := ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
    ((LinearEquiv.symm (ofDFinsuppEquiv (κ := κ) (M := fun (i : ι) (j : κ i) ↦ M i j)) :
          (a : ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
        (((lof R ((i : ι) → κ i) (fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) p :
              (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) :
            (a : ⨂[R] (i : ι), M i (p i)) → ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
          ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) x)) :
      ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
    ((tprod R (s := fun (i : ι) ↦ ⨁ (i_1 : κ i), M i i_1) :
          (a : (i : ι) → ⨁ (i_1 : κ i), M i i_1) → ⨂[R] (i : ι), ⨁ (i_1 : κ i), M i i_1)
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
      ⨂[R] (i : ι), ⨁ (i_1 : κ i), M i i_1)
⊢ Eq (α := ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
    ((LinearEquiv.symm (ofDirectSumEquiv (κ := κ) (M := M)) :
          (a : ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
        (((lof R ((i : ι) → κ i) (fun (p : (i : ι) → κ i) ↦ ⨂[R] (i : ι), M i (p i)) p :
              (⨂[R] (i : ι), M i (p i)) →ₗ[R] ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1)) :
            (a : ⨂[R] (i : ι), M i (p i)) → ⨁ (i : (i : ι) → κ i), ⨂[R] (i_1 : ι), M i_1 (i i_1))
          ((tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) x)) :
      ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
    ((tprod R (s := fun (i : ι) ↦ ⨁ (i_1 : κ i), M i i_1) :
          (a : (i : ι) → ⨁ (i_1 : κ i), M i i_1) → ⨂[R] (i : ι), ⨁ (i_1 : κ i), M i i_1)
        fun (i : ι) ↦ (lof R (κ i) (M i) (p i) : (a : M i (p i)) → ⨁ (i_1 : κ i), M i i_1) (x i) :
      ⨂[R] (i : ι), ⨁ (i_1 : κ i), M i i_1)

Tactic:
classical
  rw [ofDirectSumEquiv]
  convert! ofDFinsuppEquiv_symm_single_tprod p x

Premises used: PiTensorProduct.ofDirectSumEquiv
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Finite ι
x : (i : ι) → ⨁ (j : κ i), M i j
p : (i : ι) → κ i
have :
  ∀ (this : Fintype ι),
    (((ofDirectSumEquiv (κ := κ) (M := M) :
                (a : ⨂[R] (i : ι), ⨁ (j : κ i), M i j) → ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
              ((tprod R (s := fun (i : ι) ↦ ⨁ (j : κ i), M i j) :
                  (a : (i : ι) → ⨁ (j : κ i), M i j) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
                x) :
            ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) :
          (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i (a i))
        p =
      (tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
        (x i : (a : κ i) → M i a) (p i)
⊢ (((ofDirectSumEquiv (κ := κ) (M := M) :
              (a : ⨂[R] (i : ι), ⨁ (j : κ i), M i j) → ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
            ((tprod R (s := fun (i : ι) ↦ ⨁ (j : κ i), M i j) :
                (a : (i : ι) → ⨁ (j : κ i), M i j) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
              x) :
          ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) :
        (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i (a i))
      p =
    (tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
      (x i : (a : κ i) → M i a) (p i)

Tactic:
have : Fintype ι := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Finite ι
x : (i : ι) → ⨁ (j : κ i), M i j
p : (i : ι) → κ i
this : Fintype ι
⊢ (((ofDFinsuppEquiv (κ := κ) (M := fun (i : ι) (j : κ i) ↦ M i j) :
              (a : ⨂[R] (i : ι), Π₀ (j : κ i), M i j) → Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
            ((tprod R (s := fun (i : ι) ↦ Π₀ (j : κ i), M i j) :
                (a : (i : ι) → Π₀ (j : κ i), M i j) → ⨂[R] (i : ι), Π₀ (j : κ i), M i j)
              x) :
          Π₀ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) :
        (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i (a i))
      p =
    (tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
      (x i : (a : κ i) → M i a) (p i)

Tactic:
ofDFinsuppEquiv_tprod_apply _ _

Premises used: PiTensorProduct.ofDFinsuppEquiv_tprod_apply
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst_2 : (i : ι) → (j : κ i) → Module.{u_1, u_4} R (M i j)
inst_3 : Finite ι
x : (i : ι) → ⨁ (j : κ i), M i j
p : (i : ι) → κ i
this : Fintype ι
⊢ (((ofDirectSumEquiv (κ := κ) (M := M) :
              (a : ⨂[R] (i : ι), ⨁ (j : κ i), M i j) → ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i))
            ((tprod R (s := fun (i : ι) ↦ ⨁ (j : κ i), M i j) :
                (a : (i : ι) → ⨁ (j : κ i), M i j) → ⨂[R] (i : ι), ⨁ (j : κ i), M i j)
              x) :
          ⨁ (p : (i : ι) → κ i), ⨂[R] (i : ι), M i (p i)) :
        (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i (a i))
      p =
    (tprod R (s := fun (i : ι) ↦ M i (p i)) : (a : (i : ι) → M i (p i)) → ⨂[R] (i : ι), M i (p i)) fun (i : ι) ↦
      (x i : (a : κ i) → M i a) (p i)

Tactic:
convert! ofDFinsuppEquiv_tprod_apply _ _

Premises used: PiTensorProduct.ofDFinsuppEquiv_tprod_apply
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Fintype ι
f : (i : ι) → Dual.{u_2, u_3} R (M i)
m : (i : ι) → M i
rw :
  Eq.{u_2 + 1} (α := R)
    (((compRight R (AlgEquiv.toLinearMap (constantBaseRingEquiv ι R)) ∘ₗ
                piTensorHomMap (s := M) (t := fun (i : ι) ↦ R) :
              (a : ⨂[R] (i : ι), Dual R (M i)) → Dual R (⨂[R] (i : ι), M i))
            ((tprod R (s := fun (i : ι) ↦ Dual.{u_2, u_3} R (M i)) :
                (a : (i : ι) → Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
              fun (i : ι) ↦ f i) :
          (a : ⨂[R] (i : ι), M i) → R)
        (⨂ₜ[R] (i : ι), m i) :
      R)
    (∏ i : ι, (f i : (a : M i) → R) (m i) : R)
⊢ Eq.{u_2 + 1} (α := R)
    (((dualDistrib (M := M) : (a : ⨂[R] (i : ι), Dual R (M i)) → Dual R (⨂[R] (i : ι), M i))
            ((tprod R (s := fun (i : ι) ↦ Dual.{u_2, u_3} R (M i)) :
                (a : (i : ι) → Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
              fun (i : ι) ↦ f i) :
          (a : ⨂[R] (i : ι), M i) → R)
        (⨂ₜ[R] (i : ι), m i) :
      R)
    (∏ i : ι, (f i : (a : M i) → R) (m i) : R)

Tactic:
rw [dualDistrib, Subsingleton.elim (Fintype.ofFinite ι) ‹_›]

Premises used: Fintype.ofFinite, PiTensorProduct.dualDistrib, Subsingleton.elim