awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
a w : α
ha : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x w} a
x : α
⊢ Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x w} x ↔
    Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x a} x

Tactic:
⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩

Premises used: Setoid.trans', Setoid.symm', Iff.intro
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
a w : α
ha : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x w} a
x : α
⊢ Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x w} x ↔
    Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x a} x

Tactic:
exact ⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
x : α
b : Set α
hc : b ∈ r.classes
hb : x ∈ b
b' : Set α
hc' : b' ∈ r.classes
hb' : x ∈ b'
⊢ b = b'

Tactic:
eq_of_mem_eqv_class classes_eqv_classes hc hb hc' hb'

Premises used: Setoid.classes_eqv_classes, Setoid.eq_of_mem_eqv_class
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
h : ∀ (x : α), x ∈ s ↔ Membership.mem (γ := Set α) {x : α | (mkClasses c H : α → α → Prop) x y} x
⊢ s = {x : α | (mkClasses c H : α → α → Prop) x y}

Tactic:
ext x
-- Module: Mathlib.Data.Setoid.Partition
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
h₁ : Membership.mem (γ := Set α) {x : α | (mkClasses c H : α → α → Prop) x y} x → x ∈ s
⊢ x ∈ s ↔ Membership.mem (γ := Set α) {x : α | (mkClasses c H : α → α → Prop) x y} x

Tactic:
constructor
-- Module: Mathlib.Data.Setoid.Partition
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 : x ∈ s
_s' : Set α
hs' : _s' ∈ c
hx' : x ∈ _s'
h h₁ h₂ h₃ : y ∈ s
⊢ y ∈ _s'

Tactic:
rwa [eq_of_mem_eqv_class H hs' hx' hs hx]

Premises used: Setoid.eq_of_mem_eqv_class
-- Module: Mathlib.Data.Setoid.Partition
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
h :
  ∀ (b' : Set α), (∀ (y : Set α), (fun (b : Set α) ↦ b ∈ c ∧ x ∈ b) y → y = b') → ∀ (hc : b' ∈ c) (hb' : x ∈ b'), x ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨b', ⟨hc, hb'⟩, _⟩ := H x
-- Module: Mathlib.Data.Setoid.Partition
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
b' : Set α
right : ∀ (y : Set α), (fun (b : Set α) ↦ b ∈ c ∧ x ∈ b) y → y = b'
hc : b' ∈ c
hb' h h₁ h₂ h₃ : x ∈ b'
⊢ x ∈ s

Tactic:
rwa [eq_of_mem_eqv_class H hs hy hc (hx b' hc hb')]

Premises used: Setoid.eq_of_mem_eqv_class
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
y : α
⊢ {x : α | (mkClasses c H : α → α → Prop) x y} ∈ c

Tactic:
(H y).elim fun _ hc _ => eq_eqv_class_of_mem H hc.1 hc.2 ▸ hc.1

Premises used: ExistsUnique.elim, Eq.rec, And.right, And.left, Setoid.eq_eqv_class_of_mem
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
x : α
⊢ {x_1 : α | (mkClasses c H : α → α → Prop) x_1 x} ∈ c

Tactic:
@Setoid.eqv_class_mem _ _ H x

Premises used: Setoid.eqv_class_mem
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
x : α
h : ∀ (x_1 : α), (mkClasses c H : α → α → Prop) x x_1 ↔ (mkClasses c H : α → α → Prop) x_1 x
⊢ {y : α | (mkClasses c H : α → α → Prop) x y} ∈ c

Tactic:
convert! @Setoid.eqv_class_mem _ _ H x using 3

Premises used: Setoid.eqv_class_mem
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
x x_1 : α
h h₁ : (mkClasses c H : α → α → Prop) x_1 x ↔ (mkClasses c H : α → α → Prop) x_1 x
⊢ (mkClasses c H : α → α → Prop) x x_1 ↔ (mkClasses c H : α → α → Prop) x_1 x

Tactic:
rw [Setoid.comm']

Premises used: Setoid.comm'
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b : Set α, b ∈ c ∧ a ∈ b
⊢ c.PairwiseDisjoint id

Tactic:
fun _b₁ h₁ _b₂ h₂ h =>
  Set.disjoint_left.2 fun x hx1 hx2 =>
    (H x).elim fun _b _hc _hx => h <| eq_of_mem_eqv_class H h₁ hx1 h₂ hx2

Premises used: Iff.mpr, ExistsUnique.elim, Set.disjoint_left, Set.PairwiseDisjoint, Set.Pairwise, Setoid.eq_of_mem_eqv_class
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : c.PairwiseDisjoint id
a : α
rw : Membership.mem (γ := Set α) Set.univ a
⊢ a ∈ ⋃₀ c

Tactic:
rw [hu]
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : c.PairwiseDisjoint id
a : α
⊢ Membership.mem (γ := Set α) Set.univ a

Tactic:
Set.mem_univ a

Premises used: Set.mem_univ
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : c.PairwiseDisjoint id
a : α
⊢ Membership.mem (γ := Set α) Set.univ a

Tactic:
exact Set.mem_univ a

Premises used: Set.mem_univ
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
⊢ mkClasses r.classes ⋯ = r

Tactic:
ext fun x _y =>
    ⟨fun h => r.symm' (h { z | r z x } (r.mem_classes x) <| r.refl' x), fun h _b hb hx =>
      eq_of_mem_classes (r.mem_classes x) (r.refl' x) hb hx ▸ r.symm' h⟩

Premises used: Setoid.refl', setOf, Eq.rec, Setoid.symm', Setoid.ext, Iff.intro, Setoid.eq_of_mem_classes, Setoid.r, Setoid.mem_classes
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
⊢ ⋃₀ r.classes = Set.univ

Tactic:
Set.eq_univ_of_forall fun x => Set.mem_sUnion.2 ⟨{ y | r y x }, ⟨x, rfl⟩, Setoid.refl _⟩

Premises used: Iff.mpr, setOf, Set.eq_univ_of_forall, And.intro, Exists.intro, Setoid.refl, Set.mem_sUnion, rfl, Setoid.r
-- Module: Mathlib.Data.Setoid.Partition
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
rw : Eq.{u_1 + 1} (α := Set α) {x : α | (r : α → α → Prop) x a} {x : α | (r : α → α → Prop) x b}
⊢ f a = f b

Tactic:
rw [Subtype.mk.injEq]

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Data.Setoid.Partition
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
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | (r : α → α → Prop) x a} {x : α | (r : α → α → Prop) x b}

Tactic:
Setoid.eq_of_mem_classes (Setoid.mem_classes r a) (Setoid.symm a_rel_b)
        (Setoid.mem_classes r b) (Setoid.refl b)

Premises used: Setoid.symm, Setoid.eq_of_mem_classes, Setoid.refl, Setoid.mem_classes
-- Module: Mathlib.Data.Setoid.Partition
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
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | (r : α → α → Prop) x a} {x : α | (r : α → α → Prop) x b}

