Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case hl.fst
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : M
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N) x✝).1 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inl R M N) x✝).1

pp: case hl.snd
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : M
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N) x✝).2 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inl R M N) x✝).2

pp: case hr.fst
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : N
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N) x✝).1 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inr R M N) x✝).1

pp: case hr.snd
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : N
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N) x✝).2 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inr R M N) x✝).2

Tactic:
<;>

Goal state after:
case hl.fst
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : M
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N) x✝).1 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inl R M N) x✝).1

case hl.snd
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : M
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N) x✝).2 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inl R M N) x✝).2

case hr.fst
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : N
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N) x✝).1 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inr R M N) x✝).1

case hr.snd
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : N
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N) x✝).2 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inr R M N) x✝).2