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

State before:
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ (Set.toFinset s).card = ∑ t in Set.toFinset P, (Set.toFinset (s ∩ t)).card
Tactic:
rw [← Finset.card_biUnion]
State after:
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ (Set.toFinset s).card = (Finset.biUnion (Set.toFinset P) fun t => Set.toFinset (s ∩ t)).card

α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ ∀ x ∈ Set.toFinset P, ∀ y ∈ Set.toFinset P, x ≠ y → Disjoint (Set.toFinset (s ∩ x)) (Set.toFinset (s ∩ y))

State before:
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ (Set.toFinset s).card = (Finset.biUnion (Set.toFinset P) fun t => Set.toFinset (s ∩ t)).card

α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ ∀ x ∈ Set.toFinset P, ∀ y ∈ Set.toFinset P, x ≠ y → Disjoint (Set.toFinset (s ∩ x)) (Set.toFinset (s ∩ y))
Tactic:
apply congr_arg
State after:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ Set.toFinset s = Finset.biUnion (Set.toFinset P) fun t => Set.toFinset (s ∩ t)

α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ ∀ x ∈ Set.toFinset P, ∀ y ∈ Set.toFinset P, x ≠ y → Disjoint (Set.toFinset (s ∩ x)) (Set.toFinset (s ∩ y))

State before:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ Set.toFinset s = Finset.biUnion (Set.toFinset P) fun t => Set.toFinset (s ∩ t)
Tactic:
rw [← Finset.coe_inj]
State after:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ ↑(Set.toFinset s) = ↑(Finset.biUnion (Set.toFinset P) fun t => Set.toFinset (s ∩ t))

State before:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ ↑(Set.toFinset s) = ↑(Finset.biUnion (Set.toFinset P) fun t => Set.toFinset (s ∩ t))
Tactic:
simp only [Set.coe_toFinset, Finset.coe_biUnion]
State after:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ s = ⋃ x ∈ P, s ∩ x

State before:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ s = ⋃ x ∈ P, s ∩ x
Tactic:
rw [Set.biUnion_eq_iUnion, ← Set.inter_iUnion, ← Set.sUnion_eq_iUnion]
State after:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ s = s ∩ ⋃₀ P

State before:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ s = s ∩ ⋃₀ P
Tactic:
rw [Setoid.IsPartition.sUnion_eq_univ hP]
State after:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ s = s ∩ Set.univ

State before:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ s = s ∩ Set.univ
Tactic:
exact (Set.inter_univ s).symm
State after:
no goals

State before:
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ ∀ x ∈ Set.toFinset P, ∀ y ∈ Set.toFinset P, x ≠ y → Disjoint (Set.toFinset (s ∩ x)) (Set.toFinset (s ∩ y))
Tactic:
intro t ht u hu htu
State after:
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
t : Set α
ht : t ∈ Set.toFinset P
u : Set α
hu : u ∈ Set.toFinset P
htu : t ≠ u
⊢ Disjoint (Set.toFinset (s ∩ t)) (Set.toFinset (s ∩ u))

State before:
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
t : Set α
ht : t ∈ Set.toFinset P
u : Set α
hu : u ∈ Set.toFinset P
htu : t ≠ u
⊢ Disjoint (Set.toFinset (s ∩ t)) (Set.toFinset (s ∩ u))
Tactic:
simp only [Set.mem_toFinset] at ht hu
State after:
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
t u : Set α
htu : t ≠ u
ht : t ∈ P
hu : u ∈ P
⊢ Disjoint (Set.toFinset (s ∩ t)) (Set.toFinset (s ∩ u))

State before:
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
t u : Set α
htu : t ≠ u
ht : t ∈ P
hu : u ∈ P
⊢ Disjoint (Set.toFinset (s ∩ t)) (Set.toFinset (s ∩ u))
Tactic:
simp only [← Finset.disjoint_coe, Set.coe_toFinset]
State after:
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
t u : Set α
htu : t ≠ u
ht : t ∈ P
hu : u ∈ P
⊢ Disjoint (s ∩ t) (s ∩ u)

State before:
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
t u : Set α
htu : t ≠ u
ht : t ∈ P
hu : u ∈ P
⊢ Disjoint (s ∩ t) (s ∩ u)
Tactic:
exact
  Set.disjoint_of_subset (Set.inter_subset_right s t) (Set.inter_subset_right s u)
    (Setoid.IsPartition.pairwiseDisjoint hP ht hu htu)
State after:
no goals