awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Set (Setoid α)
e_r : ∀ (x y : α), (∃ r ∈ s, (r : α → α → Prop) x y) ↔ (⨆ a ∈ s, (⇑a : α → α → Prop)) x y
⊢ Eq.{u_1 + 1} (α := Setoid α) (EqvGen.setoid fun (x y : α) ↦ ∃ r ∈ s, (r : α → α → Prop) x y)
    (EqvGen.setoid (⨆ a ∈ s, (⇑a : α → α → Prop)))

Tactic:
congr with (x y)
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Set (Setoid α)
x y : α
⊢ (∃ r ∈ s, (r : α → α → Prop) x y) ↔ (⨆ a ∈ s, (⇑a : α → α → Prop)) x y

Tactic:
simp only [iSup_apply, iSup_Prop_eq, exists_prop]

Premises used: exists_prop, iSup_Prop_eq, iSup_apply
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : Setoid α
rw : sInf {s : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y → (s : α → α → Prop) x y} ≤ r
⊢ EqvGen.setoid (⇑r : α → α → Prop) ≤ r

Tactic:
rw [eqvGen_eq]

Premises used: Setoid.eqvGen_eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : Setoid α
⊢ sInf {s : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y → (s : α → α → Prop) x y} ≤ r

Tactic:
sInf_le fun _ _ => id

Premises used: id, sInf_le
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : Setoid α
⊢ sInf {s : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y → (s : α → α → Prop) x y} ≤ r

Tactic:
exact sInf_le fun _ _ => id
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
⊢ EqvGen.setoid (⇑(EqvGen.setoid r) : α → α → Prop) = EqvGen.setoid r

Tactic:
eqvGen_of_setoid _

Premises used: Setoid.eqvGen_of_setoid
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → (s : α → α → Prop) x y
rw : sInf {s : Setoid α | ∀ ⦃x y : α⦄, r x y → (s : α → α → Prop) x y} ≤ s
⊢ EqvGen.setoid r ≤ s

Tactic:
rw [eqvGen_eq]

Premises used: Setoid.eqvGen_eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → (s : α → α → Prop) x y
⊢ sInf {s : Setoid α | ∀ ⦃x y : α⦄, r x y → (s : α → α → Prop) x y} ≤ s

Tactic:
sInf_le h

Premises used: sInf_le
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → (s : α → α → Prop) x y
⊢ sInf {s : Setoid α | ∀ ⦃x y : α⦄, r x y → (s : α → α → Prop) x y} ≤ s

Tactic:
exact sInf_le h
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r s : α → α → Prop
h : ∀ (x y : α), r x y → s x y
⊢ EqvGen.setoid r ≤ EqvGen.setoid s

Tactic:
eqvGen_le fun _ _ hr => EqvGen.rel _ _ <| h _ _ hr

Premises used: Setoid.eqvGen_le, Relation.EqvGen.rel
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Injective f ↔ ker f = ⊥

Tactic:
(@eq_bot_iff (Setoid α) _ _ (ker f)).symm

Premises used: Function.Injective, eq_bot_iff, Iff.symm
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
x y : α
⊢ (ker f : α → α → Prop) x y ↔ x ∈ f ⁻¹' {f y}

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : Quotient r → β
x y : α
h : (r : α → α → Prop) x y
⊢ (ker (f ∘ Quotient.mk'') : α → α → Prop) x y

Tactic:
simp [ker_def, Quotient.sound' h]

Premises used: Quotient.sound', Setoid.ker_def
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
h : ∀ (x : Quotient r) (x : α), Quotient.lift f H (Quot.mk (⇑r : α → α → Prop) x) = g (Quot.mk (⇑r : α → α → Prop) x)
⊢ Quotient.lift f H = g

Tactic:
ext ⟨x⟩
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x_1 : Quotient r
x : α
h : Quotient.lift f H ⟦x⟧ = g ⟦x⟧
h₁ : f x = g ⟦x⟧
h₂ : (g ∘ Quotient.mk'') x = g ⟦x⟧
h₃ : g (Quotient.mk'' x) = g ⟦x⟧
h₄ h₅ : g ⟦x⟧ = g ⟦x⟧
⊢ Quotient.lift f H (Quot.mk (⇑r : α → α → Prop) x) = g (Quot.mk (⇑r : α → α → Prop) x)

Tactic:
rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]

