-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
a :
  ∀ (a : α),
    Membership.mem (γ := Finset α)
        (↑((fun (s : Finmap β) ↦
                  (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                      ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s.keys (β := β), fun (i : α) ↦ lookup (β := β) i s)
                      ⋯ :
                    { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }))
                ((fun (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) ↦
                    mk (β := β)
                      (Finset.val
                        ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                          ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
                      ⋯)
                  (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                    ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s, f) hf))) :
            Finset α × ((a : α) → Option (β a))).1
        a ↔
      a ∈
        (↑(Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1)
                (s, f) hf) :
            Finset α × ((a : α) → Option (β a))).1
⊢ Eq (α := { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 })
    ((fun (s : Finmap β) ↦
        (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1)
            (s.keys (β := β), fun (i : α) ↦ lookup (β := β) i s) ⋯ :
          { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }))
      ((fun (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) ↦
          mk (β := β)
            (Finset.val
              ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
            ⋯)
        (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1)
          (s, f) hf)))
    (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s, f)
      hf)
have a₁ : ∀ (x : α) (a : β x),
  (↑((fun (s : Finmap β) ↦
                  (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                      ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s.keys (β := β), fun (i : α) ↦ lookup (β := β) i s)
                      sorry :
                    { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }))
                ((fun (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) ↦
                    mk (β := β)
                      (Finset.val
                        ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                          ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
                      sorry)
                  (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                    ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s, f) hf))) :
            Finset α × ((a : α) → Option (β a))).2
        x =
      some a ↔
    (↑(Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1)
                (s, f) hf) :
            Finset α × ((a : α) → Option (β a))).2
        x =
      some a
Tactic: ext