awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
a_1 : α
h : a_1 ∈ x
_ :
  ∀ a ∈ x,
    ∀ (x_1 : α) (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a_1 x_3) (x : x_3 ∈ x)
      (h : (s : α → α → Prop) a x_3), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a x_1
⊢ ∀ a ∈ x,
    ∀ (x_1 : α) (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a_1 x_3) (x : x_3 ∈ x)
      (h : (s : α → α → Prop) a x_3), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a x_1

Tactic:
_
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
a_1 : α
h : a_1 ∈ x
a_2 : α
_ :
  a_2 ∈ x →
    ∀ (x_1 : α) (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a_1 x_3) (x : x_3 ∈ x)
      (h : (s : α → α → Prop) a_2 x_3), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1
⊢ a_2 ∈ x →
    ∀ (x_1 : α) (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a_1 x_3) (x : x_3 ∈ x)
      (h : (s : α → α → Prop) a_2 x_3), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1

Tactic:
_
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
a_1 : α
h : a_1 ∈ x
a_2 : α
h_1 : a_2 ∈ x
_ :
  ∀ (x_1 : α) (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a_1 x_3) (x : x_3 ∈ x)
    (h : (s : α → α → Prop) a_2 x_3), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1
⊢ ∀ (x_1 : α) (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a_1 x_3) (x : x_3 ∈ x)
    (h : (s : α → α → Prop) a_2 x_3), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1

