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
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 = t'
have simp : (↑(↑t : (↑P : Type u_1)) : Set α) = (↑(↑t' : (↑P : Type u_1)) : Set α)
Tactic: simp only [← 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
⊢ s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
have have : ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite), s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
Tactic: classical
  have hst (t : Set α) : (s ∩ t).Finite := hs.inter_of_left t
  have hst' (t : Set α) : Nat.card ↑(s ∩ t) = (hst t).toFinset.card :=
    Nat.card_eq_card_finite_toFinset (hst t)
  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]
  let f : Function.support (fun (t : P) ↦ (s ∩ (t : Set α)).ncard) → s := fun ⟨t, ht⟩ ↦
    ⟨(Set.nonempty_of_ncard_ne_zero ht).choose, (Set.nonempty_of_ncard_ne_zero ht).choose_spec.1⟩
  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⟩
  have : Finite ↑s := hs
  apply Finite.of_injective f
  intro t t' h
  simp only [← Subtype.coe_inj]
  exact (hP.2 (f t)).unique (hf t) (h ▸ hf 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
have have₁ have₂ : ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite), s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
⊢ s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
have have₃ : ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite)
  (hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = sorry.toFinset (s := s ∩ t).card),
  s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
Tactic: classical
  have hst (t : Set α) : (s ∩ t).Finite := hs.inter_of_left t
  have hst' (t : Set α) : Nat.card ↑(s ∩ t) = (hst t).toFinset.card :=
    Nat.card_eq_card_finite_toFinset (hst t)
  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]
  let f : Function.support (fun (t : P) ↦ (s ∩ (t : Set α)).ncard) → s := fun ⟨t, ht⟩ ↦
    ⟨(Set.nonempty_of_ncard_ne_zero ht).choose, (Set.nonempty_of_ncard_ne_zero ht).choose_spec.1⟩
  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⟩
  have : Finite ↑s := hs
  apply Finite.of_injective f
  intro t t' h
  simp only [← Subtype.coe_inj]
  exact (hP.2 (f t)).unique (hf t) (h ▸ hf 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
have have₁ have₂ : ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite), s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
have₃ :
  ∀ (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
⊢ s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
have have₄ : ∀ (hst : ∀ (t : Set α), (s ∩ t).Finite)
  (hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = sorry.toFinset (s := s ∩ t).card),
  Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
Tactic: classical
  have hst (t : Set α) : (s ∩ t).Finite := hs.inter_of_left t
  have hst' (t : Set α) : Nat.card ↑(s ∩ t) = (hst t).toFinset.card :=
    Nat.card_eq_card_finite_toFinset (hst t)
  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]
  let f : Function.support (fun (t : P) ↦ (s ∩ (t : Set α)).ncard) → s := fun ⟨t, ht⟩ ↦
    ⟨(Set.nonempty_of_ncard_ne_zero ht).choose, (Set.nonempty_of_ncard_ne_zero ht).choose_spec.1⟩
  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⟩
  have : Finite ↑s := hs
  apply Finite.of_injective f
  intro t t' h
  simp only [← Subtype.coe_inj]
  exact (hP.2 (f t)).unique (hf t) (h ▸ hf t')
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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
⊢ x ∈ s
have obtain : ∀ (t : Set α), (∀ (y : Set α), (fun (b : Set α) ↦ b ∈ c ∧ x ∈ b) y → y = t) → ∀ (ht : t ∈ c) (hx : x ∈ t), x ∈ s
Tactic: obtain ⟨t, ⟨ht, hx⟩, _⟩ := H x
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (hypothesis)
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
⊢ (r : α → α → Prop) x y
have hx₁ : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x z} x
Tactic: subst c
Cleared hypotheses: c, hz, hx, hy
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (hypothesis)
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
⊢ (r : α → α → Prop) x y
have hy₁ : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x z} y
Tactic: subst c
Cleared hypotheses: c, hz, hx, hy
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
a w : α
ha : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x w} a
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | (r : α → α → Prop) x w} {x : α | (r : α → α → Prop) x a}
have h : ∀ (x : α),
  Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x w} x ↔
    Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x a} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
