internlm/Lean-Github huggingface dataset:
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 (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)
Proof state after:
no goals
Theorem: Setoid.IsPartition.card_eq_sum_parts
Proof state before:
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Fintype.card α = ∑ t in Set.toFinset P, (Set.toFinset t).card
Tactic:
rw [← Finset.card_univ]
Proof state after:
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Finset.univ.card = ∑ t in Set.toFinset P, (Set.toFinset t).card
Theorem: Setoid.IsPartition.card_eq_sum_parts
Proof state before:
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Finset.univ.card = ∑ t in Set.toFinset P, (Set.toFinset t).card
Tactic:
convert Setoid.IsPartition.card_set_eq_sum_parts Set.univ hP
Proof state after:
case h.e'_2.h.e'_2
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Finset.univ = Set.toFinset Set.univ

case h.e'_3.a.h.e'_2.h
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
x✝ : Set α
a✝ : x✝ ∈ Set.toFinset P
⊢ x✝ = Set.univ ∩ x✝
Theorem: Setoid.IsPartition.card_eq_sum_parts
Proof state before:
case h.e'_2.h.e'_2
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Finset.univ = Set.toFinset Set.univ
Tactic:
rw [Set.toFinset_univ.symm]
Proof state after:
case h.e'_2.h.e'_2
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Set.toFinset Set.univ = Set.toFinset Set.univ
Theorem: Setoid.IsPartition.card_eq_sum_parts
Proof state before:
case h.e'_2.h.e'_2
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Set.toFinset Set.univ = Set.toFinset Set.univ
Tactic:
congr
Proof state after:
case h.e'_2.h.e'_2.h.e_3.h
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Set.fintypeUniv = Subtype.fintype fun x => x ∈ Set.univ
Theorem: Setoid.IsPartition.card_eq_sum_parts
Proof state before:
case h.e'_2.h.e'_2.h.e_3.h
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
⊢ Set.fintypeUniv = Subtype.fintype fun x => x ∈ Set.univ
Tactic:
simp only [eq_iff_true_of_subsingleton]
Proof state after:
no goals
Theorem: Setoid.IsPartition.card_eq_sum_parts
Proof state before:
case h.e'_3.a.h.e'_2.h
α✝ : Type ?u.12056
α : Type u_1
inst✝ : Fintype α
P : Set (Set α)
hP : IsPartition P
x✝ : Set α
a✝ : x✝ ∈ Set.toFinset P
⊢ x✝ = Set.univ ∩ x✝
Tactic:
rw [Set.univ_inter]
Proof state after:
no goals
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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'
Proof 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
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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 α))
Proof 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
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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
Proof 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
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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]
Proof 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
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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₂
Proof 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
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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
Proof 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')
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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]
Proof 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'
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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
Proof state after:
no goals
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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
Proof 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
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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
Proof 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✝
Theorem: Setoid.IsPartition.card_finset_eq_sum_parts
Proof 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]
Proof state after:
no goals
Theorem: Partition.card_of_partition''
Proof 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]
Proof 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
Theorem: Partition.card_of_partition''
Proof 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
Proof 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
Theorem: Partition.card_of_partition''
Proof 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]
Proof 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}
Theorem: Partition.card_of_partition''
Proof 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
Proof 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}
Theorem: Partition.card_of_partition''
Proof 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
Proof 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}
Theorem: Partition.card_of_partition''
Proof 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
Proof 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}
Theorem: Partition.card_of_partition''
Proof 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'
Proof 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}
Theorem: Partition.card_of_partition''
Proof 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
Proof 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}
Theorem: Partition.card_of_partition''
Proof 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
Proof 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}
Theorem: Partition.card_of_partition''
Proof 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
Proof 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}
Theorem: Partition.card_of_partition''
Proof 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]
Proof 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
Theorem: Partition.card_of_partition''
Proof 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
Proof 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
Theorem: Partition.card_of_partition''
Proof 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⟩
Proof 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
Theorem: Partition.card_of_partition''
Proof 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]
Proof 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
Theorem: Partition.card_of_partition''
Proof 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
Proof state after:
no goals
Theorem: Partition.card_of_partition''
Proof 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
Proof 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
Theorem: Partition.card_of_partition''
Proof 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]
Proof 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
Theorem: Partition.card_of_partition''
Proof 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⟩
Proof state after:
no goals
Theorem: Subgroup.map_subgroupOf_eq
Proof state before:
α : Type ?u.335
G : Type u_1
H : Type ?u.341
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
K : Subgroup ↥N
⊢ subgroupOf (map (Subgroup.subtype N) K) N = K
Tactic:
rw [← Subgroup.comap_subtype, Subgroup.comap_map_eq, Subgroup.ker_subtype, sup_bot_eq]
Proof state after:
no goals
Theorem: MulAction.stabilizer_subgroupOf_eq
Proof state before:
α : Type u_2
G : Type u_1
H : Type ?u.1696
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
a : α
⊢ stabilizer (↥N) a = Subgroup.subgroupOf (stabilizer G a) N
Tactic:
ext n
Proof state after:
case h
α : Type u_2
G : Type u_1
H : Type ?u.1696
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
a : α
n : ↥N
⊢ n ∈ stabilizer (↥N) a ↔ n ∈ Subgroup.subgroupOf (stabilizer G a) N