Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case zero.zero
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) 0

pp: case zero.tmul
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M
y✝ : N
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) (x✝ ⊗ₜ[R] y✝)

pp: case zero.add
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y✝ : M ⊗[R] N
a✝¹ :
  ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) x✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) x✝
a✝ :
  ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) y✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) y✝
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) (x✝ + y✝)

pp: case tmul.zero
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : Dual R N
y✝ : Dual R M
⊢ ((dualDistrib R N M) (x✝ ⊗ₜ[R] y✝)) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ ⊗ₜ[R] y✝))) 0

pp: case tmul.tmul
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : Dual R N
y✝¹ : Dual R M
x✝ : M
y✝ : N
⊢ ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) (x✝ ⊗ₜ[R] y✝)

pp: case tmul.add
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : Dual R N
y✝¹ : Dual R M
x✝ y✝ : M ⊗[R] N
a✝¹ :
  ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) x✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) x✝
a✝ :
  ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) y✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) y✝
⊢ ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) (x✝ + y✝)

pp: case add.zero
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y✝ : Dual R N ⊗[R] Dual R M
a✝¹ :
  ((dualDistrib R N M) x✝) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝)) 0
a✝ :
  ((dualDistrib R N M) y✝) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝)) 0
⊢ ((dualDistrib R N M) (x✝ + y✝)) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ + y✝))) 0

pp: case add.tmul
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ y✝¹ : Dual R N ⊗[R] Dual R M
x✝ : M
y✝ : N
a✝¹ :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) (x✝ ⊗ₜ[R] y✝)
a✝ :
  ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) (x✝ ⊗ₜ[R] y✝)
⊢ ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) (x✝ ⊗ₜ[R] y✝)

pp: case add.add
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ y✝¹ : Dual R N ⊗[R] Dual R M
x✝ y✝ : M ⊗[R] N
a✝³ :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) x✝) =
      ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) x✝ →
    ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) x✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) x✝ →
      ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) x✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) x✝
a✝² :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) y✝) =
      ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) y✝ →
    ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) y✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) y✝ →
      ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) y✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) y✝
a✝¹ :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) (x✝ + y✝)
a✝ :
  ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) (x✝ + y✝)
⊢ ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) (x✝ + y✝)

Tactic:
<;>

Goal state after:
case zero.zero
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) 0

case zero.tmul
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M
y✝ : N
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) (x✝ ⊗ₜ[R] y✝)

case zero.add
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y✝ : M ⊗[R] N
a✝¹ :
  ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) x✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) x✝
a✝ :
  ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) y✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) y✝
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) (x✝ + y✝)

case tmul.zero
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : Dual R N
y✝ : Dual R M
⊢ ((dualDistrib R N M) (x✝ ⊗ₜ[R] y✝)) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ ⊗ₜ[R] y✝))) 0

case tmul.tmul
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : Dual R N
y✝¹ : Dual R M
x✝ : M
y✝ : N
⊢ ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) (x✝ ⊗ₜ[R] y✝)

case tmul.add
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : Dual R N
y✝¹ : Dual R M
x✝ y✝ : M ⊗[R] N
a✝¹ :
  ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) x✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) x✝
a✝ :
  ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) y✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) y✝
⊢ ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) (x✝ + y✝)

case add.zero
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y✝ : Dual R N ⊗[R] Dual R M
a✝¹ :
  ((dualDistrib R N M) x✝) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝)) 0
a✝ :
  ((dualDistrib R N M) y✝) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝)) 0
⊢ ((dualDistrib R N M) (x✝ + y✝)) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ + y✝))) 0

case add.tmul
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ y✝¹ : Dual R N ⊗[R] Dual R M
x✝ : M
y✝ : N
a✝¹ :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) (x✝ ⊗ₜ[R] y✝)
a✝ :
  ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) (x✝ ⊗ₜ[R] y✝)
⊢ ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) (x✝ ⊗ₜ[R] y✝)

case add.add
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ y✝¹ : Dual R N ⊗[R] Dual R M
x✝ y✝ : M ⊗[R] N
a✝³ :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) x✝) =
      ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) x✝ →
    ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) x✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) x✝ →
      ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) x✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) x✝
a✝² :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) y✝) =
      ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) y✝ →
    ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) y✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) y✝ →
      ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) y✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) y✝
a✝¹ :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) (x✝ + y✝)
a✝ :
  ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) (x✝ + y✝)
⊢ ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) (x✝ + y✝)