Tactic:
exact Setoid.eq_of_mem_classes (Setoid.mem_classes r a) (Setoid.symm a_rel_b)
        (Setoid.mem_classes r b) (Setoid.refl b)

Premises used: Setoid.symm, Setoid.eq_of_mem_classes, Setoid.refl, Setoid.mem_classes
-- Module: Mathlib.Data.Setoid.Partition
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

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)
-- Module: Mathlib.Data.Setoid.Partition
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
apply : Function.Bijective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)
⊢ Quotient r ≃ (↑r.classes : Type u_1)

Tactic:
apply Equiv.ofBijective (Quot.lift f f_respects_relation)

Premises used: Quot.lift, Equiv.ofBijective
-- Module: Mathlib.Data.Setoid.Partition
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)
right : Function.Surjective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)
⊢ Function.Bijective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)

Tactic:
constructor
-- Module: Mathlib.Data.Setoid.Partition
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
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
⊢ ∀ ⦃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₂

Tactic:
(q_b : Quotient r)
-- Module: Mathlib.Data.Setoid.Partition
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
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
⊢ q_a = q_b

Tactic:
induction q_a using Quotient.ind with | _ a

Premises used: Quotient.ind
-- Module: Mathlib.Data.Setoid.Partition
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
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⟧
⊢ ⟦a⟧ = q_b

Tactic:
induction q_b using Quotient.ind with | _ b

Premises used: Quotient.ind
-- Module: Mathlib.Data.Setoid.Partition
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⟧
⊢ 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

Premises used: Quotient.lift_mk, Subtype.ext_iff
-- Module: Mathlib.Data.Setoid.Partition
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}
left : a ≈ b
⊢ ⟦a⟧ = ⟦b⟧

Tactic:
apply Quotient.sound

Premises used: Quotient.sound
-- Module: Mathlib.Data.Setoid.Partition
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}
left : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x b} a
⊢ a ≈ b

Tactic:
change a ∈ { x | r x b }
-- Module: Mathlib.Data.Setoid.Partition
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}
left : Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x a} a
⊢ Membership.mem (γ := Set α) {x : α | (r : α → α → Prop) x b} a

Tactic:
rw [← h_eq]
-- Module: Mathlib.Data.Setoid.Partition
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 a} a

Tactic:
Setoid.refl a

