case 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₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑(↑(arrowCongr e₁ e₃) (AlgHom.comp g f)) x✝ = ↑(AlgHom.comp (↑(arrowCongr e₂ e₃) g) (↑(arrowCongr e₁ e₂) f)) 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₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
⊢ ↑(arrowCongr e₁ e₃) (AlgHom.comp g f) = AlgHom.comp (↑(arrowCongr e₂ e₃) g) (↑(arrowCongr e₁ e₂) f)
ext
case 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₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑↑e₃ (↑g (↑f (↑↑(symm e₁) x✝))) = ↑↑e₃ (↑g (↑↑(symm e₂) (↑↑e₂ (↑f (↑↑(symm e₁) x✝)))))
case 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₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑(↑(arrowCongr e₁ e₃) (AlgHom.comp g f)) x✝ = ↑(AlgHom.comp (↑(arrowCongr e₂ e₃) g) (↑(arrowCongr e₁ e₂) f)) x✝
simp only [arrowCongr, Equiv.coe_fn_mk, AlgHom.comp_apply]
case H.h.e_6.h.h.e_6.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₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑f (↑↑(symm e₁) x✝) = ↑↑(symm e₂) (↑↑e₂ (↑f (↑↑(symm e₁) x✝)))
case 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₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑↑e₃ (↑g (↑f (↑↑(symm e₁) x✝))) = ↑↑e₃ (↑g (↑↑(symm e₂) (↑↑e₂ (↑f (↑↑(symm e₁) x✝)))))
congr
no goals
case H.h.e_6.h.h.e_6.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₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
x✝ : A₁'
⊢ ↑f (↑↑(symm e₁) x✝) = ↑↑(symm e₂) (↑↑e₂ (↑f (↑↑(symm e₁) x✝)))
exact (e₂.symm_apply_apply _).symm