-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
⊢ (fun (e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }) ↦
        ({
            toFun := fun (a : α) ↦
              Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯,
            invFun := fun (b : { y : β // y ≠ x }) ↦
              Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }))
      ((fun (e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }) ↦
          (Subtype.mk (p := fun (e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β) ↦ (e : (a : Option α) → β) none = x)
              {
                toFun := fun (a : Option α) ↦
                  a.casesOn' x
                    (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
                      (⇑e : (a : α) → { y : β // y ≠ x })),
                invFun := fun (b : β) ↦
                  if h : b = x then none
                  else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)),
                left_inv := ⋯, right_inv := ⋯ }
              ⋯ :
            { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }))
        e) =
    e
have H : ∀ (a : α),
  Eq.{u_2 + 1} (α := β)
    (↑((((fun (e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }) ↦
                  ({
                      toFun := fun (a : α) ↦
                        Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) sorry,
                      invFun := fun (b : { y : β // y ≠ x }) ↦
                        Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) sorry,
                      left_inv := sorry, right_inv := sorry } :
                    Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }))
                ((fun (e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }) ↦
                    (Subtype.mk (p := fun (e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β) ↦
                        (e : (a : Option α) → β) none = x)
                        {
                          toFun := fun (a : Option α) ↦
                            a.casesOn' x
                              (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
                                (⇑e : (a : α) → { y : β // y ≠ x })),
                          invFun := fun (b : β) ↦
                            if h : b = x then none
                            else
                              some
                                ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)),
                          left_inv := sorry, right_inv := sorry }
                        sorry :
                      { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }))
                  e) :
              Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }) :
            (a : α) → { y : β // y ≠ x })
          a) :
      β)
    (↑((e : (a : α) → { y : β // y ≠ x }) a) : β)
Tactic: ext a