case h
R : Type u_4
R₁ : Type ?u.2165977
R₂ : Type ?u.2165980
R₃ : Type ?u.2165983
R₄ : Type ?u.2165986
S : Type ?u.2165989
K : Type ?u.2165992
K₂ : Type ?u.2165995
M : Type u_5
M' : Type ?u.2166001
M₁ : Type ?u.2166004
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type ?u.2166013
N✝ : Type ?u.2166016
N₂✝ : Type ?u.2166019
ι : Type ?u.2166022
V : Type ?u.2166025
V₂ : Type ?u.2166028
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
N : Type u_1
N₂ : Type u_2
N₃ : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R N
inst✝¹ : Module R N₂
inst✝ : Module R N₃
e₁ : M ≃ₗ[R] N
e₂ : M₂ ≃ₗ[R] N₂
e₃ : M₃ ≃ₗ[R] N₃
f : M →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
x✝ : N
⊢ ↑(↑(arrowCongr e₁ e₃) (LinearMap.comp g f)) x✝ = ↑(LinearMap.comp (↑(arrowCongr e₂ e₃) g) (↑(arrowCongr e₁ e₂) f)) x✝
R : Type u_4
R₁ : Type ?u.2165977
R₂ : Type ?u.2165980
R₃ : Type ?u.2165983
R₄ : Type ?u.2165986
S : Type ?u.2165989
K : Type ?u.2165992
K₂ : Type ?u.2165995
M : Type u_5
M' : Type ?u.2166001
M₁ : Type ?u.2166004
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type ?u.2166013
N✝ : Type ?u.2166016
N₂✝ : Type ?u.2166019
ι : Type ?u.2166022
V : Type ?u.2166025
V₂ : Type ?u.2166028
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
N : Type u_1
N₂ : Type u_2
N₃ : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R N
inst✝¹ : Module R N₂
inst✝ : Module R N₃
e₁ : M ≃ₗ[R] N
e₂ : M₂ ≃ₗ[R] N₂
e₃ : M₃ ≃ₗ[R] N₃
f : M →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
⊢ ↑(arrowCongr e₁ e₃) (LinearMap.comp g f) = LinearMap.comp (↑(arrowCongr e₂ e₃) g) (↑(arrowCongr e₁ e₂) f)
ext
no goals
case h
R : Type u_4
R₁ : Type ?u.2165977
R₂ : Type ?u.2165980
R₃ : Type ?u.2165983
R₄ : Type ?u.2165986
S : Type ?u.2165989
K : Type ?u.2165992
K₂ : Type ?u.2165995
M : Type u_5
M' : Type ?u.2166001
M₁ : Type ?u.2166004
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type ?u.2166013
N✝ : Type ?u.2166016
N₂✝ : Type ?u.2166019
ι : Type ?u.2166022
V : Type ?u.2166025
V₂ : Type ?u.2166028
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
N : Type u_1
N₂ : Type u_2
N₃ : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R N
inst✝¹ : Module R N₂
inst✝ : Module R N₃
e₁ : M ≃ₗ[R] N
e₂ : M₂ ≃ₗ[R] N₂
e₃ : M₃ ≃ₗ[R] N₃
f : M →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
x✝ : N
⊢ ↑(↑(arrowCongr e₁ e₃) (LinearMap.comp g f)) x✝ = ↑(LinearMap.comp (↑(arrowCongr e₂ e₃) g) (↑(arrowCongr e₁ e₂) f)) x✝
simp only [symm_apply_apply, arrowCongr_apply, LinearMap.comp_apply]