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

Tactic:
simp only [nonempty_subtype, Set.mem_inter_iff, forall_exists_index, and_imp]

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 : α
⊢ ∀ x_1 ∈ s, x_1 ∈ ↑t → Finite ↑(s ∩ ↑t) → x ∈ s → 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
⊢ (Function.support fun t => (s ∩ ↑t).ncard).Finite

Tactic:
apply Finite.of_injective f

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.Injective f

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

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

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

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

Tactic:
intro hx

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

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:
exact (hP.2 x).unique (hP.2 x).exists.choose_spec ⟨t.prop, hxt⟩

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
this : Finite ↑s
t t' : ↑(Function.support fun t => (s ∩ ↑t).ncard)
h : f t = f t'
⊢ t = t'

Tactic:
simp only [← Subtype.coe_inj, Subtype.coe_mk]

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
⊢ s.ncard = ∑ᶠ (t : ↑P), (s ∩ ↑t).ncard

Tactic:
have hst' (t : Set α) : Nat.card ↑(s ∩ t) = (hst t).toFinset.card :=
  Nat.card_eq_card_finite_toFinset (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
⊢ s.ncard = ∑ᶠ (t : ↑P), (s ∩ ↑t).ncard

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
⊢ Nonempty ↑(s ∩ ⋯.choose)

Tactic:
simp only [nonempty_subtype, 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 : α
hx : x ∈ s
⊢ ∃ a ∈ s, a ∈ ⋯.choose

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
⊢ ∀ a ∈ Set.Finite.toFinset hs,
    (match ⟨⟨⋯.choose, ⋯⟩, a⟩ with
      | ⟨t, x⟩ => x) =
      a

Tactic:
intro t

Result:
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

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

Tactic:
rw [← Finset.card_sigma, eq_comm]

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
⊢ (⋯.toFinset.sigma fun t => ⋯.toFinset).card = (Set.Finite.toFinset hs).card