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

State before:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
⊢ ∑ s in c, s.card = Fintype.card α
Tactic:
rw [← mul_one (Fintype.card α), ← Finset.sum_card]
State after:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
⊢ ∀ (a : α), (Finset.filter (fun x => a ∈ x) c).card = 1

State before:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
⊢ ∀ (a : α), (Finset.filter (fun x => a ∈ x) c).card = 1
Tactic:
intro a
State after:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
⊢ (Finset.filter (fun x => a ∈ x) c).card = 1

State before:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
⊢ (Finset.filter (fun x => a ∈ x) c).card = 1
Tactic:
rw [Finset.card_eq_one]
State after:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}

State before:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Tactic:
obtain ⟨s, hs, hs'⟩ := hc.right a
State after:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : ∃! x, a ∈ s
hs' : ∀ (y : Set α), (fun b => ∃! x, a ∈ b) y → y = s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}

State before:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : ∃! x, a ∈ s
hs' : ∀ (y : Set α), (fun b => ∃! x, a ∈ b) y → y = s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Tactic:
simp only [Set.mem_setOf_eq, exists_unique_iff_exists, exists_eq_left', exists_prop, and_imp] at hs hs'
State after:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}

State before:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Tactic:
have hs'2 : ∀ z : Finset α, z ∈ c → a ∈ z → z = s.toFinset := by
  intro z hz ha
  rw [← Finset.coe_inj, Set.coe_toFinset]
  refine hs' z ?_ (Finset.mem_coe.mpr ha)
  simp only [Finset.toFinset_coe, hz]
State after:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}

State before:
case intro.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}
Tactic:
use s.toFinset
State after:
case h
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
⊢ Finset.filter (fun x => a ∈ x) c = {Set.toFinset s}

State before:
case h
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
⊢ Finset.filter (fun x => a ∈ x) c = {Set.toFinset s}
Tactic:
ext t
State after:
case h.a
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ Finset.filter (fun x => a ∈ x) c ↔ t ∈ {Set.toFinset s}

State before:
case h.a
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ Finset.filter (fun x => a ∈ x) c ↔ t ∈ {Set.toFinset s}
Tactic:
simp only [Finset.mem_filter, Finset.mem_singleton]
State after:
case h.a
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ c ∧ a ∈ t ↔ t = Set.toFinset s

State before:
case h.a
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ c ∧ a ∈ t ↔ t = Set.toFinset s
Tactic:
constructor
State after:
case h.a.mp
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ c ∧ a ∈ t → t = Set.toFinset s

case h.a.mpr
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t = Set.toFinset s → t ∈ c ∧ a ∈ t

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

State before:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
z : Finset α
hz : z ∈ c
ha : a ∈ z
⊢ z = Set.toFinset s
Tactic:
rw [← Finset.coe_inj, Set.coe_toFinset]
State after:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
z : Finset α
hz : z ∈ c
ha : a ∈ z
⊢ ↑z = s

State before:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
z : Finset α
hz : z ∈ c
ha : a ∈ z
⊢ ↑z = s
Tactic:
refine hs' z ?_ (Finset.mem_coe.mpr ha)
State after:
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
z : Finset α
hz : z ∈ c
ha : a ∈ z
⊢ Set.toFinset ↑z ∈ c

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

State before:
case h.a.mp
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t ∈ c ∧ a ∈ t → t = Set.toFinset s
Tactic:
rintro ⟨ht, ha⟩
State after:
case h.a.mp.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
ht : t ∈ c
ha : a ∈ t
⊢ t = Set.toFinset s

State before:
case h.a.mp.intro
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
ht : t ∈ c
ha : a ∈ t
⊢ t = Set.toFinset s
Tactic:
exact hs'2 t ht ha
State after:
no goals

State before:
case h.a.mpr
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
⊢ t = Set.toFinset s → t ∈ c ∧ a ∈ t
Tactic:
intro ht
State after:
case h.a.mpr
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
ht : t = Set.toFinset s
⊢ t ∈ c ∧ a ∈ t

State before:
case h.a.mpr
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
ht : t = Set.toFinset s
⊢ t ∈ c ∧ a ∈ t
Tactic:
simp only [ht, Set.mem_toFinset]
State after:
case h.a.mpr
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
ht : t = Set.toFinset s
⊢ Set.toFinset s ∈ c ∧ a ∈ s

State before:
case h.a.mpr
α : Type u_1
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, Set.toFinset s = t ∧ t ∈ c}
a : α
s : Set α
hs : Set.toFinset s ∈ c ∧ a ∈ s
hs' : ∀ (y : Set α), Set.toFinset y ∈ c → a ∈ y → y = s
hs'2 : ∀ z ∈ c, a ∈ z → z = Set.toFinset s
t : Finset α
ht : t = Set.toFinset s
⊢ Set.toFinset s ∈ c ∧ a ∈ s
Tactic:
exact hs
State after:
no goals