Premises used: Quotient.lift_mk, Quotient.mk, Function.comp_apply, Quotient.mk''_eq_mk
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ kerLift f ⟦x⟧ = f x

Tactic:
rfl

Premises used: Setoid.kerLift, rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Injective (kerLift f)

Tactic:
fun x y => Quotient.inductionOn₂' x y fun _ _ h => Quotient.sound' h

Premises used: Quotient.inductionOn₂', Function.Injective
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
h : Injective (Quotient.lift f H)
⊢ ker f = r

Tactic:
le_antisymm
    (fun x y hk =>
      Quotient.exact <| h <| show Quotient.lift f H ⟦x⟧ = Quotient.lift f H ⟦y⟧ from hk)
    H

Premises used: le_antisymm, Quotient.exact
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hle : r ≤ ker f
⊢ Injective (Quotient.lift f hle) ↔ ker f = r

Tactic:
⟨ker_eq_lift_of_injective f hle, fun h ↦ h ▸ kerLift_injective _⟩

Premises used: Setoid.kerLift_injective, Iff.intro, Setoid.ker_eq_lift_of_injective
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Set.range (kerLift f) = Set.range f

Tactic:
Set.range_quotient_lift (s := ker f) _

Premises used: Setoid.kerLift, Set.range_quotient_lift
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
rw : r.map f = Relation.EqvGen.setoid (⇑(r.mapOfSurjective f h hf) : β → β → Prop)
⊢ r.map f = r.mapOfSurjective f h hf

Tactic:
rw [← eqvGen_of_setoid (mapOfSurjective r f h hf)]

Premises used: Setoid.mapOfSurjective, Setoid.eqvGen_of_setoid
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ r.map f = Relation.EqvGen.setoid (⇑(r.mapOfSurjective f h hf) : β → β → Prop)

Tactic:
rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid β
x y : α
⊢ (comap f r : α → α → Prop) x y ↔ (r : β → β → Prop) (f x) (f y)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid β
x y : α
rw : (comap f r : α → α → Prop) x y ↔ (r : β → β → Prop) (f x) (f y)
⊢ (comap f r : α → α → Prop) x y ↔ ⟦f x⟧ = ⟦f y⟧

Tactic:
rw [Quotient.eq]

Premises used: Quotient.eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid β
x y : α
⊢ (comap f r : α → α → Prop) x y ↔ (r : β → β → Prop) (f x) (f y)

