-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
have have₁ have₂ : ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite), s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
have₃ :
  ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite)
    (hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card),
    s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
have₄ :
  ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite)
    (hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card),
    Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
have₅ :
  ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite)
    (hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card),
    Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
have₆ :
  ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite)
    (hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card),
    let f :
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) →
        (↑s : Type u_1) :=
      fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
      match (motive :=
        (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) →
          (↑s : Type u_1))
        x with
      | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯;
    ∀
      (hf :
        ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
          (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α)),
      Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
have₇ :
  ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite)
    (hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card),
    let f :
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) →
        (↑s : Type u_1) :=
      fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
      match (motive :=
        (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) →
          (↑s : Type u_1))
        x with
      | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯;
    ∀
      (hf :
        ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
          (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α))
      (this : Finite.{u_1 + 1} (↑s : Type u_1)),
      Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
have₈ :
  ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite)
    (hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card),
    let f :
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) →
        (↑s : Type u_1) :=
      fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
      match (motive :=
        (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) →
          (↑s : Type u_1))
        x with
      | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯;
    ∀
      (hf :
        ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
          (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α))
      (this : Finite.{u_1 + 1} (↑s : Type u_1)), Function.Injective f
have₉ :
  ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite)
    (hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card),
    let f :
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) →
        (↑s : Type u_1) :=
      fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
      match (motive :=
        (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) →
          (↑s : Type u_1))
        x with
      | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯;
    ∀
      (hf :
        ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
          (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α))
      (this : Finite.{u_1 + 1} (↑s : Type u_1))
      ⦃t t' : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)⦄
      (h : f t = f t'), t = t'
have₁₀ :
  ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite)
    (hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card),
    let f :
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) →
        (↑s : Type u_1) :=
      fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
      match (motive :=
        (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) →
          (↑s : Type u_1))
        x with
      | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯;
    ∀
      (hf :
        ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
          (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α))
      (this : Finite.{u_1 + 1} (↑s : Type u_1))
      ⦃t t' : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)⦄
      (h : f t = f t'), (↑(↑t : (↑P : Type u_1)) : Set α) = (↑(↑t' : (↑P : Type u_1)) : Set α)
⊢ s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard

Tactic:
classical
  have hst (t : Set α) : (s ∩ t).Finite := hs.inter_of_left t
  have hst' (t : Set α) : Nat.card ↑(s ∩ t) = (hst t).toFinset.card :=
    Nat.card_eq_card_finite_toFinset (hst t)
  suffices hs' : _ by
    rw [finsum_def, dif_pos hs']
    simp only [← Nat.card_coe_set_eq, Nat.card_eq_card_finite_toFinset hs]
    rw [Finset.sum_congr rfl (fun t ht ↦ by exact hst' ↑t)]
    rw [← Finset.card_sigma, eq_comm]
    apply Finset.card_nbij' (fun ⟨t, x⟩ ↦ x)
      (fun x ↦ ⟨⟨(hP.2 x).exists.choose, (hP.2 x).exists.choose_spec.1⟩, x⟩)
    · rintro ⟨t, x⟩
      simp +contextual
    · intro x
      simp only [Set.Finite.mem_toFinset, Finset.mem_sigma, Function.mem_support, Set.mem_inter_iff,
        Finset.mem_coe]
      intro hx
      refine ⟨Nat.card_ne_zero.mpr ⟨?_, hst (hP.right x).exists.choose⟩,
        hx, (hP.2 x).exists.choose_spec.2⟩
      simp only [nonempty_subtype, Set.mem_inter_iff]
      use x, hx, (hP.2 x).exists.choose_spec.2
    · rintro ⟨t, x⟩
      simp only [Finset.mem_sigma, Set.Finite.mem_toFinset, Function.mem_support, Nat.card_ne_zero,
        Set.mem_inter_iff, Sigma.mk.inj_iff, heq_eq_eq, and_true, and_imp, Finset.mem_coe]
      simp only [nonempty_subtype, Set.mem_inter_iff, forall_exists_index, and_imp]
      intro y hy hyt _ hxs hxt
      rw [← Subtype.coe_inj]
      exact (hP.2 x).unique (hP.2 x).exists.choose_spec ⟨t.prop, hxt⟩
    · intro t
      simp only [implies_true]
  let f : Function.support (fun (t : P) ↦ (s ∩ (t : Set α)).ncard) → s := fun ⟨t, ht⟩ ↦
    ⟨(Set.nonempty_of_ncard_ne_zero ht).choose, (Set.nonempty_of_ncard_ne_zero ht).choose_spec.1⟩
  have hf (t : Function.support (fun (t : P) ↦ (s ∩ (t : Set α)).ncard)) :
      ↑↑t ∈ P ∧ (f t : α) ∈ (t : Set α) :=
    ⟨(↑t : P).prop, (Set.nonempty_of_ncard_ne_zero t.prop).choose_spec.2⟩
  have : Finite ↑s := hs
  apply Finite.of_injective f
  intro t t' h
  simp only [← Subtype.coe_inj]
  exact (hP.2 (f t)).unique (hf t) (h ▸ hf t')

Premises used: Subtype.coe_inj