-- Module: Mathlib.Data.Finmap
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
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)
                        ⋯ :
                      { 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))).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
⊢ 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)

Tactic:
ext