-- 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
a :
  ∀ (x : α),
    Eq.{u_2 + 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.fst (β := 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)) :
            (a : α) → β)
          x :
        β)
a₁ :
  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))) :
      β)
⊢ Eq (α := (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))
    ((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))))
    (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:
ext