-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : (t : ↥P.parts) × ↥(↑t : Finset α)
a₁ :
  ∀ (e : α),
    Membership.mem (γ := Finset α)
        (↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
              ((fun (x : ↥s) ↦
                  (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                      (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯)
                      (Subtype.mk (p := fun (x_1 : α) ↦
                        x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯) : Finset α))
                        (↑x : α) ⋯) :
                    (t : ↥P.parts) × ↥(↑t : Finset α)))
                ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                    Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) ⋯)
                  x))) :
          Finset α)
        e ↔
      e ∈ (↑(x.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))) : Finset α)
⊢ (fun (x : ↥s) ↦
        (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
            (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯)
            (Subtype.mk (p := fun (x_1 : α) ↦
              x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯) : Finset α)) (↑x : α)
              ⋯) :
          (t : ↥P.parts) × ↥(↑t : Finset α)))
      ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
          Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) ⋯)
        x) =
    x
have a₂ : (↑(Sigma.snd (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
          ((fun (x : ↥s) ↦
              (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                  (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) sorry)
                  (Subtype.mk (p := fun (x_1 : α) ↦
                    x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) sorry) : Finset α))
                    (↑x : α) sorry) :
                (t : ↥P.parts) × ↥(↑t : Finset α)))
            ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) sorry)
              x)) :
        ↥(↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
                ((fun (x : ↥s) ↦
                    (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                        (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) sorry)
                        (Subtype.mk (p := fun (x_1 : α) ↦
                          x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) sorry) : Finset α))
                          (↑x : α) sorry) :
                      (t : ↥P.parts) × ↥(↑t : Finset α)))
                  ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                      Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α)
                        sorry)
                    x))) :
            Finset α)) :
    α) =
  (↑(x.snd (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))) : α)
Tactic: ext e