-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
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 : β)
⊢ 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 : β)
have 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 := sorry, right_inv := sorry }
                      sorry :
                    { 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)) 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 }))
                  e)) :
            Option α ≃ β) :
          (a : Option α) → β)
        (some val) :
      β)
    (((↑e : Option α ≃ β) : (a : Option α) → β) (some val) : β)
Tactic: cases a
Cleared hypotheses: a