-- 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
⊢ 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 : ∀ (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) 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.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 :
      β)
Tactic: ext