Tactic:
rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient (ker (Quot.mapRight (ra := (⇑r : α → α → Prop)) (ra' := (⇑s : α → α → Prop)) h))
y : Quot (α := α) (⇑r : α → α → Prop)
w : α
⊢ ⟦Quotient.mk'' w⟧ = Quotient.mk'' (Quotient.mk'' w)

Tactic:
rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient s
y : α
⊢ ⟦y⟧ = Quotient.mk'' y

Tactic:
rfl
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
β : Type u_2
r_1 : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : (r : α → α → Prop) x y
rw : (s : Quotient r → Quotient r → Prop) (Quotient.mk' x) (Quotient.mk' y)
rw₁ rw₂ : (s : Quotient r → Quotient r → Prop) (Quotient.mk' y) (Quotient.mk' y)
⊢ (comap Quotient.mk' s : α → α → Prop) x y

Tactic:
rw [comap_rel, Quotient.eq'.2 h]

Premises used: Iff.mpr, Setoid.comap_rel, Quotient.eq'
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Setoid α
simp : (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → (s : α → α → Prop) x y
⊢ Subsingleton.{u_1 + 1} (Quotient s) ↔ s = ⊤

Tactic:
simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply]

Premises used: eq_top_iff, subsingleton_iff, Setoid.top_def, Pi.top_apply, Setoid.le_def
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Setoid α
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → (s : α → α → Prop) x y

Tactic:
Quotient.mk'_surjective.forall.trans (forall_congr' fun a => ?_)

Premises used: Function.Surjective.forall, Quotient.mk'_surjective, forall_congr', Iff.trans
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Setoid α
refine : ∀ (a : α), (∀ (y : Quotient s), Quotient.mk' a = y) ↔ ∀ {y : α}, ⊤ → (s : α → α → Prop) a y
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → (s : α → α → Prop) x y

Tactic:
refine Quotient.mk'_surjective.forall.trans (forall_congr' fun a => ?_)

Premises used: Function.Surjective.forall, Quotient.mk'_surjective, forall_congr', Iff.trans
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Setoid α
a : α
⊢ (∀ (y : Quotient s), Quotient.mk' a = y) ↔ ∀ {y : α}, ⊤ → (s : α → α → Prop) a y

Tactic:
Quotient.mk'_surjective.forall.trans (forall_congr' fun b => ?_)

Premises used: Function.Surjective.forall, Quotient.mk'_surjective, forall_congr', Iff.trans
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Setoid α
a : α
refine : ∀ (b : α), Eq (α := Quotient s) (Quotient.mk' a) (Quotient.mk' b) ↔ ⊤ → (s : α → α → Prop) a b
⊢ (∀ (y : Quotient s), Quotient.mk' a = y) ↔ ∀ {y : α}, ⊤ → (s : α → α → Prop) a y

Tactic:
refine Quotient.mk'_surjective.forall.trans (forall_congr' fun b => ?_)

Premises used: Function.Surjective.forall, Quotient.mk'_surjective, forall_congr', Iff.trans
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
s : Setoid α
a b : α
simp_rw : Eq (α := Quotient s) (Quotient.mk' a) (Quotient.mk' b) ↔ True → (s : α → α → Prop) a b
simp_rw₁ : Eq (α := Quotient s) (Quotient.mk' a) (Quotient.mk' b) ↔ (s : α → α → Prop) a b
⊢ Eq (α := Quotient s) (Quotient.mk' a) (Quotient.mk' b) ↔ ⊤ → (s : α → α → Prop) a b

Tactic:
simp_rw [Prop.top_eq_true, true_implies, Quotient.eq']

Premises used: Quotient.eq', true_implies, Prop.top_eq_true
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
simp : (∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ Relation.EqvGen r i i_1
⊢ Subsingleton.{u_1 + 1} (Quot r) ↔ Relation.EqvGen r = ⊤

Tactic:
simp only [_root_.subsingleton_iff, _root_.eq_top_iff, Pi.le_def, Pi.top_apply]

Premises used: eq_top_iff, subsingleton_iff, Pi.top_apply, Pi.le_def
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
⊢ (∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ Relation.EqvGen r i i_1

Tactic:
Quot.mk_surjective.forall.trans (forall_congr' fun a => ?_)

Premises used: Function.Surjective.forall, forall_congr', Iff.trans, Quot.mk_surjective
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
refine : ∀ (a : α), (∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ Relation.EqvGen r a i
⊢ (∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ Relation.EqvGen r i i_1

Tactic:
refine Quot.mk_surjective.forall.trans (forall_congr' fun a => ?_)

Premises used: Function.Surjective.forall, forall_congr', Iff.trans, Quot.mk_surjective
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
a : α
⊢ (∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ Relation.EqvGen r a i

Tactic:
Quot.mk_surjective.forall.trans (forall_congr' fun b => ?_)

Premises used: Function.Surjective.forall, forall_congr', Iff.trans, Quot.mk_surjective
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
a : α
refine : ∀ (b : α), mk r a = mk r b ↔ ⊤ ≤ Relation.EqvGen r a b
⊢ (∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ Relation.EqvGen r a i

Tactic:
refine Quot.mk_surjective.forall.trans (forall_congr' fun b => ?_)

Premises used: Function.Surjective.forall, forall_congr', Iff.trans, Quot.mk_surjective
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
a b : α
rw : Relation.EqvGen r a b ↔ ⊤ ≤ Relation.EqvGen r a b
⊢ mk r a = mk r b ↔ ⊤ ≤ Relation.EqvGen r a b

Tactic:
rw [Quot.eq]

Premises used: Quot.eq
-- Module: Mathlib.Data.Setoid.Basic
Goal:
α : Type u_1
r : α → α → Prop
a b : α
⊢ Relation.EqvGen r a b ↔ ⊤ ≤ Relation.EqvGen r a b

Tactic:
simp
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
⊢ ∀ (t : Set α), (s ∩ t).Finite

Tactic:
have hst (t : Set α) : (s ∩ t).Finite := hs.inter_of_left t
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
⊢ ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card

Tactic:
have hst' (t : Set α) : Nat.card ↑(s ∩ t) = (hst t).toFinset.card :=
    Nat.card_eq_card_finite_toFinset (hst t)
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
rw :
  s.ncard =
    ∑ i ∈ Set.Finite.toFinset (s := Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) hs',
      (s ∩ (↑i : Set α)).ncard
⊢ s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard

Tactic:
rw [finsum_def, dif_pos hs']

Premises used: dif_pos, finsum_def
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
simp :
  hs.toFinset (s := s).card =
    ∑
      t ∈
        Set.Finite.toFinset (s :=
          Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1)) ⋯,
      Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1)
⊢ s.ncard =
    ∑ i ∈ Set.Finite.toFinset (s := Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) hs',
      (s ∩ (↑i : Set α)).ncard

Tactic:
simp only [← Nat.card_coe_set_eq, Nat.card_eq_card_finite_toFinset hs]

Premises used: Nat.card_coe_set_eq, Nat.card_eq_card_finite_toFinset
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
t : (↑P : Type u_1)
ht :
  t ∈
    Set.Finite.toFinset (s :=
      Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1)) ⋯
⊢ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1) = (Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯).card

Tactic:
hst' ↑t

Premises used: Subtype.val
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
t : (↑P : Type u_1)
ht :
  t ∈
    Set.Finite.toFinset (s :=
      Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1)) ⋯
⊢ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1) = (Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯).card

Tactic:
exact hst' ↑t

Premises used: Subtype.val
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
rw :
  hs.toFinset (s := s).card =
    ∑
      t ∈
        Set.Finite.toFinset (s :=
          Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1)) ⋯,
      (Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯).card
⊢ hs.toFinset (s := s).card =
    ∑
      t ∈
        Set.Finite.toFinset (s :=
          Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1)) ⋯,
      Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1)

Tactic:
rw [Finset.sum_congr rfl (fun t ht ↦ by exact hst' ↑t)]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
rw :
  Finset.card (α := (_ : (↑P : Type u_1)) × α)
      ((Set.Finite.toFinset (s :=
            Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1))
            ⋯).sigma
        (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦
        Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯) =
    hs.toFinset (s := s).card
⊢ hs.toFinset (s := s).card =
    ∑
      t ∈
        Set.Finite.toFinset (s :=
          Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1)) ⋯,
      (Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯).card

Tactic:
rw [← Finset.card_sigma, eq_comm]

Premises used: Finset.card_sigma, eq_comm
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
hi :
  Set.MapsTo
    (fun (x : (_ : (↑P : Type u_1)) × α) ↦
      match (motive := (_ : (↑P : Type u_1)) × α → α) x with
      | ⟨t, x⟩ => x)
    (↑((Set.Finite.toFinset (s :=
              Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1))
              ⋯).sigma
          (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦
          Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯) :
      Set ((_ : (↑P : Type u_1)) × α))
    (↑(hs.toFinset (s := s)) : Set α)
hj :
  Set.MapsTo
    (fun (x : α) ↦
      Sigma.mk (β := fun (i : (↑P : Type u_1)) ↦ α)
        (Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯) x)
    (↑(hs.toFinset (s := s)) : Set α)
    (↑((Set.Finite.toFinset (s :=
              Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1))
              ⋯).sigma
          (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦
          Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯) :
      Set ((_ : (↑P : Type u_1)) × α))
left_inv :
  Set.LeftInvOn
    (fun (x : α) ↦
      Sigma.mk (β := fun (i : (↑P : Type u_1)) ↦ α)
        (Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯) x)
    (fun (x : (_ : (↑P : Type u_1)) × α) ↦
      match (motive := (_ : (↑P : Type u_1)) × α → α) x with
      | ⟨t, x⟩ => x)
    (↑((Set.Finite.toFinset (s :=
              Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1))
              ⋯).sigma
          (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦
          Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯) :
      Set ((_ : (↑P : Type u_1)) × α))
right_inv :
  Set.RightInvOn
    (fun (x : α) ↦
      Sigma.mk (β := fun (i : (↑P : Type u_1)) ↦ α)
        (Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯) x)
    (fun (x : (_ : (↑P : Type u_1)) × α) ↦
      match (motive := (_ : (↑P : Type u_1)) × α → α) x with
      | ⟨t, x⟩ => x)
    (↑(hs.toFinset (s := s)) : Set α)
⊢ Finset.card (α := (_ : (↑P : Type u_1)) × α)
      ((Set.Finite.toFinset (s :=
            Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1))
            ⋯).sigma
        (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦
        Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯) =
    hs.toFinset (s := s).card

Tactic:
apply Finset.card_nbij' (fun ⟨t, x⟩ ↦ x)
      (fun x ↦ ⟨⟨(hP.2 x).exists.choose, (hP.2 x).exists.choose_spec.1⟩, x⟩)

Premises used: Finset.card_nbij'
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
t : (↑P : Type u_1)
x : α
⊢ Sigma.mk (β := fun (i : (↑P : Type u_1)) ↦ α) t x ∈
      (↑((Set.Finite.toFinset (s :=
                Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1))
                ⋯).sigma
            (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦
            Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯) :
        Set ((_ : (↑P : Type u_1)) × α)) →
    (fun (x : (_ : (↑P : Type u_1)) × α) ↦
          (match (motive := (_ : (↑P : Type u_1)) × α → α) x with
            | ⟨t, x⟩ => x :
            α))
        (Sigma.mk (β := fun (i : (↑P : Type u_1)) ↦ α) t x) ∈
      (↑(hs.toFinset (s := s)) : Set α)

Tactic:
simp +contextual
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
x : α
hj :
  x ∈ s →
    Nat.card.{u_1} (↑(s ∩ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) : Type u_1) ≠ 0 ∧
      x ∈ s ∧ x ∈ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)
⊢ x ∈ (↑(hs.toFinset (s := s)) : Set α) →
    (fun (x : α) ↦
          (Sigma.mk (β := fun (i : (↑P : Type u_1)) ↦ α)
              (Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯) x :
            (_ : (↑P : Type u_1)) × α))
        x ∈
      (↑((Set.Finite.toFinset (s :=
                Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1))
                ⋯).sigma
            (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦
            Set.Finite.toFinset (s := s ∩ (↑t : Set α)) ⋯) :
        Set ((_ : (↑P : Type u_1)) × α))

Tactic:
simp only [Set.Finite.mem_toFinset, Finset.mem_sigma, Function.mem_support, Set.mem_inter_iff,
        Finset.mem_coe]

Premises used: Set.Finite.mem_toFinset, Set.mem_inter_iff, Finset.mem_sigma, Function.mem_support, Finset.mem_coe
-- Module: Mathlib.Data.Setoid.Partition.Card
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
x : α
hx : x ∈ s
⊢ Nat.card.{u_1} (↑(s ∩ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) : Type u_1) ≠ 0 ∧
    x ∈ s ∧ x ∈ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)

Tactic:
⟨Nat.card_ne_zero.mpr ⟨?_, hst (hP.right x).exists.choose⟩,
        hx, (hP.2 x).exists.choose_spec.2⟩

Premises used: Iff.mpr, Exists.choose_spec, ExistsUnique.exists, And.right, And.intro, Exists.choose, Nat.card_ne_zero