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 : Finset α
F : Finset (Finset α)
refine_1 :
  ∀ (t : Finset α)
    (ht :
      Membership.mem (γ := Finset (Finset α))
        (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) t),
    id t ≤ s
refine_2 :
  ∀ (a : α) (ha : a ∈ s),
    Membership.mem (γ := Finset α)
      (sup (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) id) a
⊢ sup (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) id = s

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

Premises used: LE.le.antisymm, Finset.sup_le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
t : Finset α
ht :
  Membership.mem (γ := Finset (Finset α))
    (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) t
⊢ ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = t

Tactic:
rw [mem_image] at ht

Premises used: Finset.mem_image
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F : Finset (Finset α)
t : Finset α
ht : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = t
refine_1 : ∀ A ∈ F.powerset, id ({i ∈ s | ∀ t ∈ F, t ∈ A ↔ i ∈ t}) ≤ s
⊢ id t ≤ s

Tactic:
obtain ⟨A, _, rfl⟩ := ht

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 A : Finset (Finset α)
left : A ∈ F.powerset
⊢ id ({i ∈ s | ∀ t ∈ F, t ∈ A ↔ i ∈ t}) ≤ s

Tactic:
s.filter_subset _

Premises used: Set.Mem, setOf, Finset.filter_subset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
F A : Finset (Finset α)
left : A ∈ F.powerset
⊢ id ({i ∈ s | ∀ t ∈ F, t ∈ A ↔ i ∈ t}) ≤ s

Tactic:
exact s.filter_subset _

Premises used: Finset.filter_subset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a_1 : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
refine_2 :
  ∃ (i : Finset α),
    Membership.mem (γ := Finset (Finset α))
        (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) i ∧
      a ∈ id i
⊢ Membership.mem (γ := Finset α)
    (sup (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) id) a

Tactic:
rw [mem_sup]

Premises used: Finset.mem_sup
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a_1 : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ ∃ (i : Finset α),
    Membership.mem (γ := Finset (Finset α))
        (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) i ∧
      a ∈ id i

Tactic:
⟨{i ∈ s | ∀ t ∈ F, t ∈ {u ∈ F | a ∈ u} ↔ i ∈ t},
            mem_image_of_mem _ (mem_powerset.2 <| filter_subset _ _),
            mem_filter.2 ⟨ha, fun t ht ↦ ?_⟩⟩

Premises used: Iff.mpr, Finset.filter_subset, Finset.mem_powerset, And.intro, Exists.intro, Finset.mem_filter, Finset.mem_image_of_mem, Finset.filter
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a_1 : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
refine_2 : ∀ (t : Finset α) (ht : t ∈ F), t ∈ {u ∈ F | a ∈ u} ↔ a ∈ t
⊢ ∃ (i : Finset α),
    Membership.mem (γ := Finset (Finset α))
        (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) i ∧
      a ∈ id i

Tactic:
refine
          ⟨{i ∈ s | ∀ t ∈ F, t ∈ {u ∈ F | a ∈ u} ↔ i ∈ t},
            mem_image_of_mem _ (mem_powerset.2 <| filter_subset _ _),
            mem_filter.2 ⟨ha, fun t ht ↦ ?_⟩⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P : Finpartition s_1
a_1 : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
refine_2 : t ∈ F ∧ a ∈ t ↔ a ∈ t
⊢ t ∈ {u ∈ F | a ∈ u} ↔ a ∈ t

Tactic:
rw [mem_filter]

Premises used: Finset.mem_filter
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P : Finpartition s_1
a_1 : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ F ∧ a ∈ t ↔ a ∈ t

Tactic:
and_iff_right ht

Premises used: and_iff_right
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P : Finpartition s_1
a_1 : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ F ∧ a ∈ t ↔ a ∈ t

Tactic:
exact and_iff_right ht

Premises used: and_iff_right
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
⊢ t ∈ parts (atomise s F) ↔ t.Nonempty ∧ ∃ Q ⊆ F, {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} = t

