awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : p i ≠ q i
h : Eq.{uM + 1} (α := M i (q i)) ((fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) i (q i)) 0
⊢ Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    0

Tactic:
apply (f q).map_coord_zero i

Premises used: MultilinearMap.map_coord_zero
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : p i ≠ q i
h h₁ : Eq (α := M i (q i)) (Pi.single (M := M i) (p i) (m i) (q i)) 0
⊢ Eq.{uM + 1} (α := M i (q i)) ((fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) i (q i)) 0

Tactic:
simp_rw [Pi.single_eq_of_ne' hpqi]

Premises used: Pi.single_eq_of_ne'
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
h :
  ∀ (p' : (i : ι) → κ i),
    Eq.{uN + 1} (α := N p')
      ((piFamily (κ := κ) (M := M) (N := N)
              (Pi.single (M := fun (p : (i : ι) → κ i) ↦
                MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
            (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
          x p' :
        N p')
      (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p' : N p')
⊢ Eq (α := (t : (i : ι) → κ i) → N t)
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x :
      (t : (i : ι) → κ i) → N t)
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) : (j : (i : ι) → κ i) → N j)

Tactic:
ext p'
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
p' : (i : ι) → κ i
h :
  Eq.{uN + 1} (α := N p)
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x p :
      N p)
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p : N p)
h₁ :
  ∀ (hp : p ≠ p'),
    Eq.{uN + 1} (α := N p')
      ((piFamily (κ := κ) (M := M) (N := N)
              (Pi.single (M := fun (p : (i : ι) → κ i) ↦
                MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
            (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
          x p' :
        N p')
      (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p' : N p')
⊢ Eq.{uN + 1} (α := N p')
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x p' :
      N p')
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p' : N p')

Tactic:
obtain rfl | hp := eq_or_ne p p'

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
⊢ Eq.{uN + 1} (α := N p)
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x p :
      N p)
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p : N p)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
p' : (i : ι) → κ i
hp : p ≠ p'
⊢ Eq.{uN + 1} (α := N p')
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x p' :
      N p')
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p' : N p')

Tactic:
simp [hp]
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
⊢ Eq (α := MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) ((t : (i : ι) → κ i) → N t))
    (piFamily (κ := κ) (M := M) (N := N)
      (Pi.single (M := fun (p : (i : ι) → κ i) ↦ MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p
        f))
    (LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ (i_1 : κ i) → M i i_1) (LinearMap.single R N p)
      (f.compLinearMap (M₁ := fun (i : ι) ↦ (i_1 : κ i) → M i i_1) (M₁' := fun (i : ι) ↦ M i (p i)) fun (i : ι) ↦
        LinearMap.proj (φ := M i) (p i)))

Tactic:
ext <| piFamily_single_left_apply _ _

Premises used: MultilinearMap.piFamily_single_left_apply, MultilinearMap.ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
⊢ ((piFamily (κ := κ) (M := M) (N := N) f).compLinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (M₁' := fun (i : ι) ↦
      (j : κ i) → M i j) fun (i : ι) ↦ LinearMap.single R (M i) (p i)) =
    LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ M i (p i)) (LinearMap.single R N p) (f p)

Tactic:
MultilinearMap.ext <| piFamily_single f p

Premises used: MultilinearMap.ext, MultilinearMap.piFamily_single
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
H :
  ∀ (x : (i : ι) → (j : κ i) → M i j) (x_1 : (i : ι) → κ i),
    Eq.{uN + 1} (α := N x_1)
      ((piFamily (κ := κ) (M := M) (N := N) 0 : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x x_1 :
        N x_1)
      ((0 : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x x_1 : N x_1)
⊢ Eq (α := MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) ((t : (i : ι) → κ i) → N t))
    (piFamily (κ := κ) (M := M) (N := N) 0) 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
x : (i : ι) → (j : κ i) → M i j
x_1 : (i : ι) → κ i
⊢ Eq.{uN + 1} (α := N x_1)
    ((piFamily (κ := κ) (M := M) (N := N) 0 : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x x_1 :
      N x_1)
    ((0 : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x x_1 : N x_1)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
H :
  ∀ (x : (i : ι) → (j : κ i) → M i j) (x_1 : (i : ι) → κ i),
    Eq.{uN + 1} (α := N x_1)
      ((piFamily (κ := κ) (M := M) (N := N) (f + g) : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x
          x_1 :
        N x_1)
      ((piFamily (κ := κ) (M := M) (N := N) f + piFamily (κ := κ) (M := M) (N := N) g :
            (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
          x x_1 :
        N x_1)
⊢ piFamily (κ := κ) (M := M) (N := N) (f + g) =
    piFamily (κ := κ) (M := M) (N := N) f + piFamily (κ := κ) (M := M) (N := N) g

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
x_1 : (i : ι) → κ i
⊢ Eq.{uN + 1} (α := N x_1)
    ((piFamily (κ := κ) (M := M) (N := N) (f + g) : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x
        x_1 :
      N x_1)
    ((piFamily (κ := κ) (M := M) (N := N) f + piFamily (κ := κ) (M := M) (N := N) g :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x x_1 :
      N x_1)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Monoid S
inst_6 : (p : (i : ι) → κ i) → DistribMulAction.{uS, uN} S (N p)
inst_7 : ∀ (p : (i : ι) → κ i), SMulCommClass.{uR, uS, uN} R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
H :
  ∀ (x : (i : ι) → (j : κ i) → M i j) (x_1 : (i : ι) → κ i),
    Eq.{uN + 1} (α := N x_1)
      ((piFamily (κ := κ) (M := M) (N := N) (s • f) : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x
          x_1 :
        N x_1)
      ((s • piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x
          x_1 :
        N x_1)
⊢ piFamily (κ := κ) (M := M) (N := N) (s • f) = s • piFamily (κ := κ) (M := M) (N := N) f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Pi
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Monoid S
inst_6 : (p : (i : ι) → κ i) → DistribMulAction.{uS, uN} S (N p)
inst_7 : ∀ (p : (i : ι) → κ i), SMulCommClass.{uR, uS, uN} R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
x_1 : (i : ι) → κ i
⊢ Eq.{uN + 1} (α := N x_1)
    ((piFamily (κ := κ) (M := M) (N := N) (s • f) : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x
        x_1 :
      N x_1)
    ((s • piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x x_1 :
      N x_1)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst_6 : (i : ι₁ ⊕ ι₂) → Module.{u_1, u_8} R (N i)
a : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (i₁ : ι₁) ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) N₂
inst_7 : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
val : ι₁
x y : N (Sum.inl val)
this : DecidableEq ι₁ := Classical.decEq ι₁
⊢ (((a : (a : (i : ι₁) → N (Sum.inl i)) → N₁) fun (i₁ : ι₁) ↦
        Function.update (β := N) m (Sum.inl val) (x + y) (Sum.inl i₁)) ⊗ₜ[R]
      (b : (a : (i : ι₂) → N (Sum.inr i)) → N₂) fun (i₂ : ι₂) ↦
        Function.update (β := N) m (Sum.inl val) (x + y) (Sum.inr i₂)) =
    HAdd.hAdd (α := N₁ ⊗[R] N₂) (β := N₁ ⊗[R] N₂)
      (((a : (a : (i : ι₁) → N (Sum.inl i)) → N₁) fun (i₁ : ι₁) ↦
            Function.update (β := N) m (Sum.inl val) x (Sum.inl i₁)) ⊗ₜ[R]
          (b : (a : (i : ι₂) → N (Sum.inr i)) → N₂) fun (i₂ : ι₂) ↦
            Function.update (β := N) m (Sum.inl val) x (Sum.inr i₂) :
        N₁ ⊗[R] N₂)
      (((a : (a : (i : ι₁) → N (Sum.inl i)) → N₁) fun (i₁ : ι₁) ↦
            Function.update (β := N) m (Sum.inl val) y (Sum.inl i₁)) ⊗ₜ[R]
          (b : (a : (i : ι₂) → N (Sum.inr i)) → N₂) fun (i₂ : ι₂) ↦
            Function.update (β := N) m (Sum.inl val) y (Sum.inr i₂) :
        N₁ ⊗[R] N₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst_6 : (i : ι₁ ⊕ ι₂) → Module.{u_1, u_8} R (N i)
a : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (i₁ : ι₁) ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) N₂
inst_7 : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
val : ι₂
x y : N (Sum.inr val)
this : DecidableEq ι₂ := Classical.decEq ι₂
⊢ (((a : (a : (i : ι₁) → N (Sum.inl i)) → N₁) fun (i₁ : ι₁) ↦
        Function.update (β := N) m (Sum.inr val) (x + y) (Sum.inl i₁)) ⊗ₜ[R]
      (b : (a : (i : ι₂) → N (Sum.inr i)) → N₂) fun (i₂ : ι₂) ↦
        Function.update (β := N) m (Sum.inr val) (x + y) (Sum.inr i₂)) =
    HAdd.hAdd (α := N₁ ⊗[R] N₂) (β := N₁ ⊗[R] N₂)
      (((a : (a : (i : ι₁) → N (Sum.inl i)) → N₁) fun (i₁ : ι₁) ↦
            Function.update (β := N) m (Sum.inr val) x (Sum.inl i₁)) ⊗ₜ[R]
          (b : (a : (i : ι₂) → N (Sum.inr i)) → N₂) fun (i₂ : ι₂) ↦
            Function.update (β := N) m (Sum.inr val) x (Sum.inr i₂) :
        N₁ ⊗[R] N₂)
      (((a : (a : (i : ι₁) → N (Sum.inl i)) → N₁) fun (i₁ : ι₁) ↦
            Function.update (β := N) m (Sum.inr val) y (Sum.inl i₁)) ⊗ₜ[R]
          (b : (a : (i : ι₂) → N (Sum.inr i)) → N₂) fun (i₂ : ι₂) ↦
            Function.update (β := N) m (Sum.inr val) y (Sum.inr i₂) :
        N₁ ⊗[R] N₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst_6 : (i : ι₁ ⊕ ι₂) → Module.{u_1, u_8} R (N i)
a : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (i₁ : ι₁) ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) N₂
inst_7 : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
i₁ : ι₁
p : R
q : N (Sum.inl i₁)
this : DecidableEq ι₁ := Classical.decEq ι₁
⊢ (((a : (a : (i : ι₁) → N (Sum.inl i)) → N₁) fun (i₁_1 : ι₁) ↦
        Function.update (β := N) m (Sum.inl i₁) (p • q) (Sum.inl i₁_1)) ⊗ₜ[R]
      (b : (a : (i : ι₂) → N (Sum.inr i)) → N₂) fun (i₂ : ι₂) ↦
        Function.update (β := N) m (Sum.inl i₁) (p • q) (Sum.inr i₂)) =
    HSMul.hSMul (β := N₁ ⊗[R] N₂) p
      (((a : (a : (i : ι₁) → N (Sum.inl i)) → N₁) fun (i₁_1 : ι₁) ↦
            Function.update (β := N) m (Sum.inl i₁) q (Sum.inl i₁_1)) ⊗ₜ[R]
          (b : (a : (i : ι₂) → N (Sum.inr i)) → N₂) fun (i₂ : ι₂) ↦
            Function.update (β := N) m (Sum.inl i₁) q (Sum.inr i₂) :
        N₁ ⊗[R] N₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst_6 : (i : ι₁ ⊕ ι₂) → Module.{u_1, u_8} R (N i)
a : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (i₁ : ι₁) ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) N₂
inst_7 : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
i₂ : ι₂
p : R
q : N (Sum.inr i₂)
this : DecidableEq ι₂ := Classical.decEq ι₂
⊢ (((a : (a : (i : ι₁) → N (Sum.inl i)) → N₁) fun (i₁ : ι₁) ↦
        Function.update (β := N) m (Sum.inr i₂) (p • q) (Sum.inl i₁)) ⊗ₜ[R]
      (b : (a : (i : ι₂) → N (Sum.inr i)) → N₂) fun (i₂_1 : ι₂) ↦
        Function.update (β := N) m (Sum.inr i₂) (p • q) (Sum.inr i₂_1)) =
    HSMul.hSMul (β := N₁ ⊗[R] N₂) p
      (((a : (a : (i : ι₁) → N (Sum.inl i)) → N₁) fun (i₁ : ι₁) ↦
            Function.update (β := N) m (Sum.inr i₂) q (Sum.inl i₁)) ⊗ₜ[R]
          (b : (a : (i : ι₂) → N (Sum.inr i)) → N₂) fun (i₂_1 : ι₂) ↦
            Function.update (β := N) m (Sum.inr i₂) q (Sum.inr i₂_1) :
        N₁ ⊗[R] N₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst_6 : (i : ι₁ ⊕ ι₂) → Module.{u_1, u_8} R (N i)
⊢ ∀ (m₁ m₂ : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (i₁ : ι₁) ↦ N (Sum.inl i₁)) N₁)
    (n : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) N₂),
    (m₁ + m₂).domCoprodDep (N := N) n = m₁.domCoprodDep (N := N) n + m₂.domCoprodDep (N := N) n

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst_6 : (i : ι₁ ⊕ ι₂) → Module.{u_1, u_8} R (N i)
⊢ ∀ (c : R) (m : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (i₁ : ι₁) ↦ N (Sum.inl i₁)) N₁)
    (n : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) N₂),
    (c • m).domCoprodDep (N := N) n = c • m.domCoprodDep (N := N) n

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst_6 : (i : ι₁ ⊕ ι₂) → Module.{u_1, u_8} R (N i)
⊢ ∀ (m : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (i₁ : ι₁) ↦ N (Sum.inl i₁)) N₁)
    (n₁ n₂ : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) N₂),
    m.domCoprodDep (N := N) (n₁ + n₂) = m.domCoprodDep (N := N) n₁ + m.domCoprodDep (N := N) n₂

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst_6 : (i : ι₁ ⊕ ι₂) → Module.{u_1, u_8} R (N i)
⊢ ∀ (c : R) (m : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (i₁ : ι₁) ↦ N (Sum.inl i₁)) N₁)
    (n : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) N₂),
    m.domCoprodDep (N := N) (c • n) = c • m.domCoprodDep (N := N) n

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst_6 : (i : ι₁ ⊕ ι₂) → Module.{u_1, u_8} R (N i)
a : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (i₁ : ι₁) ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) N₂
⊢ (domCoprodDep' (N := N) :
        (a :
            MultilinearMap R (fun (i₁ : ι₁) ↦ N (Sum.inl i₁)) N₁ ⊗[R]
              MultilinearMap R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) N₂) →
          MultilinearMap R N (N₁ ⊗[R] N₂))
      (a ⊗ₜ[R] b) =
    a.domCoprodDep (N := N) b

Tactic:
rfl