Tactic:
_
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
a_1 : α
h : a_1 ∈ x
a_2 : α
h_1 : a_2 ∈ x
x_1 : α
_ :
  x_1 ∈ x →
    ∀ (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a_1 x_3) (x : x_3 ∈ x) (h : (s : α → α → Prop) a_2 x_3),
      (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1
⊢ ∀ (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a_1 x_3) (x : x_3 ∈ x)
    (h : (s : α → α → Prop) a_2 x_3), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1

Tactic:
_
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
a_1 : α
h : a_1 ∈ x
a_2 : α
h_1 : a_2 ∈ x
x_1 : α
h_2 : x_1 ∈ x
_ :
  ∀ (x_2 : α) (x_3 : x_2 ∈ x) (x_4 : (s : α → α → Prop) a_1 x_2) (x : x_2 ∈ x) (h : (s : α → α → Prop) a_2 x_2),
    (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1
⊢ ∀ (x_2 : α) (x_3 : x_2 ∈ x) (x_4 : (s : α → α → Prop) a_1 x_2) (x : x_2 ∈ x) (h : (s : α → α → Prop) a_2 x_2),
    (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1

Tactic:
_
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
a_1 : α
h : a_1 ∈ x
a_2 : α
h_1 : a_2 ∈ x
x_1 : α
h_2 : x_1 ∈ x
x_2 : α
_ :
  x_2 ∈ x →
    ∀ (x_4 : (s : α → α → Prop) a_1 x_2) (x : x_2 ∈ x) (h : (s : α → α → Prop) a_2 x_2),
      (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1
⊢ ∀ (x_3 : x_2 ∈ x) (x_4 : (s : α → α → Prop) a_1 x_2) (x : x_2 ∈ x) (h : (s : α → α → Prop) a_2 x_2),
    (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1

Tactic:
_
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
a_1 : α
h : a_1 ∈ x
a_2 : α
h_1 : a_2 ∈ x
x_1 : α
h_2 : x_1 ∈ x
x_2 : α
h_3 : x_2 ∈ x
ha : (s : α → α → Prop) a_1 x_2
_ : x_2 ∈ x → ∀ (h : (s : α → α → Prop) a_2 x_2), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1
⊢ ∀ (x : x_2 ∈ x) (h : (s : α → α → Prop) a_2 x_2), (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1

Tactic:
_
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
a_1 : α
h : a_1 ∈ x
a_2 : α
h_1 : a_2 ∈ x
x_1 : α
h_2 : x_1 ∈ x
x_2 : α
h_3 : x_2 ∈ x
ha : (s : α → α → Prop) a_1 x_2
h_4 : x_2 ∈ x
hb : (s : α → α → Prop) a_2 x_2
⊢ (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1

Tactic:
⟨(s.trans' hb <| s.trans' (s.symm' ha) ·), (s.trans' ha <| s.trans' (s.symm' hb) ·)⟩

Premises used: Setoid.trans', Setoid.symm', Iff.intro
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
a_1 : α
h : a_1 ∈ x
a_2 : α
h_1 : a_2 ∈ x
x_1 : α
h_2 : x_1 ∈ x
x_2 : α
h_3 : x_2 ∈ x
ha : (s : α → α → Prop) a_1 x_2
h_4 : x_2 ∈ x
hb : (s : α → α → Prop) a_2 x_2
⊢ (s : α → α → Prop) a_1 x_1 ↔ (s : α → α → Prop) a_2 x_1

Tactic:
exact ⟨(s.trans' hb <| s.trans' (s.symm' ha) ·), (s.trans' ha <| s.trans' (s.symm' hb) ·)⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
suffices :
  ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
⊢ SupIndep (α := Finset α) (image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x) id

Tactic:
suffices ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c) by
      simp only [supIndep_iff_pairwiseDisjoint, Set.PairwiseDisjoint, Set.Pairwise, coe_image,
        Set.mem_image, mem_coe, ne_eq, onFun, id_eq, disjoint_iff_ne, forall_mem_not_eq,
        forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_filter, not_and, filter_inj',
        not_forall, @not_imp_comm (_ ↔ _), Decidable.not_not]
      intro _ _ _ _ _ _ _ _ ha _ hb
      exact ⟨(s.trans' hb <| s.trans' (s.symm' ha) ·), (s.trans' ha <| s.trans' (s.symm' hb) ·)⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
⊢ ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)

Tactic:
simp +contextual [← Quotient.eq]

Premises used: Quotient.eq
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
h :
  ∀ (a : α),
    Membership.mem (γ := Finset α) (sup (image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x) id) a ↔ a ∈ x
⊢ sup (image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x) id = x

Tactic:
ext a
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a_1 : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
a : α
h : (∃ i ∈ x, a ∈ x ∧ (s : α → α → Prop) i a) ↔ a ∈ x
⊢ Membership.mem (γ := Finset α) (sup (image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x) id) a ↔ a ∈ x

Tactic:
simp_rw [sup_image, id_comp, mem_sup, mem_filter]

Premises used: Finset.mem_sup, Finset.sup_image, Finset.mem_filter, Function.id_comp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a_1 : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
a : α
h_1 : a ∈ x
w : α
h : a ∈ x ∧ a ∈ x ∧ (s : α → α → Prop) a a
⊢ ∃ i ∈ x, a ∈ x ∧ (s : α → α → Prop) i a

Tactic:
use a
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a_1 : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
a : α
⊢ (∃ i ∈ x, a ∈ x ∧ (s : α → α → Prop) i a) ↔ a ∈ x

Tactic:
refine ⟨(·.choose_spec.2.1), fun _ ↦ by use a⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
this : ∀ x₁ ∈ x, ∃ x₂ ∈ x, (s : α → α → Prop) x₁ x₂
⊢ ⊥ ∉ image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x

Tactic:
simpa [filter_eq_empty_iff]

Premises used: Finset.filter_eq_empty_iff
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
suffices : ∀ x₁ ∈ x, ∃ x₂ ∈ x, (s : α → α → Prop) x₁ x₂
⊢ ⊥ ∉ image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x

Tactic:
suffices ∀ x₁ ∈ x, ∃ x₂ ∈ x, s x₁ x₂ by simpa [filter_eq_empty_iff]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x_1 : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
x : α
_ : x ∈ x_1 → ∃ x₂ ∈ x_1, (s : α → α → Prop) x x₂
⊢ x ∈ x_1 → ∃ x₂ ∈ x_1, (s : α → α → Prop) x x₂

Tactic:
_
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Setoid α
x_1 : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
x : α
h_1 : x ∈ x_1
w : α
h : x ∈ x_1 ∧ (s : α → α → Prop) x x
⊢ ∃ x₂ ∈ x_1, (s : α → α → Prop) x x₂

Tactic:
use x
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
b : α
this :
  (∃ a₁ ∈ x, (b ∈ x ∧ (s : α → α → Prop) a₁ b) ∧ a ∈ x ∧ (s : α → α → Prop) a₁ a) ↔
    a ∈ x ∧ b ∈ x ∧ (s : α → α → Prop) a b
⊢ b ∈ part (ofSetSetoid s x) a ↔ a ∈ x ∧ b ∈ x ∧ (s : α → α → Prop) a b

Tactic:
simpa [mem_part_iff_exists, ofSetSetoid_parts]

Premises used: Finpartition.mem_part_iff_exists, Finpartition.ofSetSetoid_parts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
b : α
suffices :
  (∃ a₁ ∈ x, (b ∈ x ∧ (s : α → α → Prop) a₁ b) ∧ a ∈ x ∧ (s : α → α → Prop) a₁ a) ↔
    a ∈ x ∧ b ∈ x ∧ (s : α → α → Prop) a b
⊢ b ∈ part (ofSetSetoid s x) a ↔ a ∈ x ∧ b ∈ x ∧ (s : α → α → Prop) a b

Tactic:
suffices (∃ a₁ ∈ x, (b ∈ x ∧ s a₁ b) ∧ a ∈ x ∧ s a₁ a) ↔ a ∈ x ∧ b ∈ x ∧ s a b by
    simpa [mem_part_iff_exists, ofSetSetoid_parts]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
b : α
⊢ (∃ a₁ ∈ x, (b ∈ x ∧ (s : α → α → Prop) a₁ b) ∧ a ∈ x ∧ (s : α → α → Prop) a₁ a) ↔
    a ∈ x ∧ b ∈ x ∧ (s : α → α → Prop) a b

Tactic:
⟨
    fun ⟨c, _, ⟨hb, hcb⟩, ⟨ha, hca⟩⟩ ↦ ⟨ha, hb, s.trans' (s.symm' hca) hcb⟩,
    fun h ↦ ⟨a, ⟨h.1, ⟨⟨h.2.1, h.2.2⟩, ⟨h.1, s.refl _⟩⟩⟩⟩
  ⟩

Premises used: Membership.mem, Setoid.trans', Setoid.symm', _private.0.Finpartition.mem_part_ofSetSetoid_iff_rel.match_2, And, And.right, And.left, And.intro, Iff.intro, Exists.intro, Setoid.refl, Setoid.r
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
b : α
⊢ (∃ a₁ ∈ x, (b ∈ x ∧ (s : α → α → Prop) a₁ b) ∧ a ∈ x ∧ (s : α → α → Prop) a₁ a) ↔
    a ∈ x ∧ b ∈ x ∧ (s : α → α → Prop) a b

Tactic:
exact ⟨
    fun ⟨c, _, ⟨hb, hcb⟩, ⟨ha, hca⟩⟩ ↦ ⟨ha, hb, s.trans' (s.symm' hca) hcb⟩,
    fun h ↦ ⟨a, ⟨h.1, ⟨⟨h.2.1, h.2.2⟩, ⟨h.1, s.refl _⟩⟩⟩⟩
  ⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
a : α
inst_1 : Fintype α
s : Setoid α
inst_2 : DecidableRel (α := α) (⇑s : α → α → Prop)
b : α
this :
  b ∈ part (s := univ) (ofSetSetoid s univ) a ↔
    Membership.mem (γ := Finset α) univ a ∧ Membership.mem (γ := Finset α) univ b ∧ (s : α → α → Prop) a b
⊢ b ∈ part (s := univ) (ofSetoid s) a ↔ (s : α → α → Prop) a b

Tactic:
simpa
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
a : α
inst_1 : Fintype α
s : Setoid α
inst_2 : DecidableRel (α := α) (⇑s : α → α → Prop)
b : α
suffices :
  b ∈ part (s := univ) (ofSetSetoid s univ) a ↔
    Membership.mem (γ := Finset α) univ a ∧ Membership.mem (γ := Finset α) univ b ∧ (s : α → α → Prop) a b
⊢ b ∈ part (s := univ) (ofSetoid s) a ↔ (s : α → α → Prop) a b

Tactic:
suffices b ∈ (ofSetSetoid s univ).part a ↔ a ∈ univ ∧ b ∈ univ ∧ s a b by simpa
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
a : α
inst_1 : Fintype α
s : Setoid α
inst_2 : DecidableRel (α := α) (⇑s : α → α → Prop)
b : α
⊢ b ∈ part (s := univ) (ofSetSetoid s univ) a ↔
    Membership.mem (γ := Finset α) univ a ∧ Membership.mem (γ := Finset α) univ b ∧ (s : α → α → Prop) a b

Tactic:
mem_part_ofSetSetoid_iff_rel univ

Premises used: Finpartition.mem_part_ofSetSetoid_iff_rel, Finset.univ
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
a : α
inst_1 : Fintype α
s : Setoid α
inst_2 : DecidableRel (α := α) (⇑s : α → α → Prop)
b : α
⊢ b ∈ part (s := univ) (ofSetSetoid s univ) a ↔
    Membership.mem (γ := Finset α) univ a ∧ Membership.mem (γ := Finset α) univ b ∧ (s : α → α → Prop) a b

Tactic:
exact mem_part_ofSetSetoid_iff_rel univ

Premises used: Finpartition.mem_part_ofSetSetoid_iff_rel, Finset.univ
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
x : Finset α
hx : x ∈ (↑(image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) : Set (Finset α))
y : Finset α
hy : y ∈ (↑(image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) : Set (Finset α))
h : x ≠ y
z : α
hz1 : z ∈ id x
hz2 : z ∈ id y
rw :
  ∀ (hx : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = x) (y : Finset α)
    (hy : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = y) (h : x ≠ y) (z : α) (hz1 : z ∈ id x) (hz2 : z ∈ id y),
    x = y
⊢ x = y

Tactic:
rw [mem_coe, mem_image] at hx hy

Premises used: Finset.mem_image, Finset.mem_coe
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
x : Finset α
hx : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = x
y : Finset α
hy : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = y
h : x ≠ y
z : α
hz1 : z ∈ id x
hz2 : z ∈ id y
obtain :
  ∀ (Q : Finset (Finset α)) (hQ : Q ∈ F.powerset) (h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ y)
    (hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})), {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = y
⊢ x = y

Tactic:
obtain ⟨Q, hQ, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
y : Finset α
hy : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = y
z : α
hz2 : z ∈ id y
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ y
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
obtain :
  ∀ (R : Finset (Finset α)) (hR : R ∈ F.powerset) (hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}))
    (h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}),
    {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = y

Tactic:
obtain ⟨R, hR, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t})
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
h' : Q = R
subst :
  ∀ (hR : Q ∈ F.powerset) (hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}))
    (h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}),
    {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}

