-- Module: Mathlib.Logic.Equiv.Option
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 }
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)) ⋯,
                        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) :
                Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }) :
              (a : α) → { y : β // y ≠ x })
            a) :
        β)
      (↑((e : (a : α) → { y : β // y ≠ x }) a) : β)
⊢ (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

Tactic:
ext a