-- 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
f : ↑(Function.support fun t => (s ∩ ↑t).ncard) → ↑s :=
  fun x =>
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
⊢ (Function.support fun t => (s ∩ ↑t).ncard).Finite

Tactic:
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⟩

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
f : ↑(Function.support fun t => (s ∩ ↑t).ncard) → ↑s :=
  fun x =>
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
hf : ∀ (t : ↑(Function.support fun t => (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
⊢ (Function.support fun t => (s ∩ ↑t).ncard).Finite

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 : α
⊢ ∀ x_1 ∈ s, x_1 ∈ ↑t → Finite ↑(s ∩ ↑t) → x ∈ s → x ∈ ↑t → ⟨⋯.choose, ⋯⟩ = t

Tactic:
intro y hy hyt _ hxs hxt

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

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
f : ↑(Function.support fun t => (s ∩ ↑t).ncard) → ↑s :=
  fun x =>
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
hf : ∀ (t : ↑(Function.support fun t => (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
this : Finite ↑s
t t' : ↑(Function.support fun t => (s ∩ ↑t).ncard)
h : f t = f t'
⊢ ↑↑t = ↑↑t'

Tactic:
exact (hP.2 (f t)).unique (hf t) (h ▸ hf 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
f : ↑(Function.support fun t => (s ∩ ↑t).ncard) → ↑s :=
  fun x =>
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
hf : ∀ (t : ↑(Function.support fun t => (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
⊢ (Function.support fun t => (s ∩ ↑t).ncard).Finite

Tactic:
have : Finite ↑s := 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
f : ↑(Function.support fun t => (s ∩ ↑t).ncard) → ↑s :=
  fun x =>
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
hf : ∀ (t : ↑(Function.support fun t => (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
this : Finite ↑s
⊢ (Function.support fun t => (s ∩ ↑t).ncard).Finite

Proof state:
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

Tactic:
rintro ⟨t, x⟩

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, x⟩ ∈ ⋯.toFinset.sigma fun t => ⋯.toFinset) →
    (match ⟨t, x⟩ with
      | ⟨t, x⟩ => x) ∈
      Set.Finite.toFinset hs

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
f : ↑(Function.support fun t => (s ∩ ↑t).ncard) → ↑s :=
  fun x =>
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
hf : ∀ (t : ↑(Function.support fun t => (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
this : Finite ↑s
⊢ Function.Injective f

Tactic:
intro t t' h

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
f : ↑(Function.support fun t => (s ∩ ↑t).ncard) → ↑s :=
  fun x =>
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
hf : ∀ (t : ↑(Function.support fun t => (s ∩ ↑t).ncard)), ↑↑t ∈ P ∧ ↑(f t) ∈ ↑↑t
this : Finite ↑s
t t' : ↑(Function.support fun t => (s ∩ ↑t).ncard)
h : f t = f t'
⊢ t = t'

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
⊢ (Set.Finite.toFinset hs).card = ∑ t ∈ ⋯.toFinset, Nat.card ↑(s ∩ ↑t)

Tactic:
rw [Finset.sum_congr rfl (fun t ht ↦ by exact hst' ↑t)]

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, ⋯.toFinset.card

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
⊢ ∃ a ∈ s, a ∈ ⋯.choose

Tactic:
use x, hx, (hP.2 x).exists.choose_spec.2

Result:
no goals

Proof state:
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

Tactic:
rintro ⟨t, x⟩

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 : α
⊢ (⟨t, x⟩ ∈ ⋯.toFinset.sigma fun t => ⋯.toFinset) →
    ⟨⟨⋯.choose, ⋯⟩,
        match ⟨t, x⟩ with
        | ⟨t, x⟩ => x⟩ =
      ⟨t, x⟩

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 : α
⊢ x ∈ Set.Finite.toFinset hs → ⟨⟨⋯.choose, ⋯⟩, x⟩ ∈ ⋯.toFinset.sigma fun t => ⋯.toFinset

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

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 ∈ s → Nat.card ↑(s ∩ ⋯.choose) ≠ 0 ∧ x ∈ s ∧ x ∈ ⋯.choose