-- Lean 4 proof step from Mathlib.Logic.Embedding.Set (goal)
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 :
        β)
⊢ 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))
have 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) sorry) :
                (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))) :
                    β)
                  sorry)
              (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) sorry) :
                            (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))) :
                                β)
                              sorry)
                          (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: ext