-- 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 : Option α
a₁ :
  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 α) → β)
        none :
      β)
    (((↑e : Option α ≃ β) : (a : Option α) → β) none : β)
a₂ :
  ∀ (val : α),
    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 α) → β)
          (some val) :
        β)
      (((↑e : Option α ≃ β) : (a : Option α) → β) (some val) : β)
⊢ 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 : β)

Tactic:
cases a