awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hj : Nonempty.{u_1 + 1} (↑(s ∩ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) : Type u_1)
⊢ 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:
refine ⟨Nat.card_ne_zero.mpr ⟨?_, hst (hP.right x).exists.choose⟩,
        hx, (hP.2 x).exists.choose_spec.2⟩
-- 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
hj : ∃ a ∈ s, a ∈ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)
⊢ Nonempty.{u_1 + 1} (↑(s ∩ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) : Type u_1)

Tactic:
simp only [nonempty_subtype, Set.mem_inter_iff]

Premises used: Set.mem_inter_iff, nonempty_subtype
-- 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
w : α
left : x ∈ s
right : x ∈ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)
⊢ ∃ a ∈ s, a ∈ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)

Tactic:
use x, hx, (hP.2 x).exists.choose_spec.2

Premises used: Exists.choose_spec, ExistsUnique.exists, And.right
-- 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 : α
left_inv :
  Nonempty.{u_1 + 1} (↑(s ∩ (↑t : Set α)) : Type u_1) →
    Finite.{u_1 + 1} (↑(s ∩ (↑t : Set α)) : Type u_1) →
      x ∈ s →
        x ∈ (↑t : Set α) →
          Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯ = t
⊢ 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)) × α)) →
    Eq (α := (_ : (↑P : Type u_1)) × α)
      ((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)) × α))
        ((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)))
      (Sigma.mk (β := fun (i : (↑P : Type u_1)) ↦ α) t x)

Tactic:
simp only [Finset.mem_sigma, Set.Finite.mem_toFinset, Function.mem_support, Nat.card_ne_zero,
        Set.mem_inter_iff, Sigma.mk.inj_iff, heq_eq_eq, and_true, and_imp, Finset.mem_coe]

Premises used: and_true, and_imp, Set.Finite.mem_toFinset, Set.mem_inter_iff, heq_eq_eq, Finset.mem_sigma, Sigma.mk.inj_iff, Function.mem_support, Nat.card_ne_zero, 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
t : (↑P : Type u_1)
x : α
left_inv :
  ∀ x_1 ∈ s,
    x_1 ∈ (↑t : Set α) →
      Finite.{u_1 + 1} (↑(s ∩ (↑t : Set α)) : Type u_1) →
        x ∈ s →
          x ∈ (↑t : Set α) →
            Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_2 : Set α) ↦ x_2 ∈ P ∧ x ∈ x_2)) ⋯ = t
⊢ Nonempty.{u_1 + 1} (↑(s ∩ (↑t : Set α)) : Type u_1) →
    Finite.{u_1 + 1} (↑(s ∩ (↑t : Set α)) : Type u_1) →
      x ∈ s →
        x ∈ (↑t : Set α) →
          Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯ = t

Tactic:
simp only [nonempty_subtype, Set.mem_inter_iff, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_inter_iff, forall_exists_index, nonempty_subtype
-- 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 y : α
hy : y ∈ s
hyt : y ∈ (↑t : Set α)
left_inv :
  Finite.{u_1 + 1} (↑(s ∩ (↑t : Set α)) : Type u_1) →
    x ∈ s →
      x ∈ (↑t : Set α) →
        Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯ = t
⊢ Finite.{u_1 + 1} (↑(s ∩ (↑t : Set α)) : Type u_1) →
    x ∈ s →
      x ∈ (↑t : Set α) →
        Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯ = t

Tactic:
_
-- 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 y : α
hy : y ∈ s
hyt : y ∈ (↑t : Set α)
h : Finite.{u_1 + 1} (↑(s ∩ (↑t : Set α)) : Type u_1)
hxs : x ∈ s
hxt : x ∈ (↑t : Set α)
left_inv :
  (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯) : Set α) =
    (↑t : Set α)
⊢ Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯ = t

Tactic:
rw [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- 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 y : α
hy : y ∈ s
hyt : y ∈ (↑t : Set α)
h : Finite.{u_1 + 1} (↑(s ∩ (↑t : Set α)) : Type u_1)
hxs : x ∈ s
hxt : x ∈ (↑t : Set α)
⊢ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯) : Set α) =
    (↑t : Set α)