Tactic:
simp only [atomise, ofErase, bot_eq_empty, mem_erase, mem_image, nonempty_iff_ne_empty,
    mem_powerset]

Premises used: Finset.bot_eq_empty, Finset.mem_image, Finpartition.ofErase, Finset.nonempty_iff_ne_empty, Finset.mem_powerset, Finset.mem_erase, Finpartition.atomise
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
hs : s.Nonempty
simp : parts (a := s) (ofErase {s} ⋯ ⋯) = {s}
⊢ parts (atomise s ∅) = {s}

Tactic:
simp only [atomise, powerset_empty, image_singleton, notMem_empty, IsEmpty.forall_iff,
    imp_true_iff, filter_true]

Premises used: Finset.filter_true, Finset.image_singleton, imp_true_iff, Finset.notMem_empty, Finpartition.atomise, Finset.powerset_empty, IsEmpty.forall_iff
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ parts (a := s) (ofErase {s} ⋯ ⋯) = {s}

Tactic:
erase_eq_of_notMem (notMem_singleton.2 hs.ne_empty.symm)

Premises used: Finset.notMem_singleton, Iff.mpr, Ne.symm, Finset.Nonempty.ne_empty, Finset.erase_eq_of_notMem, Finset.erase
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ parts (a := s) (ofErase {s} ⋯ ⋯) = {s}

Tactic:
exact erase_eq_of_notMem (notMem_singleton.2 hs.ne_empty.symm)

Premises used: Finset.notMem_singleton, Iff.mpr, Ne.symm, Finset.Nonempty.ne_empty, Finset.erase_eq_of_notMem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
F : Finset (Finset α)
⊢ #(parts (atomise s F)) ≤ HPow.hPow (α := ℕ) 2 #F

Tactic:
(card_le_card <| erase_subset _ _).trans <| Finset.card_image_le.trans (card_powerset _).le

Premises used: Finset.card_le_card, Eq.le, Finset.card_image_le, LE.le.trans, Finset.erase, Finset.erase_subset, Finset.card_powerset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
h : ∀ (a : α), a ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}.biUnion id ↔ a ∈ t
⊢ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}.biUnion id = t

Tactic:
ext a
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
⊢ a ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}.biUnion id ↔ a ∈ t

Tactic:
mem_biUnion.trans ⟨fun ⟨u, hu, ha⟩ ↦ (mem_filter.1 hu).2.1 ha, fun ha ↦ ?_⟩

Premises used: Membership.mem, And.right, And.left, Iff.intro, Iff.mp, Iff.trans, Finset.mem_filter, _private.0.Finpartition.biUnion_filter_atomise.match_1, Finset.mem_biUnion
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
h : ∀ (ha : a ∈ t), ∃ a_1 ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1
⊢ a ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}.biUnion id ↔ a ∈ t

Tactic:
refine mem_biUnion.trans ⟨fun ⟨u, hu, ha⟩ ↦ (mem_filter.1 hu).2.1 ha, fun ha ↦ ?_⟩

Premises used: Iff.intro, Iff.trans, Finset.mem_biUnion
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
h :
  ∀ (u : Finset α) (hu : u ∈ parts (atomise s F)) (hau : a ∈ u),
    ∃ a_1 ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1
⊢ ∃ a_1 ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1

Tactic:
obtain ⟨u, hu, hau⟩ := (atomise s F).exists_mem (hts ha)

Premises used: Finpartition.exists_mem, Finpartition.atomise
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ parts (atomise s F)
hau : a ∈ u
⊢ ∃ a_1 ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1

Tactic:
⟨u, mem_filter.2 ⟨hu, fun b hb ↦ ?_, _, hau⟩, hau⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.mem_filter
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ parts (atomise s F)
hau : a ∈ u
h : ∀ (b : α) (hb : b ∈ u), b ∈ t
⊢ ∃ a_1 ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}, a ∈ id a_1

