Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case 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
z : M ⊗[R] N
x✝ y✝ : Dual R N ⊗[R] Dual R M
a✝¹ :
  ((dualDistrib R N M) x✝) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝)) z
a✝ :
  ((dualDistrib R N M) y✝) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝)) z
⊢ ((dualDistrib R N M) (x✝ + y✝)) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ + y✝))) z

Tactic:
induction z

Goal state after:
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✝)