awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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
⊢ 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)
have 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)) sorry,
    (Set.Finite.toFinset (s := s ∩ (↑t : Set α)) sorry).card
Tactic: rw [Finset.sum_congr rfl (fun t ht ↦ by exact hst' ↑t)]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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
⊢ 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
have 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))
          sorry).sigma
      (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦ Set.Finite.toFinset (s := s ∩ (↑t : Set α)) sorry) =
  hs.toFinset (s := s).card
Tactic: rw [← Finset.card_sigma, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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
⊢ 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
have 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))
            sorry).sigma
        (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦
        Set.Finite.toFinset (s := s ∩ (↑t : Set α)) sorry) :
    Set ((_ : (↑P : Type u_1)) × α))
  (↑(hs.toFinset (s := s)) : Set α)
Tactic: apply Finset.card_nbij' (fun ⟨t, x⟩ ↦ x)
      (fun x ↦ ⟨⟨(hP.2 x).exists.choose, (hP.2 x).exists.choose_spec.1⟩, x⟩)
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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 α)
⊢ 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
have hj : Set.MapsTo
  (fun (x : α) ↦
    Sigma.mk (β := fun (i : (↑P : Type u_1)) ↦ α)
      (Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (sorry.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) sorry) 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))
            sorry).sigma
        (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦
        Set.Finite.toFinset (s := s ∩ (↑t : Set α)) sorry) :
    Set ((_ : (↑P : Type u_1)) × α))
Tactic: apply Finset.card_nbij' (fun ⟨t, x⟩ ↦ x)
      (fun x ↦ ⟨⟨(hP.2 x).exists.choose, (hP.2 x).exists.choose_spec.1⟩, x⟩)
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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)) × α))
⊢ 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
have left_inv : Set.LeftInvOn
  (fun (x : α) ↦
    Sigma.mk (β := fun (i : (↑P : Type u_1)) ↦ α)
      (Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (sorry.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) sorry) 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))
            sorry).sigma
        (α := fun (a : (↑P : Type u_1)) ↦ α) fun (t : (↑P : Type u_1)) ↦
        Set.Finite.toFinset (s := s ∩ (↑t : Set α)) sorry) :
    Set ((_ : (↑P : Type u_1)) × α))
Tactic: apply Finset.card_nbij' (fun ⟨t, x⟩ ↦ x)
      (fun x ↦ ⟨⟨(hP.2 x).exists.choose, (hP.2 x).exists.choose_spec.1⟩, x⟩)
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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)) × α))
⊢ 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
have right_inv : Set.RightInvOn
  (fun (x : α) ↦
    Sigma.mk (β := fun (i : (↑P : Type u_1)) ↦ α)
      (Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (sorry.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) sorry) x)
  (fun (x : (_ : (↑P : Type u_1)) × α) ↦
    match (motive := (_ : (↑P : Type u_1)) × α → α) x with
    | ⟨t, x⟩ => x)
  (↑(hs.toFinset (s := s)) : Set α)
Tactic: apply Finset.card_nbij' (fun ⟨t, x⟩ ↦ x)
      (fun x ↦ ⟨⟨(hP.2 x).exists.choose, (hP.2 x).exists.choose_spec.1⟩, x⟩)
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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 : α
⊢ 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)) × α))
have hj : x ∈ s →
  Nat.card.{u_1} (↑(s ∩ sorry.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) : Type u_1) ≠ 0 ∧
    x ∈ s ∧ x ∈ sorry.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)
Tactic: simp only [Set.Finite.mem_toFinset, Finset.mem_sigma, Function.mem_support, Set.mem_inter_iff,
        Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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)
have hj : Nonempty.{u_1 + 1} (↑(s ∩ sorry.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) : Type u_1)
Tactic: refine ⟨Nat.card_ne_zero.mpr ⟨?_, hst (hP.right x).exists.choose⟩,
        hx, (hP.2 x).exists.choose_spec.2⟩
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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
⊢ Nonempty.{u_1 + 1} (↑(s ∩ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) : Type u_1)
have hj : ∃ a ∈ s, a ∈ sorry.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)
Tactic: simp only [nonempty_subtype, Set.mem_inter_iff]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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
⊢ ∃ a ∈ s, a ∈ ⋯.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)
have right : x ∈ sorry.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)
Tactic: use x, hx, (hP.2 x).exists.choose_spec.2
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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)) × α)) →
    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)
have 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) (sorry.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) sorry = t
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]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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 : α
⊢ 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
have 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) (sorry.choose (p := fun (x_2 : Set α) ↦ x_2 ∈ P ∧ x ∈ x_2)) sorry = t
Tactic: simp only [nonempty_subtype, Set.mem_inter_iff, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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)) ⋯ = t
have left_inv : (↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ P) (sorry.choose (p := fun (x_1 : Set α) ↦ x_1 ∈ P ∧ x ∈ x_1)) sorry) : Set α) =
  (↑t : Set α)
Tactic: rw [← Subtype.coe_inj]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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
⊢ s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
have suffices : Function.HasFiniteSupport (M := ℕ) fun (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]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (hypothesis)
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 α))) ⋯) ⋯
⊢ Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
have 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 α)
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⟩
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (hypothesis)
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 α)
⊢ Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
have this : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: have : Finite ↑s := hs
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
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)
⊢ Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
have apply : Function.Injective f
Tactic: apply Finite.of_injective f