case H.mk
α₁ : Type u_3
β₁ : Type u_2
β₂ : Type u_1
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ↑((prodCongrRight e).trans (prodComm α₁ β₂)) (a, b) = ↑((prodComm α₁ β₁).trans (prodCongrLeft e)) (a, b)
α₁ : Type u_3
β₁ : Type u_2
β₂ : Type u_1
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrRight e).trans (prodComm α₁ β₂) = (prodComm α₁ β₁).trans (prodCongrLeft e)
ext ⟨a, b⟩ : 1
no goals
case H.mk
α₁ : Type u_3
β₁ : Type u_2
β₂ : Type u_1
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ↑((prodCongrRight e).trans (prodComm α₁ β₂)) (a, b) = ↑((prodComm α₁ β₁).trans (prodCongrLeft e)) (a, b)
simp