Theorem: Partition.card_of_partition (Jordan/Mathlib/Partitions.lean)

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
hc : Setoid.IsPartition c
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = Fintype.card α
Tactic:
let c' : Finset (Finset α) := {s : Finset α | (s : Set α) ∈ c}.toFinset
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
hc : Setoid.IsPartition c
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = Fintype.card α

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
hc : Setoid.IsPartition c
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = Fintype.card α
Tactic:
have hcc' : c = {s : Set α | ∃ t : Finset α, s.toFinset = t ∧ t ∈ c'} := by
  simp only [c', Set.toFinset_setOf, Finset.mem_univ, forall_true_left,
    Finset.mem_filter, true_and, exists_eq_left', Set.coe_toFinset, Set.setOf_mem_eq]
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
hc : Setoid.IsPartition c
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = Fintype.card α

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
hc : Setoid.IsPartition c
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = Fintype.card α
Tactic:
rw [hcc'] at hc
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = Fintype.card α

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = Fintype.card α
Tactic:
rw [← Partition.card_of_partition' hc]
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = ∑ s in c', s.card

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = ∑ s in c', s.card
Tactic:
have hi : ∀ a ∈ c.toFinset, a.toFinset ∈ c' := by
  intro a ha
  simp only [c', Set.toFinset_setOf, Finset.mem_univ, forall_true_left,
    Finset.mem_filter, Set.coe_toFinset, true_and]
  simp only [Set.mem_toFinset] at ha
  exact ha
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = ∑ s in c', s.card

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = ∑ s in c', s.card
Tactic:
have hj : ∀ a ∈ c', (a : Set α) ∈ c.toFinset := by
  intro a ha
  simp only [c', Set.toFinset_setOf, Finset.mem_univ, forall_true_left,
    Finset.mem_filter, true_and] at ha
  simp only [Set.mem_toFinset]
  exact ha
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = ∑ s in c', s.card

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
⊢ ∑ s in Set.toFinset c, (Set.toFinset s).card = ∑ s in c', s.card
Tactic:
rw [Finset.sum_bij' _ _ hi hj _ _]
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
⊢ ∀ a ∈ Set.toFinset c, (Set.toFinset a).card = (Set.toFinset a).card

α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
⊢ ∀ a ∈ Set.toFinset c, ↑(Set.toFinset a) = a

α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
⊢ ∀ a ∈ c', Set.toFinset ↑a = a

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
⊢ ∀ a ∈ Set.toFinset c, (Set.toFinset a).card = (Set.toFinset a).card

α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
⊢ ∀ a ∈ Set.toFinset c, ↑(Set.toFinset a) = a

α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
⊢ ∀ a ∈ c', Set.toFinset ↑a = a
Tactic:
all_goals { intros; simp only [Set.coe_toFinset, Finset.toFinset_coe] }
State after:
no goals

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
hc : Setoid.IsPartition c
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
⊢ c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
Tactic:
simp only [c', Set.toFinset_setOf, Finset.mem_univ, forall_true_left,
  Finset.mem_filter, true_and, exists_eq_left', Set.coe_toFinset, Set.setOf_mem_eq]
State after:
no goals

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
⊢ ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
Tactic:
intro a ha
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
a : Set α
ha : a ∈ Set.toFinset c
⊢ Set.toFinset a ∈ c'

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
a : Set α
ha : a ∈ Set.toFinset c
⊢ Set.toFinset a ∈ c'
Tactic:
simp only [c', Set.toFinset_setOf, Finset.mem_univ, forall_true_left,
  Finset.mem_filter, Set.coe_toFinset, true_and]
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
a : Set α
ha : a ∈ Set.toFinset c
⊢ a ∈ c

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
a : Set α
ha : a ∈ Set.toFinset c
⊢ a ∈ c
Tactic:
simp only [Set.mem_toFinset] at ha
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
a : Set α
ha : a ∈ c
⊢ a ∈ c

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
a : Set α
ha : a ∈ c
⊢ a ∈ c
Tactic:
exact ha
State after:
no goals

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
⊢ ∀ a ∈ c', ↑a ∈ Set.toFinset c
Tactic:
intro a ha
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
a : Finset α
ha : a ∈ c'
⊢ ↑a ∈ Set.toFinset c

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
a : Finset α
ha : a ∈ c'
⊢ ↑a ∈ Set.toFinset c
Tactic:
simp only [c', Set.toFinset_setOf, Finset.mem_univ, forall_true_left,
  Finset.mem_filter, true_and] at ha
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
a : Finset α
ha : ↑a ∈ c
⊢ ↑a ∈ Set.toFinset c

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
a : Finset α
ha : ↑a ∈ c
⊢ ↑a ∈ Set.toFinset c
Tactic:
simp only [Set.mem_toFinset]
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
a : Finset α
ha : ↑a ∈ c
⊢ ↑a ∈ c

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
a : Finset α
ha : ↑a ∈ c
⊢ ↑a ∈ c
Tactic:
exact ha
State after:
no goals

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
⊢ ∀ a ∈ c', Set.toFinset ↑a = a
Tactic:
intros
State after:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
a✝ : Finset α
ha✝ : a✝ ∈ c'
⊢ Set.toFinset ↑a✝ = a✝

State before:
α : Type u_1
inst✝ : Fintype α
c : Set (Set α)
c' : Finset (Finset α) := Set.toFinset {s | ↑s ∈ c}
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hcc' : c = {s | ∃ t, Set.toFinset s = t ∧ t ∈ c'}
hi : ∀ a ∈ Set.toFinset c, Set.toFinset a ∈ c'
hj : ∀ a ∈ c', ↑a ∈ Set.toFinset c
a✝ : Finset α
ha✝ : a✝ ∈ c'
⊢ Set.toFinset ↑a✝ = a✝
Tactic:
simp only [Set.coe_toFinset, Finset.toFinset_coe]
State after:
no goals