[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✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
p q : N
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (p + q)) =
    (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p) +
      (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i q)
[PROOFSTEP]
letI := (@Sum.inl_injective ι₁ ι₂).decidableEq
[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✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
p q : N
this : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (p + q)) =
    (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p) +
      (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i q)
[PROOFSTEP]
letI := (@Sum.inr_injective ι₁ ι₂).decidableEq
[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✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
p q : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (p + q)) =
    (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p) +
      (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i q)
[PROOFSTEP]
cases i
[GOAL]
case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
p q : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
val✝ : ι₁
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inl val✝) (p + q)) =
    (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inl val✝) p) +
      (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inl val✝) q)
[PROOFSTEP]
simp [TensorProduct.add_tmul, TensorProduct.tmul_add]
[GOAL]
case inr
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
p q : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
val✝ : ι₂
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inr val✝) (p + q)) =
    (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inr val✝) p) +
      (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inr val✝) q)
[PROOFSTEP]
simp [TensorProduct.add_tmul, TensorProduct.tmul_add]
[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✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
c : R
p : N
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (c • p)) =
    c • (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p)
[PROOFSTEP]
letI := (@Sum.inl_injective ι₁ ι₂).decidableEq
[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✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
c : R
p : N
this : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (c • p)) =
    c • (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p)
[PROOFSTEP]
letI := (@Sum.inr_injective ι₁ ι₂).decidableEq
[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✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
i : ι₁ ⊕ ι₂
c : R
p : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i (c • p)) =
    c • (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ i p)
[PROOFSTEP]
cases i
[GOAL]
case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
c : R
p : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
val✝ : ι₁
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inl val✝) (c • p)) =
    c • (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inl val✝) p)
[PROOFSTEP]
simp [TensorProduct.smul_tmul', TensorProduct.tmul_smul]
[GOAL]
case inr
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : Type u_8
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
a : MultilinearMap R (fun x => N) N₁
b : MultilinearMap R (fun x => N) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
x✝ : ι₁ ⊕ ι₂ → N
c : R
p : N
this✝ : DecidableEq ι₁ := Function.Injective.decidableEq (_ : Function.Injective Sum.inl)
this : DecidableEq ι₂ := Function.Injective.decidableEq (_ : Function.Injective Sum.inr)
val✝ : ι₂
⊢ (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inr val✝) (c • p)) =
    c • (fun v => (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)) (Function.update x✝ (Sum.inr val✝) p)
[PROOFSTEP]
simp [TensorProduct.smul_tmul', TensorProduct.tmul_smul]
[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✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m₁ m₂ : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
⊢ domCoprod (m₁ + m₂) n = domCoprod m₁ n + domCoprod m₂ n
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m₁ m₂ : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
x✝ : ι₁ ⊕ ι₂ → N
⊢ ↑(domCoprod (m₁ + m₂) n) x✝ = ↑(domCoprod m₁ n + domCoprod m₂ n) x✝
[PROOFSTEP]
simp only [domCoprod_apply, TensorProduct.add_tmul, add_apply]
[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✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
c : R
m : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
⊢ domCoprod (c • m) n = c • domCoprod m n
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
c : R
m : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
x✝ : ι₁ ⊕ ι₂ → N
⊢ ↑(domCoprod (c • m) n) x✝ = ↑(c • domCoprod m n) x✝
[PROOFSTEP]
simp only [domCoprod_apply, TensorProduct.smul_tmul', smul_apply]
[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✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m : MultilinearMap R (fun x => N) N₁
n₁ n₂ : MultilinearMap R (fun x => N) N₂
⊢ domCoprod m (n₁ + n₂) = domCoprod m n₁ + domCoprod m n₂
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
m : MultilinearMap R (fun x => N) N₁
n₁ n₂ : MultilinearMap R (fun x => N) N₂
x✝ : ι₁ ⊕ ι₂ → N
⊢ ↑(domCoprod m (n₁ + n₂)) x✝ = ↑(domCoprod m n₁ + domCoprod m n₂) x✝
[PROOFSTEP]
simp only [domCoprod_apply, TensorProduct.tmul_add, add_apply]
[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✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
c : R
m : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
⊢ domCoprod m (c • n) = c • domCoprod m n
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
c : R
m : MultilinearMap R (fun x => N) N₁
n : MultilinearMap R (fun x => N) N₂
x✝ : ι₁ ⊕ ι₂ → N
⊢ ↑(domCoprod m (c • n)) x✝ = ↑(c • domCoprod m n) x✝
[PROOFSTEP]
simp only [domCoprod_apply, TensorProduct.tmul_smul, smul_apply]
