-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
β : Type u_2
x : (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)
f : α ↪ β
y : β
hy : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ y
⊢ Eq.{u_2 + 1} (α := β)
    (↑(Sigma.snd (β := fun (a : α ↪ β) ↦
            { x : β // Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑a : (a : α) → β))ᶜ x })
            ((fun (f : Embedding.{u_1 + 1, u_2 + 1} (Option α) β) ↦
                (Sigma.mk (β := fun (f : α ↪ β) ↦ (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))
                    (Embedding.trans Embedding.some f)
                    (Subtype.mk (p := fun (x : β) ↦
                      Membership.mem (γ := Set β)
                        (range.{u_2, u_1 + 1} (ι := α) (⇑(Embedding.trans Embedding.some f) : (a : α) → β))ᶜ x)
                      ((f : (a : Option α) → β) none) ⋯) :
                  (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)))
              ((fun (f : (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)) ↦
                  f.fst (β := fun (f : α ↪ β) ↦
                        (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)).optionElim
                    (↑(f.snd (β := fun (f : α ↪ β) ↦
                          (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))) :
                      β)
                    ⋯)
                (Sigma.mk (β := fun (f : α ↪ β) ↦ (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)) f
                  (Subtype.mk (p := fun (x : β) ↦
                    Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ x) y hy)))) :
          { x : β //
            Membership.mem (γ := Set β)
              (range.{u_2, u_1 + 1} (ι := α)
                  (⇑(Sigma.fst (β := fun (a : α ↪ β) ↦
                        { x : β // Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑a : (a : α) → β))ᶜ x })
                        ((fun (f : Embedding.{u_1 + 1, u_2 + 1} (Option α) β) ↦
                            (Sigma.mk (β := fun (f : α ↪ β) ↦
                                (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))
                                (Embedding.trans Embedding.some f)
                                (Subtype.mk (p := fun (x : β) ↦
                                  Membership.mem (γ := Set β)
                                    (range.{u_2, u_1 + 1} (ι := α) (⇑(Embedding.trans Embedding.some f) : (a : α) → β))ᶜ
                                    x)
                                  ((f : (a : Option α) → β) none) ⋯) :
                              (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)))
                          ((fun (f : (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)) ↦
                              f.fst (β := fun (f : α ↪ β) ↦
                                    (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)).optionElim
                                (↑(f.snd (β := fun (f : α ↪ β) ↦
                                      (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))) :
                                  β)
                                ⋯)
                            (Sigma.mk (β := fun (f : α ↪ β) ↦
                              (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)) f
                              (Subtype.mk (p := fun (x : β) ↦
                                Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ x) y
                                hy))))) :
                    (a : α) → β))ᶜ
              x }) :
      β)
    (↑(Sigma.snd (β := fun (a : α ↪ β) ↦
          { x : β // Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑a : (a : α) → β))ᶜ x })
          (Sigma.mk (β := fun (f : α ↪ β) ↦ (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)) f
            (Subtype.mk (p := fun (x : β) ↦
              Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ x) y hy))) :
      β)

Tactic:
simp