case H.H.H.h.h.h.h
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.721821
inst✝¹³ : Monoid R'
R'' : Type ?u.721827
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
g h : ((M ⊗[R] N) ⊗[R] P) ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), ↑g (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) = ↑h (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
w : M
x : N
y : P
z : Q
⊢ ↑(↑(↑(↑(LinearMap.compr₂ (mk R M N)
                      (LinearMap.compr₂ (mk R (M ⊗[R] N) P) (LinearMap.compr₂ (mk R ((M ⊗[R] N) ⊗[R] P) Q) g)))
                  w)
              x)
          y)
      z =
    ↑(↑(↑(↑(LinearMap.compr₂ (mk R M N)
                      (LinearMap.compr₂ (mk R (M ⊗[R] N) P) (LinearMap.compr₂ (mk R ((M ⊗[R] N) ⊗[R] P) Q) h)))
                  w)
              x)
          y)
      z
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.721821
inst✝¹³ : Monoid R'
R'' : Type ?u.721827
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
g h : ((M ⊗[R] N) ⊗[R] P) ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), ↑g (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) = ↑h (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
⊢ g = h
ext w x y z
no goals
case H.H.H.h.h.h.h
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.721821
inst✝¹³ : Monoid R'
R'' : Type ?u.721827
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
g h : ((M ⊗[R] N) ⊗[R] P) ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), ↑g (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) = ↑h (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
w : M
x : N
y : P
z : Q
⊢ ↑(↑(↑(↑(LinearMap.compr₂ (mk R M N)
                      (LinearMap.compr₂ (mk R (M ⊗[R] N) P) (LinearMap.compr₂ (mk R ((M ⊗[R] N) ⊗[R] P) Q) g)))
                  w)
              x)
          y)
      z =
    ↑(↑(↑(↑(LinearMap.compr₂ (mk R M N)
                      (LinearMap.compr₂ (mk R (M ⊗[R] N) P) (LinearMap.compr₂ (mk R ((M ⊗[R] N) ⊗[R] P) Q) h)))
                  w)
              x)
          y)
      z
exact H w x y z