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