Tactic:
(hP.2 x).unique (hP.2 x).exists.choose_spec ⟨t.prop, hxt⟩

Premises used: Exists.choose_spec, ExistsUnique.exists, And.right, Subtype.prop, And.intro, ExistsUnique.unique
-- 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 y : α
hy : y ∈ s
hyt : y ∈ (↑t : Set α)
h : Finite.{u_1 + 1} (↑(s ∩ (↑t : Set α)) : Type u_1)
hxs : x ∈ s
hxt : x ∈ (↑t : Set α)
⊢ (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) ⋯) : Set α) =
    (↑t : Set α)

Tactic:
exact (hP.2 x).unique (hP.2 x).exists.choose_spec ⟨t.prop, hxt⟩

Premises used: Exists.choose_spec, ExistsUnique.exists, And.right, Subtype.prop, And.intro, ExistsUnique.unique
-- 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 : α
⊢ t ∈ (↑(hs.toFinset (s := s)) : Set α) →
    (fun (x : (_ : (↑P : Type u_1)) × α) ↦
          (match (motive := (_ : (↑P : Type u_1)) × α → α) x with
            | ⟨t, x⟩ => x :
            α))
        ((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)) × α))
          t) =
      t

Tactic:
simp only [implies_true]

Premises used: implies_true
-- 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
suffices : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
⊢ s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard

Tactic:
suffices hs' : _ by
    rw [finsum_def, dif_pos hs']
    simp only [← Nat.card_coe_set_eq, Nat.card_eq_card_finite_toFinset hs]
    rw [Finset.sum_congr rfl (fun t ht ↦ by exact hst' ↑t)]
    rw [← Finset.card_sigma, eq_comm]
    apply Finset.card_nbij' (fun ⟨t, x⟩ ↦ x)
      (fun x ↦ ⟨⟨(hP.2 x).exists.choose, (hP.2 x).exists.choose_spec.1⟩, x⟩)
    · rintro ⟨t, x⟩
      simp +contextual
    · intro x
      simp only [Set.Finite.mem_toFinset, Finset.mem_sigma, Function.mem_support, Set.mem_inter_iff,
        Finset.mem_coe]
      intro hx
      refine ⟨Nat.card_ne_zero.mpr ⟨?_, hst (hP.right x).exists.choose⟩,
        hx, (hP.2 x).exists.choose_spec.2⟩
      simp only [nonempty_subtype, Set.mem_inter_iff]
      use x, hx, (hP.2 x).exists.choose_spec.2
    · rintro ⟨t, x⟩
      simp only [Finset.mem_sigma, Set.Finite.mem_toFinset, Function.mem_support, Nat.card_ne_zero,
        Set.mem_inter_iff, Sigma.mk.inj_iff, heq_eq_eq, and_true, and_imp, Finset.mem_coe]
      simp only [nonempty_subtype, Set.mem_inter_iff, forall_exists_index, and_imp]
      intro y hy hyt _ hxs hxt
      rw [← Subtype.coe_inj]
      exact (hP.2 x).unique (hP.2 x).exists.choose_spec ⟨t.prop, hxt⟩
    · intro t
      simp only [implies_true]
-- 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
f : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1) :=
  fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
    match (motive :=
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1))
      x with
    | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯
⊢ ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
    (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α)

Tactic:
have hf (t : Function.support (fun (t : P) ↦ (s ∩ (t : Set α)).ncard)) :
      ↑↑t ∈ P ∧ (f t : α) ∈ (t : Set α) :=
    ⟨(↑t : P).prop, (Set.nonempty_of_ncard_ne_zero t.prop).choose_spec.2⟩
-- 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
f : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1) :=
  fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
    match (motive :=
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1))
      x with
    | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯
hf :
  ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
    (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α)
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have : Finite ↑s := hs
-- 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
f : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1) :=
  fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
    match (motive :=
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1))
      x with
    | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯
hf :
  ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
    (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α)
