-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
w : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
h h₁ :
  Eq (α := { t : Set α // #(↑t : Type u) ≤ #β })
    ((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
        (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
          { t : Set α // #(↑t : Type u) ≤ #β }))
      fun (y : β) ↦
      if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
        Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
      else Sum.inr { down := 0 })
    (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯)
h₂ h₃ :
  (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
            (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
              { t : Set α // #(↑t : Type u) ≤ #β }))
          fun (y : β) ↦
          if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
            Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
          else Sum.inr { down := 0 }) :
      Set α) =
    (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
h₄ :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
                (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
                  { t : Set α // #(↑t : Type u) ≤ #β }))
              fun (y : β) ↦
              if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
                Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
              else Sum.inr { down := 0 }) :
          Set α)
        x ↔
      x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
h₅ :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
                (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
                  { t : Set α // #(↑t : Type u) ≤ #β }))
              fun (y : β) ↦
              if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
                Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
              else Sum.inr { down := 0 }) :
          Set α)
        x →
      x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
h₆ h₇ :
  ∀ x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α),
    Membership.mem (γ := Set α)
      (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
              (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
                { t : Set α // #(↑t : Type u) ≤ #β }))
            fun (y : β) ↦
            if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
              Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
            else Sum.inr { down := 0 }) :
        Set α)
      x
⊢ ∃ (a : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β),
    Eq (α := { t : Set α // #(↑t : Type u) ≤ #β })
      ((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
          (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
            { t : Set α // #(↑t : Type u) ≤ #β }))
        a)
      (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯)

Tactic:
classical
  use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
               else Sum.inr (ULift.up 0)
  apply Subtype.ext; ext x
  constructor
  · rintro ⟨y, h⟩
    dsimp only at h
    by_cases h' : ∃ z : s, g z = y
    · rw [dif_pos h'] at h
      cases Sum.inl.inj h
      exact (Classical.choose h').2
    · rw [dif_neg h'] at h
      cases h
  · intro h
    have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩
    use g ⟨x, h⟩
    dsimp only
    rw [dif_pos this]
    congr
    suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this
    apply g.2
    exact Classical.choose_spec this

Premises used: Function.Embedding.inj', Subtype.ext