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
inst✝³ : Semiring A₁'
inst✝² : Semiring A₂'
inst✝¹ : Algebra R A₁'
inst✝ : Algebra R A₂'
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
x✝¹ : A₁' →ₐ[R] A₂'
x✝ : A₁
⊢ ↑(↑(arrowCongr e₁ e₂).symm x✝¹) x✝ = ↑(↑(arrowCongr (symm e₁) (symm 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
inst✝³ : Semiring A₁'
inst✝² : Semiring A₂'
inst✝¹ : Algebra R A₁'
inst✝ : Algebra R A₂'
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
⊢ (arrowCongr e₁ e₂).symm = arrowCongr (symm e₁) (symm 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
inst✝³ : Semiring A₁'
inst✝² : Semiring A₂'
inst✝¹ : Algebra R A₁'
inst✝ : Algebra R A₂'
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
x✝¹ : A₁' →ₐ[R] A₂'
x✝ : A₁
⊢ ↑(↑(arrowCongr e₁ e₂).symm x✝¹) x✝ = ↑(↑(arrowCongr (symm e₁) (symm e₂)) x✝¹) x✝
rfl