Tactic:
refine ⟨u, mem_filter.2 ⟨hu, fun b hb ↦ ?_, _, hau⟩, hau⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
u : Finset α
hu : u ∈ parts (atomise s F)
hau : a ∈ u
b : α
hb : b ∈ u
h :
  ∀ (Q : Finset (Finset α)) (_hQ : Q ⊆ F) (hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ parts (atomise s F))
    (hau : a ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}) (hb : b ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}), b ∈ t
⊢ b ∈ t

Tactic:
obtain ⟨Q, _hQ, rfl⟩ := (mem_atomise.1 hu).2

Premises used: Finpartition.mem_atomise, And.right, Iff.mp, rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ parts (atomise s F)
hau : a ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}
hb : b ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}
⊢ a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u

Tactic:
rw [mem_filter] at hau hb

Premises used: Finset.mem_filter
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ parts (atomise s F)
hau : a ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}
hb : b ∈ {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u}
hau₁ : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
⊢ b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u

Tactic:
rw [mem_filter] at hau hb

Premises used: Finset.mem_filter
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
ha : a ∈ t
b : α
Q : Finset (Finset α)
_hQ : Q ⊆ F
hu : {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} ∈ parts (atomise s F)
hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u
hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u
h : t ∈ Q
h₁ h₂ h₃ h₄ : a ∈ t
⊢ b ∈ t

Tactic:
rwa [← hb.2 _ ht, hau.2 _ ht]

Premises used: And.right
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun (P : Finset (Finset α)) ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
⊢ #({u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}) ≤ HPow.hPow (α := ℕ) 2 (#F - 1)

Tactic:
(card_le_card h).trans (card_image_le.trans ?_)

Premises used: Finset.card_le_card, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun (P : Finset (Finset α)) ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
refine : #(F.erase t).powerset ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
⊢ #({u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}) ≤ HPow.hPow (α := ℕ) 2 (#F - 1)

Tactic:
refine (card_le_card h).trans (card_image_le.trans ?_)

