case H.H.h.h.H.h.h
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.731485
inst✝¹³ : Monoid R'
R'' : Type ?u.731491
inst✝¹² : Semiring R''
M : Type u_5
N : Type u_4
P : Type u_3
Q : Type u_2
S : Type u_6
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] N →ₗ[R] P
φ ψ : (M ⊗[R] N) ⊗[R] P ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), ↑φ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z) = ↑ψ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z)
m : M
n : N
p : P
q : Q
⊢ ↑(↑(LinearMap.compr₂ (mk R P Q)
              (↑(↑(LinearMap.compr₂ (mk R M N) (LinearMap.compr₂ (mk R (M ⊗[R] N) (P ⊗[R] Q)) φ)) m) n))
          p)
      q =
    ↑(↑(LinearMap.compr₂ (mk R P Q)
              (↑(↑(LinearMap.compr₂ (mk R M N) (LinearMap.compr₂ (mk R (M ⊗[R] N) (P ⊗[R] Q)) ψ)) m) n))
          p)
      q
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.731485
inst✝¹³ : Monoid R'
R'' : Type ?u.731491
inst✝¹² : Semiring R''
M : Type u_5
N : Type u_4
P : Type u_3
Q : Type u_2
S : Type u_6
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] N →ₗ[R] P
φ ψ : (M ⊗[R] N) ⊗[R] P ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), ↑φ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z) = ↑ψ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z)
⊢ φ = ψ
ext m n p q
no goals
case H.H.h.h.H.h.h
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.731485
inst✝¹³ : Monoid R'
R'' : Type ?u.731491
inst✝¹² : Semiring R''
M : Type u_5
N : Type u_4
P : Type u_3
Q : Type u_2
S : Type u_6
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] N →ₗ[R] P
φ ψ : (M ⊗[R] N) ⊗[R] P ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), ↑φ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z) = ↑ψ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z)
m : M
n : N
p : P
q : Q
⊢ ↑(↑(LinearMap.compr₂ (mk R P Q)
              (↑(↑(LinearMap.compr₂ (mk R M N) (LinearMap.compr₂ (mk R (M ⊗[R] N) (P ⊗[R] Q)) φ)) m) n))
          p)
      q =
    ↑(↑(LinearMap.compr₂ (mk R P Q)
              (↑(↑(LinearMap.compr₂ (mk R M N) (LinearMap.compr₂ (mk R (M ⊗[R] N) (P ⊗[R] Q)) ψ)) m) n))
          p)
      q
exact H m n p q