⊢ s = {x : α | (mkClasses c H : α → α → Prop) x y}
have h : ∀ (x : α), x ∈ s ↔ Membership.mem (γ := Set α) {x : α | (mkClasses c H : α → α → Prop) x y} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s ↔ Membership.mem (γ := Set α) {x : α | (mkClasses c H : α → α → Prop) x y} x
have h : x ∈ s → Membership.mem (γ := Set α) {x : α | (mkClasses c H : α → α → Prop) x y} x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
h : x ∈ s → Membership.mem (γ := Set α) {x : α | (mkClasses c H : α → α → Prop) x y} x
⊢ x ∈ s ↔ Membership.mem (γ := Set α) {x : α | (mkClasses c H : α → α → Prop) x y} x
have h₁ : Membership.mem (γ := Set α) {x : α | (mkClasses c H : α → α → Prop) x y} x → x ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : Membership.mem (γ := Set α) {x : α | (mkClasses c H : α → α → Prop) x y} x
⊢ x ∈ s
have h : ∀ (b' : Set α), (∀ (y : Set α), (fun (b : Set α) ↦ b ∈ c ∧ x ∈ b) y → y = b') → ∀ (hc : b' ∈ c) (hb' : x ∈ b'), x ∈ s
Tactic: obtain ⟨b', ⟨hc, hb'⟩, _⟩ := H x
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
x : α
⊢ {y : α | (mkClasses c H : α → α → Prop) x y} ∈ c
have h : ∀ (x_1 : α), (mkClasses c H : α → α → Prop) x x_1 ↔ (mkClasses c H : α → α → Prop) x_1 x
Tactic: convert! @Setoid.eqv_class_mem _ _ H x using 3
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
x x_1 : α
⊢ (mkClasses c H : α → α → Prop) x x_1 ↔ (mkClasses c H : α → α → Prop) x_1 x
have h : (mkClasses c H : α → α → Prop) x_1 x ↔ (mkClasses c H : α → α → Prop) x_1 x
Tactic: rw [Setoid.comm']
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : c.PairwiseDisjoint id
a : α
⊢ a ∈ ⋃₀ c
have rw : Membership.mem (γ := Set α) Set.univ a
Tactic: rw [hu]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
a b : α
a_rel_b : (r : α → α → Prop) a b
⊢ f a = f b
have rw : Eq.{u_1 + 1} (α := Set α) {x : α | (r : α → α → Prop) x a} {x : α | (r : α → α → Prop) x b}
Tactic: rw [Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (hypothesis)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
⊢ Quotient r ≃ (↑r.classes : Type u_1)
have f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
Tactic: have f_respects_relation (a b : α) (a_rel_b : r a b) : f a = f b := by
    rw [Subtype.mk.injEq]
    exact Setoid.eq_of_mem_classes (Setoid.mem_classes r a) (Setoid.symm a_rel_b)
        (Setoid.mem_classes r b) (Setoid.refl b)
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
⊢ Quotient r ≃ (↑r.classes : Type u_1)
have apply : Function.Bijective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)
Tactic: apply Equiv.ofBijective (Quot.lift f f_respects_relation)
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
⊢ Function.Bijective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)
have left : Function.Injective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
left : Function.Injective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)
⊢ Function.Bijective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)
have right : Function.Surjective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
q_a : Quotient r
⊢ ∀ ⦃a₂ : Quot (α := α) (⇑r : α → α → Prop)⦄,
    Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation q_a =
        Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation a₂ →
      q_a = a₂
have left : ∀ ⦃q_b : Quotient r⦄,
  Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation q_a =
      Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation q_b →
    q_a = q_b
Tactic: (q_b : Quotient r)
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
q_a q_b : Quotient r
h_eq :
  Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation q_a =
    Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation q_b
⊢ q_a = q_b
have left : ∀ (a : α)
  (h_eq :
    Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation ⟦a⟧ =
      Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation q_b),
  ⟦a⟧ = q_b
Tactic: induction q_a using Quotient.ind with | _ a
Cleared hypotheses: q_a, h_eq
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
q_b : Quotient r
a : α
h_eq :
  Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation ⟦a⟧ =
    Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation q_b
⊢ ⟦a⟧ = q_b
have left : ∀ (b : α)
  (h_eq :
    Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation ⟦a⟧ =
      Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation ⟦b⟧),
  ⟦a⟧ = ⟦b⟧
Tactic: induction q_b using Quotient.ind with | _ b
Cleared hypotheses: q_b, h_eq
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (hypothesis)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
a b : α
h_eq :
  Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation ⟦a⟧ =
    Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation ⟦b⟧
