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

State before:
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
⊢ let P' := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅};
  s.card = ∑ t in Set.toFinset P', (Set.toFinset t).card
Tactic:
intro P'
State after:
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
⊢ s.card = ∑ t in Set.toFinset P', (Set.toFinset t).card

State before:
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
⊢ s.card = ∑ t in Set.toFinset P', (Set.toFinset t).card
Tactic:
have :=
  @Partition.card_of_partition _ (FinsetCoe.fintype s) _ (Setoid.isPartition_on hP (s : Set α))
State after:
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this :
  ∑ s_1 in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset s_1).card = Fintype.card ↑↑s
⊢ s.card = ∑ t in Set.toFinset P', (Set.toFinset t).card

State before:
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this :
  ∑ s_1 in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset s_1).card = Fintype.card ↑↑s
⊢ s.card = ∑ t in Set.toFinset P', (Set.toFinset t).card
Tactic:
simp only [Finset.coe_sort_coe, Fintype.card_coe] at this
State after:
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ s.card = ∑ t in Set.toFinset P', (Set.toFinset t).card

State before:
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ s.card = ∑ t in Set.toFinset P', (Set.toFinset t).card
Tactic:
rw [← this]
State after:
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card =
    ∑ t in Set.toFinset P', (Set.toFinset t).card

State before:
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card =
    ∑ t in Set.toFinset P', (Set.toFinset t).card
Tactic:
apply congr_arg₂
State after:
case hx
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅} = Set.toFinset P'

case hy
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ (fun x => (Set.toFinset x).card) = fun t => (Set.toFinset t).card

State before:
case hx
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅} = Set.toFinset P'
Tactic:
apply Finset.coe_injective
State after:
case hx.a
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ ↑(Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}) = ↑(Set.toFinset P')

State before:
case hx.a
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ ↑(Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}) = ↑(Set.toFinset P')
Tactic:
simp only [Ne.def, Set.coe_toFinset]
State after:
case hx.a
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ ¬t ∩ ↑s = ∅} = P'

State before:
case hx.a
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ ¬t ∩ ↑s = ∅} = P'
Tactic:
exact rfl
State after:
no goals

State before:
case hy
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
⊢ (fun x => (Set.toFinset x).card) = fun t => (Set.toFinset t).card
Tactic:
ext
State after:
case hy.h
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
x✝ : Set { x // x ∈ s }
⊢ (Set.toFinset x✝).card = (Set.toFinset x✝).card

State before:
case hy.h
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
x✝ : Set { x // x ∈ s }
⊢ (Set.toFinset x✝).card = (Set.toFinset x✝).card
Tactic:
apply congr_arg
State after:
case hy.h.h
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
x✝ : Set { x // x ∈ s }
⊢ Set.toFinset x✝ = Set.toFinset x✝

State before:
case hy.h.h
α✝ : Type ?u.17222
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Finset α
P' : Set (Set { x // x ∈ s }) := {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}
this : ∑ x in Set.toFinset {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ ↑s ≠ ∅}, (Set.toFinset x).card = s.card
x✝ : Set { x // x ∈ s }
⊢ Set.toFinset x✝ = Set.toFinset x✝
Tactic:
rw [Set.toFinset_inj]
State after:
no goals