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