⊢ ⟦a⟧ = ⟦b⟧
have h_eq₁ : Eq.{u_1 + 1} (α := Set α) {x : α | (r : α → α → Prop) x a} {x : α | (r : α → α → Prop) x b}
Tactic: simp only [f, Quotient.lift_mk, Subtype.ext_iff] at h_eq
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
a b : α
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | (r : α → α → Prop) x a} {x : α | (r : α → α → Prop) x b}
⊢ ⟦a⟧ = ⟦b⟧
have left : a ≈ b
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
a b : α
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | (r : α → α → Prop) x a} {x : α | (r : α → α → Prop) x b}
⊢ a ≈ b
have left : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x b} a
Tactic: change a ∈ { x | r x b }
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
a b : α
h_eq : Eq.{u_1 + 1} (α := Set α) {x : α | (r : α → α → Prop) x a} {x : α | (r : α → α → Prop) x b}
⊢ Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x b} a
have left : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x a} a
Tactic: rw [← h_eq]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r : Setoid α
f : (a : α) → (↑r.classes : Type u_1) :=
  fun (a : α) ↦ Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) {x : α | (r : α → α → Prop) x a} ⋯
f_respects_relation : ∀ (a b : α) (a_rel_b : (r : α → α → Prop) a b), f a = f b
⊢ Function.Surjective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)
have right : Function.Surjective f
Tactic: rw [Quot.surjective_lift]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
⊢ IsPartition s
have refine : ∀ (a : α) (y₁ y₂ : Set α), y₁ ∈ s ∧ a ∈ y₁ → y₂ ∈ s ∧ a ∈ y₂ → y₁ = y₂
Tactic: refine ⟨h₃, fun a ↦ existsUnique_of_exists_of_unique (h₂ a) ?_⟩
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ b₁ = b₂
have apply : ¬Disjoint (id b₁) (id b₂)
Tactic: apply h₁.elim hb₁.1 hb₂.1
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
a : α
b₁ b₂ : Set α
hb₁ : b₁ ∈ s ∧ a ∈ b₁
hb₂ : b₂ ∈ s ∧ a ∈ b₂
⊢ ¬Disjoint (id b₁) (id b₂)
have simp : ∃ x ∈ id b₁, x ∈ id b₂
Tactic: simp only [Set.not_disjoint_iff]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (t ∈ c ∧ x ∈ t) ∧ ∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t
⊢ t ∈ c ∧ x ∈ t
have tauto : (∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t) → t ∈ c → x ∈ t → t ∈ c ∧ x ∈ t
Tactic: tauto
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (t ∈ c ∧ x ∈ t) ∧ ∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t
tauto tauto₁ : (∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t) → t ∈ c → x ∈ t → t ∈ c ∧ x ∈ t
⊢ t ∈ c ∧ x ∈ t
have left : (∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t) → t ∈ c → x ∈ t → t ∈ c
Tactic: tauto
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (t ∈ c ∧ x ∈ t) ∧ ∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t
tauto tauto₁ : (∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t) → t ∈ c → x ∈ t → t ∈ c ∧ x ∈ t
left : (∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t) → t ∈ c → x ∈ t → t ∈ c
⊢ t ∈ c ∧ x ∈ t
have right : (∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t) → t ∈ c → x ∈ t → x ∈ t
Tactic: tauto
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
⊢ (mkClasses c ⋯).classes = c
have h : ∀ (s : Set α), s ∈ (mkClasses c sorry).classes ↔ s ∈ c
Tactic: ext s
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ (mkClasses c ⋯).classes ↔ s ∈ c
have h : s ∈ (mkClasses c sorry).classes → s ∈ c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
h : s ∈ (mkClasses c ⋯).classes → s ∈ c
⊢ s ∈ (mkClasses c ⋯).classes ↔ s ∈ c
have h₁ : s ∈ c → s ∈ (mkClasses c sorry).classes
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
⊢ {x : α | (mkClasses c ⋯ : α → α → Prop) x y} ∈ c
have h : ∀ (b : Set α),
  (∀ (y_1 : Set α), (fun (b : Set α) ↦ b ∈ c ∧ y ∈ b) y_1 → y_1 = b) →
    ∀ (hb : b ∈ c) (hy : y ∈ b), {x : α | (mkClasses c sorry : α → α → Prop) x y} ∈ c
Tactic: obtain ⟨b, ⟨hb, hy⟩, _⟩ := hc.2 y
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
x y : Partitions α
hx : x ≤ y
hy : y ≤ x
h : mkClasses x.toSet ⋯ = mkClasses y.toSet ⋯ := ⋯
⊢ x = y
have rw : x.toSet = y.toSet
Tactic: rw [Partitions.ext_iff, ← classes_mkClasses x.toSet x.isPartition,
      ← classes_mkClasses y.toSet y.isPartition, h]