Premises used: Set.Mem, setOf, Setoid.refl
-- Module: Mathlib.Data.Setoid.Partition
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 a} a

Tactic:
exact Setoid.refl a

Premises used: Setoid.refl
-- Module: Mathlib.Data.Setoid.Partition
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
right : Function.Surjective f
⊢ Function.Surjective (Quot.lift (r := (⇑r : α → α → Prop)) f f_respects_relation)

Tactic:
rw [Quot.surjective_lift]

Premises used: Quot.surjective_lift
-- Module: Mathlib.Data.Setoid.Partition
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
c : Set α
a : α
hc : c = {x : α | (r : α → α → Prop) x a}
⊢ ∃ (a_1 : α), f a_1 = Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) c ⋯

Tactic:
⟨a, Subtype.ext hc.symm⟩

Premises used: Exists.intro, Eq.symm, Subtype.ext
-- Module: Mathlib.Data.Setoid.Partition
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
c : Set α
a : α
hc : c = {x : α | (r : α → α → Prop) x a}
⊢ ∃ (a_1 : α), f a_1 = Subtype.mk (p := fun (x : Set α) ↦ x ∈ r.classes) c ⋯

Tactic:
exact ⟨a, Subtype.ext hc.symm⟩
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
a : α
⊢ Eq.{u_1 + 1} (α := Set α) (↑((r.quotientEquivClasses : (a : Quotient r) → (↑r.classes : Type u_1)) ⟦a⟧) : Set α)
    {x : α | (r : α → α → Prop) x a}

Tactic:
(@Subtype.ext_iff _ _ _ ⟨{ x | r x a }, Setoid.mem_classes r a⟩).mp rfl

Premises used: setOf, Subtype.ext_iff, Iff.mp, rfl
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
h : s ∈ c
⊢ s.Nonempty

Tactic:
Set.nonempty_iff_ne_empty.2 fun hs0 => hc.1 <| hs0 ▸ h

Premises used: Iff.mpr, Eq.rec, And.left, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r : Setoid α
⊢ IsPartition r.classes

Tactic:
⟨empty_notMem_classes, classes_eqv_classes⟩

Premises used: Setoid.classes_eqv_classes, Setoid.empty_notMem_classes, Setoid.IsPartition, And.intro
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
⊢ c.PairwiseDisjoint id

Tactic:
eqv_classes_disjoint hc.2

Premises used: Setoid.eqv_classes_disjoint, And.right
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
⊢ IsPartition s

Tactic:
⟨h₃, fun a ↦ existsUnique_of_exists_of_unique (h₂ a) ?_⟩

Premises used: existsUnique_of_exists_of_unique, Setoid.IsPartition, And.intro
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_2
s : Set (Set α)
h₁ : s.PairwiseDisjoint id
h₂ : ∀ (a : α), ∃ x ∈ s, a ∈ x
h₃ : ∅ ∉ s
refine : ∀ (a : α) (y₁ y₂ : Set α), y₁ ∈ s ∧ a ∈ y₁ → y₂ ∈ s ∧ a ∈ y₂ → y₁ = y₂
⊢ IsPartition s

Tactic:
refine ⟨h₃, fun a ↦ existsUnique_of_exists_of_unique (h₂ a) ?_⟩
-- Module: Mathlib.Data.Setoid.Partition
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₂
apply : ¬Disjoint (id b₁) (id b₂)
⊢ b₁ = b₂

Tactic:
apply h₁.elim hb₁.1 hb₂.1

Premises used: And.left, Set.PairwiseDisjoint.elim
-- Module: Mathlib.Data.Setoid.Partition
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₂
simp : ∃ x ∈ id b₁, x ∈ id b₂
⊢ ¬Disjoint (id b₁) (id b₂)

Tactic:
simp only [Set.not_disjoint_iff]

Premises used: Set.not_disjoint_iff
-- Module: Mathlib.Data.Setoid.Partition
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₂
⊢ ∃ x ∈ id b₁, x ∈ id b₂

Tactic:
⟨a, hb₁.2, hb₂.2⟩

Premises used: And.right, And.intro, Exists.intro
-- Module: Mathlib.Data.Setoid.Partition
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₂
⊢ ∃ x ∈ id b₁, x ∈ id b₂

Tactic:
exact ⟨a, hb₁.2, hb₂.2⟩
-- Module: Mathlib.Data.Setoid.Partition
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
right : (∀ (y : Set α), y ∈ c ∧ x ∈ y → y = t) → t ∈ c → x ∈ t → x ∈ t
⊢ t ∈ c ∧ x ∈ t

Tactic:
tauto
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
hs : s ∈ c
⊢ ∃ (y : α), s = {x : α | (mkClasses c ⋯ : α → α → Prop) x y}

