-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
a :
  ∀ (a : Option α),
    Eq.{u_2 + 1} (α := β)
      (((↑((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 }))
                  ((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 }))
                    e)) :
              Option α ≃ β) :
            (a : Option α) → β)
          a :
        β)
      (((↑e : Option α ≃ β) : (a : Option α) → β) a : β)
⊢ (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 }))
      ((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 }))
        e) =
    e

Tactic:
ext a