case H.H
R : Type u
A₁ : Type v
A₂ : Type w
A₃ : Type u₁
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Algebra R A₁
inst✝⁷ : Algebra R A₂
inst✝⁶ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
A₁' : Type u_1
A₂' : Type u_2
A₃' : Type u_3
inst✝⁵ : Semiring A₁'
inst✝⁴ : Semiring A₂'
inst✝³ : Semiring A₃'
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e₁ : A₁ ≃ₐ[R] A₂
e₁' : A₁' ≃ₐ[R] A₂'
e₂ : A₂ ≃ₐ[R] A₃
e₂' : A₂' ≃ₐ[R] A₃'
x✝¹ : A₁ →ₐ[R] A₁'
x✝ : A₃
⊢ ↑(↑(arrowCongr (trans e₁ e₂) (trans e₁' e₂')) x✝¹) x✝ = ↑(↑((arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂')) x✝¹) x✝
R : Type u
A₁ : Type v
A₂ : Type w
A₃ : Type u₁
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Algebra R A₁
inst✝⁷ : Algebra R A₂
inst✝⁶ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
A₁' : Type u_1
A₂' : Type u_2
A₃' : Type u_3
inst✝⁵ : Semiring A₁'
inst✝⁴ : Semiring A₂'
inst✝³ : Semiring A₃'
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e₁ : A₁ ≃ₐ[R] A₂
e₁' : A₁' ≃ₐ[R] A₂'
e₂ : A₂ ≃ₐ[R] A₃
e₂' : A₂' ≃ₐ[R] A₃'
⊢ arrowCongr (trans e₁ e₂) (trans e₁' e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂')
ext
no goals
case H.H
R : Type u
A₁ : Type v
A₂ : Type w
A₃ : Type u₁
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Algebra R A₁
inst✝⁷ : Algebra R A₂
inst✝⁶ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
A₁' : Type u_1
A₂' : Type u_2
A₃' : Type u_3
inst✝⁵ : Semiring A₁'
inst✝⁴ : Semiring A₂'
inst✝³ : Semiring A₃'
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e₁ : A₁ ≃ₐ[R] A₂
e₁' : A₁' ≃ₐ[R] A₂'
e₂ : A₂ ≃ₐ[R] A₃
e₂' : A₂' ≃ₐ[R] A₃'
x✝¹ : A₁ →ₐ[R] A₁'
x✝ : A₃
⊢ ↑(↑(arrowCongr (trans e₁ e₂) (trans e₁' e₂')) x✝¹) x✝ = ↑(↑((arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂')) x✝¹) x✝
rfl