Tactic:
let ⟨y, hy⟩ := nonempty_of_mem_partition hc hs
  ⟨y, eq_eqv_class_of_mem hc.2 hs hy⟩

Premises used: setOf, Exists, _private.0.Setoid.exists_of_mem_partition.match_1, And.right, Exists.intro, Setoid.nonempty_of_mem_partition, Setoid.eq_eqv_class_of_mem, Eq, Setoid.r
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
h : ∀ (s : Set α), s ∈ (mkClasses c ⋯).classes ↔ s ∈ c
⊢ (mkClasses c ⋯).classes = c

Tactic:
ext s
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
h : s ∈ (mkClasses c ⋯).classes → s ∈ c
h₁ : s ∈ c → s ∈ (mkClasses c ⋯).classes
⊢ s ∈ (mkClasses c ⋯).classes ↔ s ∈ c

Tactic:
constructor
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
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 ⋯ : α → α → Prop) x y} ∈ c
⊢ {x : α | (mkClasses c ⋯ : α → α → Prop) x y} ∈ c

Tactic:
obtain ⟨b, ⟨hb, hy⟩, _⟩ := hc.2 y

Premises used: And.right
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
b : Set α
right : ∀ (y_1 : Set α), (fun (b : Set α) ↦ b ∈ c ∧ y ∈ b) y_1 → y_1 = b
hb : b ∈ c
hy : y ∈ b
h h₁ h₂ h₃ : b ∈ c
⊢ {x : α | (mkClasses c ⋯ : α → α → Prop) x y} ∈ c

Tactic:
rwa [← eq_eqv_class_of_mem _ hb hy]

Premises used: Setoid.eq_eqv_class_of_mem
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ c → s ∈ (mkClasses c ⋯).classes

Tactic:
exists_of_mem_partition hc

Premises used: Set.Mem, setOf, Setoid.classes, Setoid.exists_of_mem_partition
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ c → s ∈ (mkClasses c ⋯).classes

Tactic:
exact exists_of_mem_partition hc

Premises used: Setoid.exists_of_mem_partition
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
p q : Partitions α
⊢ p = q ↔ p.toSet = q.toSet

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff, Setoid.Partitions.toSet, Setoid.Partitions
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
p : Partitions α
⊢ IsPartition p.toSet

Tactic:
p.2

Premises used: Setoid.Partitions.toSet, Subtype.property
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
x y : Partitions α
hx : x ≤ y
hy : y ≤ x
h : mkClasses x.toSet ⋯ = mkClasses y.toSet ⋯ := ⋯
rw : x.toSet = y.toSet
rw₁ : (mkClasses x.toSet ⋯).classes = y.toSet
rw₂ : (mkClasses x.toSet ⋯).classes = (mkClasses y.toSet ⋯).classes
rw₃ rw₄ : (mkClasses y.toSet ⋯).classes = (mkClasses y.toSet ⋯).classes
⊢ x = y

Tactic:
rw [Partitions.ext_iff, ← classes_mkClasses x.toSet x.isPartition,
      ← classes_mkClasses y.toSet y.isPartition, h]

Premises used: Setoid.classes_mkClasses, Setoid.Partitions.isPartition, Setoid.Partitions.toSet, Setoid.Partitions.ext_iff
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
C : Partitions α
rw :
  Partitions.toSet
      ((fun (r : Setoid α) ↦ (Subtype.mk (p := IsPartition) r.classes ⋯ : Subtype (α := Set (Set α)) IsPartition))
        ((fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) ⋯) C)) =
    (mkClasses C.toSet ⋯).classes
⊢ (fun (r : Setoid α) ↦ (Subtype.mk (p := IsPartition) r.classes ⋯ : Subtype (α := Set (Set α)) IsPartition))
      ((fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) ⋯) C) =
    C

Tactic:
rw [Partitions.ext_iff, ← classes_mkClasses C.toSet C.isPartition]

Premises used: Setoid.classes_mkClasses, Setoid.Partitions.isPartition, Setoid.Partitions.toSet, Setoid.Partitions.ext_iff
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
C : Partitions α
⊢ Partitions.toSet
      ((fun (r : Setoid α) ↦ (Subtype.mk (p := IsPartition) r.classes ⋯ : Subtype (α := Set (Set α)) IsPartition))
        ((fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) ⋯) C)) =
    (mkClasses C.toSet ⋯).classes

Tactic:
rfl
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r s : Setoid α
rw : mkClasses r.classes ⋯ ≤ mkClasses s.classes ⋯
| r ≤ s

Tactic:
rw [← mkClasses_classes r, ← mkClasses_classes s]

Premises used: Setoid.mkClasses_classes