-- Mathlib/Data/Setoid/Partition/Card.lean
theorem Setoid.IsPartition.ncard_eq_finsum {α : Type*} {P : Set (Set α)}
    (hP : Setoid.IsPartition P) (s : Set α) (hs : s.Finite

Proof state:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : ?m.379
⊢ s.ncard = ∑ᶠ (t : ↑P), (s ∩ ↑t).ncard

Tactic:
rw [finsum_def, dif_pos hs']

Result:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
⊢ s.ncard = ∑ i ∈ hs'.toFinset, (s ∩ ↑i).ncard

Proof state:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
⊢ (⋯.toFinset.sigma fun t => ⋯.toFinset).card = (Set.Finite.toFinset hs).card

Tactic:
apply Finset.card_nbij' (fun ⟨t, x⟩ ↦ x)
  (fun x ↦ ⟨⟨(hP.2 x).exists.choose, (hP.2 x).exists.choose_spec.1⟩, x⟩)

Result:
case hi
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
⊢ ∀ a ∈ ⋯.toFinset.sigma fun t => ⋯.toFinset,
    (match a with
      | ⟨t, x⟩ => x) ∈
      Set.Finite.toFinset hs

case hj
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
⊢ ∀ a ∈ Set.Finite.toFinset hs, ⟨⟨⋯.choose, ⋯⟩, a⟩ ∈ ⋯.toFinset.sigma fun t => ⋯.toFinset

case left_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
⊢ ∀ a ∈ ⋯.toFinset.sigma fun t => ⋯.toFinset,
    ⟨⟨⋯.choose, ⋯⟩,
        match a with
        | ⟨t, x⟩ => x⟩ =
      a

case right_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
⊢ ∀ a ∈ Set.Finite.toFinset hs,
    (match ⟨⟨⋯.choose, ⋯⟩, a⟩ with
      | ⟨t, x⟩ => x) =
      a

Proof state:
case hi.mk
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
t : ↑P
x : α
⊢ (t ∈ Function.support fun t => Nat.card ↑(s ∩ ↑t)) → x ∈ s → x ∈ ↑t → x ∈ s

Tactic:
exact fun _ a _ ↦ a

Result:
no goals

Proof state:
case hi.mk
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
t : ↑P
x : α
⊢ (⟨t, x⟩ ∈ ⋯.toFinset.sigma fun t => ⋯.toFinset) →
    (match ⟨t, x⟩ with
      | ⟨t, x⟩ => x) ∈
      Set.Finite.toFinset hs

Tactic:
simp only [Finset.mem_sigma, Set.Finite.mem_toFinset, Set.mem_inter_iff, and_imp]

Result:
case hi.mk
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
t : ↑P
x : α
⊢ (t ∈ Function.support fun t => Nat.card ↑(s ∩ ↑t)) → x ∈ s → x ∈ ↑t → x ∈ s

Proof state:
case hj
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
⊢ ∀ a ∈ Set.Finite.toFinset hs, ⟨⟨⋯.choose, ⋯⟩, a⟩ ∈ ⋯.toFinset.sigma fun t => ⋯.toFinset

Tactic:
intro x

Result:
case hj
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
x : α
⊢ x ∈ Set.Finite.toFinset hs → ⟨⟨⋯.choose, ⋯⟩, x⟩ ∈ ⋯.toFinset.sigma fun t => ⋯.toFinset

Proof state:
case hj
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
x : α
hx : x ∈ s
⊢ Nat.card ↑(s ∩ ⋯.choose) ≠ 0 ∧ x ∈ s ∧ x ∈ ⋯.choose

Tactic:
refine ⟨Nat.card_ne_zero.mpr ⟨?_, hst (hP.right x).exists.choose⟩,
  hx, (hP.2 x).exists.choose_spec.2⟩

Result:
case hj
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
x : α
hx : x ∈ s
⊢ Nonempty ↑(s ∩ ⋯.choose)

Proof state:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
t : ↑P
ht : t ∈ ⋯.toFinset
⊢ Nat.card ↑(s ∩ ↑t) = ?m.797 t

Tactic:
exact hst' ↑t

Result:
no goals

Proof state:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
⊢ s.ncard = ∑ i ∈ hs'.toFinset, (s ∩ ↑i).ncard

Tactic:
simp only [← Set.Nat.card_coe_set_eq, Nat.card_eq_card_finite_toFinset hs]

Result:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
⊢ (Set.Finite.toFinset hs).card = ∑ t ∈ ⋯.toFinset, Nat.card ↑(s ∩ ↑t)

Proof state:
case right_inv
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
t : α
⊢ t ∈ Set.Finite.toFinset hs →
    (match ⟨⟨⋯.choose, ⋯⟩, t⟩ with
      | ⟨t, x⟩ => x) =
      t

Tactic:
simp only [Set.Finite.mem_toFinset, implies_true]

Result:
no goals

Proof state:
case left_inv.mk
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
t : ↑P
x y : α
hy : y ∈ s
hyt : y ∈ ↑t
a✝ : Finite ↑(s ∩ ↑t)
hxs : x ∈ s
hxt : x ∈ ↑t
⊢ ⟨⋯.choose, ⋯⟩ = t

Tactic:
rw [← Subtype.coe_inj]

Result:
case left_inv.mk
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : (Function.support fun t => (s ∩ ↑t).ncard).Finite
t : ↑P
x y : α
hy : y ∈ s
hyt : y ∈ ↑t
a✝ : Finite ↑(s ∩ ↑t)
hxs : x ∈ s
hxt : x ∈ ↑t
⊢ ↑⟨⋯.choose, ⋯⟩ = ↑t