S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e✝.symm α)
e :
  { fst := ↑e✝ (Set ((α : S) × ↑e✝.symm α)),
      snd := cast (_ : Set ((α : S) × ↑e✝.symm α) = ↑e✝.symm (↑e✝ (Set ((α : S) × ↑e✝.symm α)))) a } =
    { fst := ↑e✝ (Set ((α : S) × ↑e✝.symm α)),
      snd := cast (_ : Set ((α : S) × ↑e✝.symm α) = ↑e✝.symm (↑e✝ (Set ((α : S) × ↑e✝.symm α)))) b }
⊢ a = b
S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e✝.symm α)
e :
  (fun a =>
        { fst := Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)),
          snd :=
            cast (_ : Set ((α : S) × ↑e✝.symm α) = Equiv.invFun e✝ (Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)))) a })
      a =
    (fun a =>
        { fst := Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)),
          snd :=
            cast (_ : Set ((α : S) × ↑e✝.symm α) = Equiv.invFun e✝ (Equiv.toFun e✝ (Set ((α : S) × ↑e✝.symm α)))) a })
      b
⊢ a = b
dsimp at e
S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e.symm α)
h₁ : ↑e (Set ((α : S) × ↑e.symm α)) = ↑e (Set ((α : S) × ↑e.symm α))
h₂ :
  cast (_ : Set ((α : S) × ↑e.symm α) = ↑e.symm (↑e (Set ((α : S) × ↑e.symm α)))) a =
    cast (_ : Set ((α : S) × ↑e.symm α) = ↑e.symm (↑e (Set ((α : S) × ↑e.symm α)))) b
⊢ a = b
S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e✝.symm α)
e :
  { fst := ↑e✝ (Set ((α : S) × ↑e✝.symm α)),
      snd := cast (_ : Set ((α : S) × ↑e✝.symm α) = ↑e✝.symm (↑e✝ (Set ((α : S) × ↑e✝.symm α)))) a } =
    { fst := ↑e✝ (Set ((α : S) × ↑e✝.symm α)),
      snd := cast (_ : Set ((α : S) × ↑e✝.symm α) = ↑e✝.symm (↑e✝ (Set ((α : S) × ↑e✝.symm α)))) b }
⊢ a = b
injection e with h₁ h₂
no goals
S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × ↑e.symm α)
h₁ : ↑e (Set ((α : S) × ↑e.symm α)) = ↑e (Set ((α : S) × ↑e.symm α))
h₂ :
  cast (_ : Set ((α : S) × ↑e.symm α) = ↑e.symm (↑e (Set ((α : S) × ↑e.symm α)))) a =
    cast (_ : Set ((α : S) × ↑e.symm α) = ↑e.symm (↑e (Set ((α : S) × ↑e.symm α)))) b
⊢ a = b
simpa using h₂