this : Finite.{u_1 + 1} (↑s : Type u_1)
apply : Function.Injective f
⊢ Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard

Tactic:
apply Finite.of_injective f

Premises used: Finite.of_injective
-- 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
f : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1) :=
  fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
    match (motive :=
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1))
      x with
    | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯
hf :
  ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
    (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α)
this : Finite.{u_1 + 1} (↑s : Type u_1)
t t' : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)
h : f t = f t'
simp : (↑(↑t : (↑P : Type u_1)) : Set α) = (↑(↑t' : (↑P : Type u_1)) : Set α)
⊢ t = t'

Tactic:
simp only [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- 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
f : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1) :=
  fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
    match (motive :=
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1))
      x with
    | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯
hf :
  ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
    (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α)
this : Finite.{u_1 + 1} (↑s : Type u_1)
t t' : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)
h : f t = f t'
⊢ (↑(↑t : (↑P : Type u_1)) : Set α) = (↑(↑t' : (↑P : Type u_1)) : Set α)

Tactic:
(hP.2 (f t)).unique (hf t) (h ▸ hf t')

Premises used: Eq.rec, And.right, ExistsUnique.unique, Eq.symm, 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
f : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1) :=
  fun (x : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)) ↦
    match (motive :=
      (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1) → (↑s : Type u_1))
      x with
    | ⟨t, ht⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ s) (Exists.choose (p := Membership.mem (s ∩ (↑t : Set α))) ⋯) ⋯
hf :
  ∀ (t : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)),
    (↑(↑t : (↑P : Type u_1)) : Set α) ∈ P ∧ (↑(f t) : α) ∈ (↑(↑t : (↑P : Type u_1)) : Set α)
