-- Module: Mathlib.Order.Partition.Finpartition
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 α)
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 : α)) ⋯)
                    (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)) :
          ↥(↑(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 α)) :
      α) =
    (↑(x.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 : α)) ⋯)
            (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

Tactic:
ext e