a fact about cardinalities of preimages

Stream: Is there code for X?

[Scott Morrison]

Could anyone help me either by identifying an existing proof of this fact, or helping me out of the dependent type theory hell I've landed myself in in the proof? :-)

import set_theory.cardinal.basic

open_locale cardinal

universes u₁ u₂ u₃

lemma exists_equiv_of_preimage_cardinal_eq
  {α : Type u₁} {β : Type u₂} {γ : Type u₃} (f : α → γ) (g : β → γ)
  (w : ∀ c, cardinal.lift.{u₂} (#(f ⁻¹' {c})) = cardinal.lift.{u₁} (#(g ⁻¹' {c}))) :
  ∃ e : α ≃ β, ∀ a, g (e a) = f a :=
begin
  let e' : Π c, (f ⁻¹' {c}) ≃ g ⁻¹' {c} := λ c, nonempty.some (cardinal.lift_mk_eq'.mp (w c)),
  have h : ∀ a, g (e' (f a) ⟨a, (by simp)⟩) = f a := λ a, (e' (f a) ⟨a, (by simp)⟩).2,
  refine ⟨⟨_, _, _, _⟩, _⟩,
  { intro a, exact (e' (f a) ⟨a, (by simp)⟩).1, },
  { intro b, exact ((e' (g b)).symm ⟨b, (by simp)⟩).1, },
  { intro a,
    have := (e' (f a)).symm_apply_apply ⟨a, (by simp)⟩,
    sorry, },
  { intro b,
    have := (e' (g b)).apply_symm_apply ⟨b, (by simp)⟩,
    sorry, },
  { simpa using h, },
end