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