internlm/Lean-Github huggingface dataset:
Theorem: Partition.card_of_partition'
Proof 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
Proof 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
Theorem: Partition.card_of_partition'
Proof 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]
Proof 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
Theorem: Partition.card_of_partition'
Proof 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)
Proof 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
Theorem: Partition.card_of_partition'
Proof 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]
Proof state after:
no goals
Theorem: Partition.card_of_partition'
Proof 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⟩
Proof 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
Theorem: Partition.card_of_partition'
Proof 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
Proof state after:
no goals
Theorem: Partition.card_of_partition'
Proof 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
Proof 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
Theorem: Partition.card_of_partition'
Proof 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]
Proof 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
Theorem: Partition.card_of_partition'
Proof 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
Proof state after:
no goals
Theorem: Partition.card_of_partition
Proof 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
Proof 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 α
Theorem: Partition.card_of_partition
Proof 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]
Proof 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 α
Theorem: Partition.card_of_partition
Proof 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
Proof 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 α
Theorem: Partition.card_of_partition
Proof 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]
Proof 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
Theorem: Partition.card_of_partition
Proof 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
Proof 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
Theorem: Partition.card_of_partition
Proof 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
Proof 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
Theorem: Partition.card_of_partition
Proof 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 _ _]
Proof 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
Theorem: Partition.card_of_partition
Proof 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] }
Proof state after:
no goals
Theorem: Partition.card_of_partition
Proof 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]
Proof state after:
no goals
Theorem: Partition.card_of_partition
Proof 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
Proof 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'
Theorem: Partition.card_of_partition
Proof 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]
Proof 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
Theorem: Partition.card_of_partition
Proof 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
Proof 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
Theorem: Partition.card_of_partition
Proof 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
Proof state after:
no goals
Theorem: Partition.card_of_partition
Proof 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
Proof 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
Theorem: Partition.card_of_partition
Proof 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
Proof 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
Theorem: Partition.card_of_partition
Proof 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]
Proof 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
Theorem: Partition.card_of_partition
Proof 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
Proof state after:
no goals
Theorem: Partition.card_of_partition
Proof 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
Proof 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✝
Theorem: Partition.card_of_partition
Proof 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]
Proof state after:
no goals
Theorem: Setoid.IsPartition.card_set_eq_sum_parts
Proof 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]
Proof 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))
Theorem: Setoid.IsPartition.card_set_eq_sum_parts
Proof 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
Proof 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))
Theorem: Setoid.IsPartition.card_set_eq_sum_parts
Proof 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]
Proof 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))
Theorem: Setoid.IsPartition.card_set_eq_sum_parts
Proof 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]
Proof 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
Theorem: Setoid.IsPartition.card_set_eq_sum_parts
Proof 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]
Proof state after:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ s = s ∩ ⋃₀ P
Theorem: Setoid.IsPartition.card_set_eq_sum_parts
Proof 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]
Proof state after:
case h
α✝ : Type ?u.9159
α : Type u_1
inst✝ : Fintype α
s : Set α
P : Set (Set α)
hP : IsPartition P
⊢ s = s ∩ Set.univ
Theorem: Setoid.IsPartition.card_set_eq_sum_parts
Proof 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
Proof state after:
no goals
Theorem: Setoid.IsPartition.card_set_eq_sum_parts
Proof 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
Proof 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))
Theorem: Setoid.IsPartition.card_set_eq_sum_parts
Proof 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
Proof 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))
Theorem: Setoid.IsPartition.card_set_eq_sum_parts
Proof 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]
Proof 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)