Premises used: Finset.card_le_card, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun (P : Finset (Finset α)) ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
rw : HPow.hPow (α := ℕ) 2 #(F.erase t) ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
rw₁ rw₂ : HPow.hPow (α := ℕ) 2 (#F - 1) ≤ HPow.hPow (α := ℕ) 2 (#F - 1)
⊢ #(F.erase t).powerset ≤ HPow.hPow (α := ℕ) 2 (#F - 1)

Tactic:
rw [card_powerset, card_erase_of_mem ht]

Premises used: Finset.card_erase_of_mem, Finset.card_powerset
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
suffices :
  {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun (P : Finset (Finset α)) ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
⊢ #({u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty}) ≤ HPow.hPow (α := ℕ) 2 (#F - 1)

Tactic:
suffices h :
    {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ⊆
      (F.erase t).powerset.image fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x} by
    refine (card_le_card h).trans (card_image_le.trans ?_)
    rw [card_powerset, card_erase_of_mem ht]
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
simp_rw :
  ∀ ⦃x : Finset α⦄,
    ∀ x_1 ∈ x,
      ∀ x_2 ⊆ F,
        {i ∈ s | ∀ u ∈ F, u ∈ x_2 ↔ i ∈ u} = x →
          x ⊆ t → ∀ x_3 ∈ x, ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ {u ∈ parts (atomise s F) | u ⊆ t ∧ u.Nonempty} →
      Membership.mem (γ := Finset (Finset α))
        (image (fun (P : Finset (Finset α)) ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset) x

Tactic:
simp_rw [mem_image, mem_powerset, mem_filter, and_imp, Finset.Nonempty, exists_imp, mem_atomise,
    and_imp, Finset.Nonempty, exists_imp, and_imp]

Premises used: Finset.mem_image, and_imp, Finpartition.mem_atomise, Finset.mem_powerset, Finset.Nonempty, Finset.mem_filter, exists_imp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
hy₂ : {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u} ⊆ t
j : α
_hj : j ∈ {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
⊢ ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}

Tactic:
⟨P.erase t, erase_subset_erase _ PQ, ?_⟩

Premises used: Finset.erase_subset_erase, And.intro, Exists.intro, Finset.erase
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
hy₂ : {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u} ⊆ t
j : α
_hj : j ∈ {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
refine : {i ∈ s | ∀ x ∈ F, x ∈ insert t (P.erase t) ↔ i ∈ x} = {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
⊢ ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}

Tactic:
refine ⟨P.erase t, erase_subset_erase _ PQ, ?_⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
i : α
P : Finset (Finset α)
PQ : P ⊆ F
hi : i ∈ {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
hy₂ : {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u} ⊆ t
j : α
_hj : j ∈ {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}
⊢ {i ∈ s | ∀ x ∈ F, x ∈ insert t (P.erase t) ↔ i ∈ x} = {i ∈ s | ∀ u ∈ F, u ∈ P ↔ i ∈ u}

Tactic:
simp only [insert_erase (((mem_filter.1 hi).2 _ ht).2 <| hy₂ hi)]

Premises used: Iff.mpr, And.right, Iff.mp, Finset.mem_filter, Finset.insert_erase
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : (i : ι) → Preorder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ ∃ (i : ι), (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
let h' := Pi.lt_def.1 hlt
  let ⟨i, hi, hl⟩ := hwf.has_min {i | x i < y i} h'.2
  ⟨i, fun j hj => ⟨h'.1 j, not_not.1 fun h => hl j (lt_of_le_not_ge (h'.1 j) h) hj⟩, hi⟩

Premises used: Classical.not_not, Pi.lt_def, setOf, Exists, And, _private.0.Pi.lex_lt_of_lt_of_preorder.match_1, And.right, And.left, lt_of_le_not_ge, And.intro, LT.lt, Exists.intro, Iff.mp, WellFounded.has_min
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
simp_rw : ∃ (i : ι), (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
⊢ Pi.Lex (β := β) r (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) x y

Tactic:
simp_rw [Pi.Lex, le_antisymm_iff]

Premises used: Pi.Lex, le_antisymm_iff
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ ∃ (i : ι), (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
lex_lt_of_lt_of_preorder hwf hlt

Premises used: Pi.lex_lt_of_lt_of_preorder
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ ∃ (i : ι), (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
exact lex_lt_of_lt_of_preorder hwf hlt

Premises used: Pi.lex_lt_of_lt_of_preorder
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : (i : ι) → LT (β i)
r : ι → ι → Prop
inst_2 : Std.Irrefl r
x y : (i : ι) → β i
⊢ Pi.Lex (β := β) r (fun {i : ι} (x1 x2 : β i) ↦ x1 < x2) x y ↔ LT.lt (α := β default) (x default) (y default)

Tactic:
simp [Pi.Lex, Unique.forall_iff, Unique.exists_iff, irrefl]

Premises used: irrefl, Pi.Lex, Unique.forall_iff, Unique.exists_iff
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : ∀ (i : ι), Std.Trichotomous (α := β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex (β := β) r (@s) a b
hba : ¬Pi.Lex (β := β) r (@s) b a
by_contra! : ∀ (h : a ≠ b), False
⊢ a = b

Tactic:
by_contra! h
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : ∀ (i : ι), Std.Trichotomous (α := β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex (β := β) r (@s) a b
hba : ¬Pi.Lex (β := β) r (@s) b a
h : a ≠ b
⊢ ∃ (a_1 : ι), a a_1 ≠ b a_1

Tactic:
rw [Function.ne_iff] at h

Premises used: Function.ne_iff
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : ∀ (i : ι), Std.Trichotomous (α := β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex (β := β) r (@s) a b
hba : ¬Pi.Lex (β := β) r (@s) b a
h : ∃ (a_1 : ι), a a_1 ≠ b a_1
i : ι := wf.min (r := r) {i : ι | a i ≠ b i} h
⊢ ∀ (j : ι) (hr : r j i), a j = b j

Tactic:
have hri j (hr : r j i) : a j = b j := not_not.mp (wf.not_lt_min _ · hr)
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : ∀ (i : ι), Std.Trichotomous (α := β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex (β := β) r (@s) a b
hba : ¬Pi.Lex (β := β) r (@s) b a
h : ∃ (a_1 : ι), a a_1 ≠ b a_1
i : ι := wf.min (r := r) {i : ι | a i ≠ b i} h
hri : ∀ (j : ι) (hr : r j i), a j = b j
⊢ ¬s (b i) (a i) → a i = b i

Tactic:
have := Std.Trichotomous.trichotomous (a i) (b i) (hab ⟨i, hri, ·⟩)
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : ∀ (i : ι), Std.Trichotomous (α := β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex (β := β) r (@s) a b
hba : ¬Pi.Lex (β := β) r (@s) b a
h : ∃ (a_1 : ι), a a_1 ≠ b a_1
i : ι := wf.min (r := r) {i : ι | a i ≠ b i} h
hri : ∀ (j : ι) (hr : r j i), a j = b j
this : ¬s (b i) (a i) → a i = b i
⊢ False

Tactic:
hba ⟨i, (hri · · |>.symm), Not.imp_symm this <| wf.min_mem {i | a i ≠ b i} h⟩

Premises used: WellFounded.min_mem, setOf, Not.imp_symm, Ne, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : ∀ (i : ι), Std.Trichotomous (α := β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex (β := β) r (@s) a b
hba : ¬Pi.Lex (β := β) r (@s) b a
h : ∃ (a_1 : ι), a a_1 ≠ b a_1
i : ι := wf.min (r := r) {i : ι | a i ≠ b i} h
hri : ∀ (j : ι) (hr : r j i), a j = b j
this : ¬s (b i) (a i) → a i = b i
⊢ False

Tactic:
exact hba ⟨i, (hri · · |>.symm), Not.imp_symm this <| wf.min_mem {i | a i ≠ b i} h⟩

Premises used: WellFounded.min_mem, setOf, Not.imp_symm, Ne, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
x : (i : ι) → β i
i : ι
⊢ (toLex : (a : (i : ι) → β i) → Lex ((i : ι) → β i)) x i = x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
x : Lex ((i : ι) → β i)
i : ι
⊢ (ofLex : (a : Lex ((i : ι) → β i)) → (i : ι) → β i) x i = x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
x : (i : ι) → β i
i : ι
⊢ (toColex : (a : (i : ι) → β i) → Colex ((i : ι) → β i)) x i = x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
x : Colex ((i : ι) → β i)
i : ι
⊢ (ofColex : (a : Colex ((i : ι) → β i)) → (i : ι) → β i) x i = x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : (i : ι) → LT (β i)
inst_2 : Preorder ι
x y : Lex ((i : ι) → β i)
⊢ x < y ↔ LT.lt (α := β default) (x default) (y default)

Tactic:
lex_iff_of_unique

Premises used: Pi.lex_iff_of_unique
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
inst : Unique ι
inst_1 : (i : ι) → LT (β i)
inst_2 : Preorder ι
x y : Colex ((i : ι) → β i)
⊢ x < y ↔ LT.lt (α := β default) (x default) (y default)

Tactic:
lex_iff_of_unique

Premises used: Pi.lex_iff_of_unique
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
inl : ∀ (H : N₁ < N₂), a < c
inr : ∀ (lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → b j = c j) (b_lt_c : b N₁ < c N₁), a < c
inr₁ : ∀ (H : N₂ < N₁), a < c
⊢ a < c

Tactic:
rcases lt_trichotomy N₁ N₂ with (H | rfl | H)

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Order.PiLex
Goal:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst : LinearOrder ι
inst_1 : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
H : N₁ < N₂
⊢ a < c

Tactic:
⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ <| hj.trans H), lt_N₂ _ H ▸ a_lt_b⟩

Premises used: Eq.rec, Pi.Lex, And.intro, Exists.intro, LT.lt.trans, Eq.trans