case H.H.h.h.h
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.714453
inst✝¹³ : Monoid R'
R'' : Type ?u.714459
inst✝¹² : Semiring R''
M : Type u_4
N : Type u_3
P : Type u_2
Q : Type u_5
S : Type ?u.714477
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
H : ∀ (x : M) (y : N) (z : P), ↑g ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = ↑h ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
x : M
y : N
z : P
⊢ ↑(↑(↑(LinearMap.compr₂ (mk R M N) (LinearMap.compr₂ (mk R (M ⊗[R] N) P) g)) x) y) z =
    ↑(↑(↑(LinearMap.compr₂ (mk R M N) (LinearMap.compr₂ (mk R (M ⊗[R] N) P) h)) x) y) z
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.714453
inst✝¹³ : Monoid R'
R'' : Type ?u.714459
inst✝¹² : Semiring R''
M : Type u_4
N : Type u_3
P : Type u_2
Q : Type u_5
S : Type ?u.714477
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
H : ∀ (x : M) (y : N) (z : P), ↑g ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = ↑h ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
⊢ g = h
ext x y z
no goals
case H.H.h.h.h
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.714453
inst✝¹³ : Monoid R'
R'' : Type ?u.714459
inst✝¹² : Semiring R''
M : Type u_4
N : Type u_3
P : Type u_2
Q : Type u_5
S : Type ?u.714477
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
H : ∀ (x : M) (y : N) (z : P), ↑g ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = ↑h ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
x : M
y : N
z : P
⊢ ↑(↑(↑(LinearMap.compr₂ (mk R M N) (LinearMap.compr₂ (mk R (M ⊗[R] N) P) g)) x) y) z =
    ↑(↑(↑(LinearMap.compr₂ (mk R M N) (LinearMap.compr₂ (mk R (M ⊗[R] N) P) h)) x) y) z
exact H x y z