Tactic:
subst h'
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
hR : Q ∈ F.powerset
hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}

Tactic:
of_eq_true (eq_self {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})

Premises used: eq_self, of_eq_true, Finset.filter
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
hR : Q ∈ F.powerset
hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}

Tactic:
exact of_eq_true (eq_self {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})

Premises used: eq_self, of_eq_true, Finset.filter
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t})
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
suffices : Q = R
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}

Tactic:
suffices h' : Q = R by
              subst h'
              exact of_eq_true (eq_self {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t})
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
rw :
  ∀ (hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t) (R : Finset (Finset α)) (hR : R ∈ F.powerset)
    (hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t) (h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}),
    Q = R
⊢ Q = R

Tactic:
rw [id, mem_filter] at hz1 hz2

Premises used: id, Finset.mem_filter
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
rw :
  ∀ (hQ : Q ⊆ F) (hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t) (R : Finset (Finset α)) (hR : R ⊆ F)
    (hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t) (h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}),
    Q = R
⊢ Q = R

Tactic:
rw [mem_powerset] at hQ hR

Premises used: Finset.mem_powerset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
h₁ : ∀ (i : Finset α), i ∈ Q ↔ i ∈ R
⊢ Q = R

Tactic:
ext i
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
⊢ i ∈ Q ↔ i ∈ R

Tactic:
⟨fun hi ↦ ?_, fun hi ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
h₁ : ∀ (hi : i ∈ Q), i ∈ R
h₂ : ∀ (hi : i ∈ R), i ∈ Q
⊢ i ∈ Q ↔ i ∈ R

Tactic:
refine ⟨fun hi ↦ ?_, fun hi ↦ ?_⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ Q
h₁ : z ∈ i
h₂ h₃ h₄ h₅ : i ∈ Q
⊢ i ∈ R

Tactic:
rwa [hz2.2 _ (hQ hi), ← hz1.2 _ (hQ hi)]

Premises used: And.right
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ R
h₁ : z ∈ i
h₂ h₃ h₄ h₅ : i ∈ R
⊢ i ∈ Q

Tactic:
rwa [hz1.2 _ (hR hi), ← hz2.2 _ (hR hi)]

Premises used: And.right
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
⊢ sup (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) id = s

Tactic:
(Finset.sup_le fun t ht ↦ ?_).antisymm fun a ha ↦ ?_

Premises used: LE.le.antisymm, Finset.sup_le