this : Finite.{u_1 + 1} (↑s : Type u_1)
t t' : (↑(Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) : Type u_1)
h : f t = f t'
⊢ (↑(↑t : (↑P : Type u_1)) : Set α) = (↑(↑t' : (↑P : Type u_1)) : Set α)

Tactic:
exact (hP.2 (f t)).unique (hf t) (h ▸ hf t')

Premises used: And.right, ExistsUnique.unique, Subtype.val
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
x : α
b b' : Set α
hc : b ∈ c
hb : x ∈ b
hc' : b' ∈ c
hb' : x ∈ b'
⊢ b = b'

Tactic:
(H x).unique ⟨hc, hb⟩ ⟨hc', hb'⟩

Premises used: And.intro, ExistsUnique.unique
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
x _y : α
h : ∀ s ∈ c, x ∈ s → _y ∈ s
s : Set α
hs : s ∈ c
hy : _y ∈ s
obtain :
  ∀ (t : Set α), (∀ (y : Set α), (fun (b : Set α) ↦ b ∈ c ∧ x ∈ b) y → y = t) → ∀ (ht : t ∈ c) (hx : x ∈ t), x ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨t, ⟨ht, hx⟩, _⟩ := H x
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
x _y : α
h : ∀ s ∈ c, x ∈ s → _y ∈ s
s : Set α
hs : s ∈ c
hy : _y ∈ s
t : Set α
right : ∀ (y : Set α), (fun (b : Set α) ↦ b ∈ c ∧ x ∈ b) y → y = t
ht : t ∈ c
hx rwa rwa₁ rwa₂ rwa₃ : x ∈ t
⊢ x ∈ s

Tactic:
rwa [eq_of_mem_eqv_class H hs hy ht (h t ht hx)]

Premises used: Setoid.eq_of_mem_eqv_class
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
y : α
⊢ {x : α | (r : α → α → Prop) x y} ∈ r.classes

Tactic:
⟨y, rfl⟩

Premises used: Set.Mem, setOf, Setoid.classes, Exists.intro, rfl
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ ∃ (y : β), Eq.{u_1 + 1} (α := Set α) {x : α | f x = y} {x_1 : α | (ker f : α → α → Prop) x_1 x}

Tactic:
⟨f x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ ∃ (y : β), Eq.{u_1 + 1} (α := Set α) {x : α | f x = y} {x_1 : α | (ker f : α → α → Prop) x_1 x}

Tactic:
exact ⟨f x, rfl⟩
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_2
β : Type u_3
inst : Finite β
f : α → β
⊢ (ker f).classes.Finite

Tactic:
(Set.finite_range _).subset <| classes_ker_subset_fiber_set f

Premises used: Setoid.classes_ker_subset_fiber_set, Set.finite_range, Set.Finite.subset
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_2
β : Type u_3
inst : Fintype β
f : α → β
inst_1 : Fintype (↑(ker f).classes : Type u_2)
⊢ Fintype.card.{u_2} (↑(ker f).classes : Type u_2) ≤ Fintype.card β

Tactic:
le_trans (Set.card_le_card (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)

Premises used: Fintype.card_range_le, Setoid.classes_ker_subset_fiber_set, Set.card_le_card, le_trans
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_2
β : Type u_3
inst : Fintype β
f : α → β
inst_1 : Fintype (↑(ker f).classes : Type u_2)
⊢ Fintype.card.{u_2} (↑(ker f).classes : Type u_2) ≤ Fintype.card β

Tactic:
exact
      le_trans (Set.card_le_card (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)

Premises used: Fintype.card_range_le, Setoid.classes_ker_subset_fiber_set, Set.card_le_card, le_trans
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_2
β : Type u_3
inst : Fintype β
f : α → β
inst_1 : Fintype (↑(ker f).classes : Type u_2)
⊢ Fintype.card.{u_2} (↑(ker f).classes : Type u_2) ≤ Fintype.card β

Tactic:
classical exact
      le_trans (Set.card_le_card (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)

Premises used: Fintype.card_range_le, Setoid.classes_ker_subset_fiber_set, Set.card_le_card, le_trans
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r₁ r₂ : Setoid α
⊢ r₁ = r₂ ↔ ∀ (x : α), Eq.{u_1 + 1} (α := Set α) {y : α | (r₁ : α → α → Prop) x y} {y : α | (r₂ : α → α → Prop) x y}

Tactic:
⟨fun h _x => h ▸ rfl, fun h => ext fun x => Set.ext_iff.1 <| h x⟩

Premises used: Eq.rec, Setoid.ext, Iff.intro, Iff.mp, Set.ext_iff, rfl
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
x y : α
h : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
c : Set α
z : α
hz : c = {x : α | (r : α → α → Prop) x z}
hx : x ∈ c
hy : y ∈ c
⊢ Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x z} x

Tactic:
subst c
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
x y : α
h : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
c : Set α
z : α
hz : c = {x : α | (r : α → α → Prop) x z}
hx : x ∈ c
hy : y ∈ c
hx₁ : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x z} x
⊢ Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x z} y

Tactic:
subst c
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
x y : α
h : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
z : α
hx : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x z} x
hy : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x z} y
⊢ (r : α → α → Prop) x y

Tactic:
r.trans' hx (r.symm' hy)

Premises used: Setoid.trans', Setoid.symm'
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
x y : α
h : ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c
z : α
hx : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x z} x
hy : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x z} y
⊢ (r : α → α → Prop) x y

Tactic:
exact r.trans' hx (r.symm' hy)

Premises used: Setoid.trans', Setoid.symm'
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r₁ r₂ : Setoid α
h : r₁.classes = r₂.classes
a b : α
⊢ (r₁ : α → α → Prop) a b ↔ (r₂ : α → α → Prop) a b

Tactic:
simp only [rel_iff_exists_classes, h]

Premises used: Setoid.rel_iff_exists_classes
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
⊢ ∅ ∉ r.classes

Tactic:
fun ⟨y, hy⟩ =>
  Set.notMem_empty y <| hy.symm ▸ r.refl' y

Premises used: False, Setoid.refl', Eq.rec, Set.notMem_empty, _private.0.Setoid.empty_notMem_classes.match_1, Eq.symm, Not
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
a w : α
ha : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x w} a
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x w} x ↔
      Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x a} x
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | (r : α → α → Prop) x w} {x : α | (r : α → α → Prop) x a}

Tactic:
ext x