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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, 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✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
⊢ ∀ (a : α), (Finset.filter (fun x => a ∈ x) c).card = 1

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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, 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✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
a : α
⊢ ∃ a_1, Finset.filter (fun x => a ∈ x) c = {a_1}

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

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

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

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

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

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

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

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

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

case h.a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
a : α
t : Finset α
ht : t ∈ c
has : a ∈ ↑t
hs' : ∀ (y : Set α) (x : Finset α), y = ↑x → x ∈ c → a ∈ y → y = ↑t
u : Finset α
⊢ u = t → u ∈ c ∧ a ∈ u

State before:
case h.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
a : α
t : Finset α
ht : t ∈ c
has : a ∈ ↑t
hs' : ∀ (y : Set α) (x : Finset α), y = ↑x → x ∈ c → a ∈ y → y = ↑t
u : Finset α
⊢ u ∈ c ∧ a ∈ u → u = t
Tactic:
rintro ⟨huc, hau⟩
State after:
case h.a.mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
a : α
t : Finset α
ht : t ∈ c
has : a ∈ ↑t
hs' : ∀ (y : Set α) (x : Finset α), y = ↑x → x ∈ c → a ∈ y → y = ↑t
u : Finset α
huc : u ∈ c
hau : a ∈ u
⊢ u = t

State before:
case h.a.mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
a : α
t : Finset α
ht : t ∈ c
has : a ∈ ↑t
hs' : ∀ (y : Set α) (x : Finset α), y = ↑x → x ∈ c → a ∈ y → y = ↑t
u : Finset α
huc : u ∈ c
hau : a ∈ u
⊢ u = t
Tactic:
rw [← Finset.coe_inj]
State after:
case h.a.mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
a : α
t : Finset α
ht : t ∈ c
has : a ∈ ↑t
hs' : ∀ (y : Set α) (x : Finset α), y = ↑x → x ∈ c → a ∈ y → y = ↑t
u : Finset α
huc : u ∈ c
hau : a ∈ u
⊢ ↑u = ↑t

State before:
case h.a.mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
a : α
t : Finset α
ht : t ∈ c
has : a ∈ ↑t
hs' : ∀ (y : Set α) (x : Finset α), y = ↑x → x ∈ c → a ∈ y → y = ↑t
u : Finset α
huc : u ∈ c
hau : a ∈ u
⊢ ↑u = ↑t
Tactic:
exact hs' ↑u u rfl huc hau
State after:
no goals

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

State before:
case h.a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
a : α
t : Finset α
ht : t ∈ c
has : a ∈ ↑t
hs' : ∀ (y : Set α) (x : Finset α), y = ↑x → x ∈ c → a ∈ y → y = ↑t
u : Finset α
hut : u = t
⊢ u ∈ c ∧ a ∈ u
Tactic:
rw [hut]
State after:
case h.a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
a : α
t : Finset α
ht : t ∈ c
has : a ∈ ↑t
hs' : ∀ (y : Set α) (x : Finset α), y = ↑x → x ∈ c → a ∈ y → y = ↑t
u : Finset α
hut : u = t
⊢ t ∈ c ∧ a ∈ t

State before:
case h.a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Finset (Finset α)
hc : Setoid.IsPartition {s | ∃ t, s = ↑t ∧ t ∈ c}
a : α
t : Finset α
ht : t ∈ c
has : a ∈ ↑t
hs' : ∀ (y : Set α) (x : Finset α), y = ↑x → x ∈ c → a ∈ y → y = ↑t
u : Finset α
hut : u = t
⊢ t ∈ c ∧ a ∈ t
Tactic:
exact ⟨ht, has⟩
State after:
no goals