Theorem: Setoid.IsPartition.card_eq_sum_parts (Jordan/Mathlib/Partitions.lean)

State before:
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Fintype.card α = ∑ t in Set.toFinset P, (Set.toFinset t).card
Tactic:
rw [← Finset.card_univ]
State after:
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Finset.univ.card = ∑ t in Set.toFinset P, (Set.toFinset t).card

State before:
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Finset.univ.card = ∑ t in Set.toFinset P, (Set.toFinset t).card
Tactic:
convert Setoid.IsPartition.card_set_eq_sum_parts Set.univ hP
State after:
case h.e'_2.h.e'_2
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Finset.univ = Set.toFinset Set.univ

case h.e'_3.a.h.e'_2.h
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
x✝ : Set α
a✝ : x✝ ∈ Set.toFinset P
⊢ x✝ = Set.univ ∩ x✝

State before:
case h.e'_2.h.e'_2
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Finset.univ = Set.toFinset Set.univ
Tactic:
rw [Set.toFinset_univ.symm]
State after:
case h.e'_2.h.e'_2
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Set.toFinset Set.univ = Set.toFinset Set.univ

State before:
case h.e'_2.h.e'_2
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Set.toFinset Set.univ = Set.toFinset Set.univ
Tactic:
congr
State after:
case h.e'_2.h.e'_2.h.e_3.h
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Set.fintypeUniv = Subtype.fintype fun x => x ∈ Set.univ

State before:
case h.e'_2.h.e'_2.h.e_3.h
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Set.fintypeUniv = Subtype.fintype fun x => x ∈ Set.univ
Tactic:
simp only [eq_iff_true_of_subsingleton]
State after:
no goals

State before:
case h.e'_3.a.h.e'_2.h
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
x✝ : Set α
a✝ : x✝ ∈ Set.toFinset P
⊢ x✝ = Set.univ ∩ x✝
Tactic:
rw [Set.univ_inter]
State after:
no goals