awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a : α
P : Finpartition a
b c : α
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ #(P.extend hb hab hc).parts = #P.parts + 1

Tactic:
card_insert_of_notMem fun h ↦ hb <| hab.symm.eq_bot_of_le <| P.le h

Premises used: Finset.card_insert_of_notMem, Disjoint.eq_bot_of_le, Disjoint.symm, Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b_1 c : α
P : Finpartition a
b : α
rw : P.parts.sup (id ∘ fun (x : α) ↦ x \ b) = a \ b
rw₁ : (P.parts.sup fun (x : α) ↦ x \ b) = a \ b
rw₂ : (P.parts.sup fun (x : α) ↦ x) \ b = a \ b
rw₃ : P.parts.sup id \ b = a \ b
rw₄ rw₅ : a \ b = a \ b
⊢ sup (image (fun (x : α) ↦ x \ b) P.parts) id = a \ b

Tactic:
rw [sup_image, id_comp, Finset.sup_sdiff_right, ← Function.id_def, P.sup_parts]

Premises used: Function.id_def, Finset.sup_sdiff_right, Finset.sup_image, Finpartition.sup_parts, Function.id_comp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b c : α
P : Finpartition a
simp : (∃ x ∈ P.parts, ¬c = ⊥ ∧ x \ b = c) ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c
⊢ c ∈ (P.avoid b).parts ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c

Tactic:
simp only [avoid, ofErase, mem_erase, Ne, mem_image, ← exists_and_left,
    @and_left_comm (c ≠ ⊥)]

Premises used: Finset.mem_image, Finpartition.avoid, exists_and_left, and_left_comm, Finpartition.ofErase, Ne, Finset.mem_erase
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b c : α
P : Finpartition a
⊢ (∃ x ∈ P.parts, ¬c = ⊥ ∧ x \ b = c) ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c

Tactic:
exists_congr fun d ↦ and_congr_right' <| and_congr_left ?_

Premises used: and_congr_right', and_congr_left, exists_congr
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b c : α
P : Finpartition a
refine : ∀ (d : α), d \ b = c → (¬c = ⊥ ↔ ¬d ≤ b)
⊢ (∃ x ∈ P.parts, ¬c = ⊥ ∧ x \ b = c) ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c

Tactic:
refine exists_congr fun d ↦ and_congr_right' <| and_congr_left ?_

Premises used: and_congr_right', and_congr_left, exists_congr
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
d : α
rw rw₁ : ¬d ≤ b ↔ ¬d ≤ b
⊢ ¬d \ b = ⊥ ↔ ¬d ≤ b

Tactic:
rw [sdiff_eq_bot_iff]

Premises used: sdiff_eq_bot_iff
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a = b
subst : (P.extendOfLE ⋯).parts = P.parts
⊢ (P.extendOfLE ⋯).parts = P.parts

Tactic:
subst hab
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a : α
P : Finpartition a
⊢ (P.extendOfLE ⋯).parts = P.parts

Tactic:
simp [extendOfLE]

Premises used: Finpartition.extendOfLE
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a < b
⊢ (P.extendOfLE ⋯).parts = insert (b \ a) P.parts

Tactic:
simp [extendOfLE, sdiff_eq_bot_iff.not.mpr (not_le_of_gt hab)]

Premises used: Iff.mpr, Finpartition.extendOfLE, Iff.not, sdiff_eq_bot_iff, not_le_of_gt
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
unfold :
  P.parts ⊆
    parts (a := b)
      (if hr : b \ a = ⊥ then Eq.rec (motive := fun (x : α) (h : a = x) ↦ Finpartition x) P ⋯ else P.extend hr ⋯ ⋯)
⊢ P.parts ⊆ (P.extendOfLE hab).parts

Tactic:
unfold extendOfLE

Premises used: Finpartition.extendOfLE
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
pos : ∀ (hr : b \ a = ⊥), P.parts ⊆ parts (a := b) (Eq.rec (motive := fun (x : α) (h : a = x) ↦ Finpartition x) P ⋯)
neg : ∀ (hr : ¬b \ a = ⊥), P.parts ⊆ (P.extend hr ⋯ ⋯).parts
⊢ P.parts ⊆
    parts (a := b)
      (if hr : b \ a = ⊥ then Eq.rec (motive := fun (x : α) (h : a = x) ↦ Finpartition x) P ⋯ else P.extend hr ⋯ ⋯)

Tactic:
split_ifs with hr
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
hr : b \ a = ⊥
pos : ∀ (hab : a ≤ a) (hr : a \ a = ⊥), P.parts ⊆ P.parts
⊢ P.parts ⊆ parts (a := b) (Eq.rec (motive := fun (x : α) (h : a = x) ↦ Finpartition x) P ⋯)

Tactic:
cases le_antisymm (sdiff_eq_bot_iff.mp hr) hab

Premises used: sdiff_eq_bot_iff, le_antisymm, Iff.mp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a : α
P : Finpartition a
hab : a ≤ a
hr : a \ a = ⊥
⊢ P.parts ⊆ P.parts

Tactic:
rfl
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
hr : ¬b \ a = ⊥
⊢ P.parts ⊆ (P.extend hr ⋯ ⋯).parts

Tactic:
Finset.subset_insert _ _

Premises used: Set.Mem, setOf, Finset.subset_insert
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
hr : ¬b \ a = ⊥
⊢ P.parts ⊆ (P.extend hr ⋯ ⋯).parts

Tactic:
exact Finset.subset_insert _ _

Premises used: Finset.subset_insert
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
p : α
hp : p ∈ (P.extendOfLE hab).parts
pos : ∀ (h : a < b), p ∈ P.parts ∨ p = b \ a
neg : ∀ (h : ¬a < b), p ∈ P.parts ∨ p = b \ a
⊢ p ∈ P.parts ∨ p = b \ a

Tactic:
by_cases h : a < b
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
p : α
hp : p ∈ (P.extendOfLE hab).parts
h : a < b
⊢ p ∈ P.parts ∨ p = b \ a

Tactic:
simp_all [parts_extendOfLE_of_lt _ h, mem_insert, Or.comm]

Premises used: Or.comm, Finpartition.parts_extendOfLE_of_lt, Finset.mem_insert
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
p : α
hp : p ∈ (P.extendOfLE hab).parts
h : ¬a < b
neg : p ∈ P.parts
⊢ p ∈ P.parts ∨ p = b \ a

Tactic:
left
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
p : α
hp : p ∈ (P.extendOfLE hab).parts
h : ¬a < b
⊢ p ∈ P.parts

Tactic:
simpa [parts_extendOfLE_of_eq _ (LE.le.eq_of_not_lt hab h)] using hp

Premises used: LE.le.eq_of_not_lt, Finpartition.parts_extendOfLE_of_eq
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : Finset α
ha : a ∈ P.parts
⊢ a ⊆ s

Tactic:
P.le ha

Premises used: Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : Finset α
ha : a ∈ P.parts
⊢ a.Nonempty

Tactic:
nonempty_iff_ne_empty.2 <| P.ne_bot ha

Premises used: Iff.mpr, Finset.nonempty_iff_ne_empty, Finpartition.ne_bot
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∅ ∉ P.parts

Tactic:
P.bot_notMem

Premises used: Set.Mem, setOf, Finpartition.bot_notMem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
h : t ∈ P.parts
⊢ t ≠ ∅

Tactic:
P.ne_bot h

Premises used: Finpartition.ne_bot
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hu : u ∈ P.parts
hat : a ∈ t
hau : a ∈ u
⊢ t = u

Tactic:
P.disjoint.elim ht hu <| not_disjoint_iff.2 ⟨a, hat, hau⟩

Premises used: Iff.mpr, Finpartition.disjoint, Set.PairwiseDisjoint.elim, And.intro, Exists.intro, Finset.not_disjoint_iff
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ a ∈ P.parts.sup id

Tactic:
simp_rw [← P.sup_parts] at ha

Premises used: Finpartition.sup_parts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ P.parts.sup id
⊢ ∃ t ∈ P.parts, a ∈ t

Tactic:
mem_sup.1 ha

Premises used: Finset.mem_sup, Iff.mp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ P.parts.sup id
⊢ ∃ t ∈ P.parts, a ∈ t

Tactic:
exact mem_sup.1 ha

Premises used: Finset.mem_sup, Iff.mp
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P.parts.biUnion id = s

Tactic:
(sup_eq_biUnion _ _).symm.trans P.sup_parts

Premises used: Finset.sup_eq_biUnion, Eq.symm, Finpartition.sup_parts, Eq.trans
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
obtain : ∀ (t : Finset α) (ht : t ∈ P.parts) (ht' : a ∈ t), ∃! t : Finset α, t ∈ P.parts ∧ a ∈ t
⊢ ∃! t : Finset α, t ∈ P.parts ∧ a ∈ t

Tactic:
obtain ⟨t, ht, ht'⟩ := P.exists_mem ha

Premises used: Finpartition.exists_mem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
⊢ ∃! t : Finset α, t ∈ P.parts ∧ a ∈ t

Tactic:
⟨t, ⟨ht, ht'⟩, ?_⟩

Premises used: ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
refine : ∀ (y : Finset α), (fun (t : Finset α) ↦ t ∈ P.parts ∧ a ∈ t) y → y = t
⊢ ∃! t : Finset α, t ∈ P.parts ∧ a ∈ t

Tactic:
refine ⟨t, ⟨ht, ht'⟩, ?_⟩
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
u : Finset α
hu : u ∈ P.parts
hu' : a ∈ u
⊢ u = t

Tactic:
P.eq_of_mem_parts hu ht hu' ht'

Premises used: Finpartition.eq_of_mem_parts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
u : Finset α
hu : u ∈ P.parts
hu' : a ∈ u
⊢ u = t

Tactic:
exact P.eq_of_mem_parts hu ht hu' ht'

Premises used: Finpartition.eq_of_mem_parts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
simp : (↑parts : Set (Finset α)).PairwiseDisjoint id
⊢ parts.SupIndep id

Tactic:
simp only [supIndep_iff_pairwiseDisjoint]

Premises used: Finset.supIndep_iff_pairwiseDisjoint
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a_1 : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ (↑parts : Set (Finset α))
b : Finset α
hb : b ∈ (↑parts : Set (Finset α))
hab : a ≠ b
rw : ∀ ⦃a_2 : α⦄, a_2 ∈ id a → a_2 ∉ id b
⊢ (Disjoint on id) a b

Tactic:
rw [Function.onFun, Finset.disjoint_left]

Premises used: Function.onFun, Finset.disjoint_left
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a_1 : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ (↑parts : Set (Finset α))
b : Finset α
hb : b ∈ (↑parts : Set (Finset α))
hab : a ≠ b
x : α
hx : x ∈ id a
hx' : x ∈ id b
⊢ False

Tactic:
hab ((h' x (h _ ha hx)).unique ⟨ha, hx⟩ ⟨hb, hx'⟩)

Premises used: And.intro, ExistsUnique.unique
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a_1 : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ (↑parts : Set (Finset α))
b : Finset α
hb : b ∈ (↑parts : Set (Finset α))
hab : a ≠ b
x : α
hx : x ∈ id a
hx' : x ∈ id b
⊢ False

Tactic:
exact hab ((h' x (h _ ha hx)).unique ⟨ha, hx⟩ ⟨hb, hx'⟩)

Premises used: And.intro, ExistsUnique.unique
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
h₁ : ∀ (i : α), i ∈ parts.sup id ↔ i ∈ s
⊢ parts.sup id = s

Tactic:
ext i
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
i : α
h₁ : (∃ i_1 ∈ parts, i ∈ i_1) ↔ i ∈ s
⊢ i ∈ parts.sup id ↔ i ∈ s

Tactic:
simp only [mem_sup, id_eq]

Premises used: Finset.mem_sup, id_eq
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
i : α
h₁ : (∃ i_1 ∈ parts, i ∈ i_1) → i ∈ s
h₂ : i ∈ s → ∃ i_1 ∈ parts, i ∈ i_1
⊢ (∃ i_1 ∈ parts, i ∈ i_1) ↔ i ∈ s

Tactic:
constructor
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
i : α
j : Finset α
hj : j ∈ parts
hj' : i ∈ j
⊢ i ∈ s

Tactic:
h j hj hj'
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
i : α
j : Finset α
hj : j ∈ parts
hj' : i ∈ j
⊢ i ∈ s

Tactic:
exact h j hj hj'
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
i : α
hi : i ∈ s
⊢ ∃ i_1 ∈ parts, i ∈ i_1

Tactic:
(h' i hi).exists

Premises used: ExistsUnique.exists
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
i : α
hi : i ∈ s
⊢ ∃ i_1 ∈ parts, i ∈ i_1

Tactic:
exact (h' i hi).exists

Premises used: ExistsUnique.exists
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
pos : ∀ (ha : a ∈ s), P.part a ∈ P.parts ↔ a ∈ s
neg : ∀ (ha : a ∉ s), P.part a ∈ P.parts ↔ a ∈ s
⊢ P.part a ∈ P.parts ↔ a ∈ s

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ P.part a ∈ P.parts ↔ a ∈ s

Tactic:
simp [part, ha, choose_mem]

Premises used: Finpartition.part, Finset.choose_mem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∉ s
⊢ P.part a ∈ P.parts ↔ a ∈ s

Tactic:
simp [part, ha, choose_mem]

Premises used: Finpartition.part, Finset.choose_mem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
h : a ∉ s
⊢ P.part a = ∅

Tactic:
simp [part, h]

Premises used: Finpartition.part
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
contrapose! : P.part a = ∅ ↔ a ∉ s
⊢ (P.part a).Nonempty ↔ a ∈ s

Tactic:
contrapose!
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
⊢ P.part a = ∅ ↔ a ∉ s

Tactic:
part_eq_empty P

Premises used: Finpartition.part_eq_empty
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
⊢ P.part a = ∅ ↔ a ∉ s

Tactic:
exact part_eq_empty P

Premises used: Finpartition.part_eq_empty
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
pos : ∀ (ha : a ∈ s), P.part a ⊆ s
neg : ∀ (ha : a ∉ s), P.part a ⊆ s
⊢ P.part a ⊆ s

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ P.part a ⊆ s

Tactic:
P.le <| P.part_mem.2 ha

Premises used: Iff.mpr, Finpartition.part_mem, Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ P.part a ⊆ s

Tactic:
exact P.le <| P.part_mem.2 ha

Premises used: Iff.mpr, Finpartition.part_mem, Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∉ s
⊢ P.part a ⊆ s

Tactic:
simp [P.part_eq_empty.2 ha]

Premises used: Iff.mpr, Finpartition.part_eq_empty
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
pos : ∀ (ha : a ∈ s), a ∈ P.part a ↔ a ∈ s
neg : ∀ (ha : a ∉ s), a ∈ P.part a ↔ a ∈ s
⊢ a ∈ P.part a ↔ a ∈ s

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ a ∈ P.part a ↔ a ∈ s

Tactic:
simp [part, ha, choose_property (p := fun s => a ∈ s) P.parts (P.existsUnique_mem ha)]

Premises used: Finpartition.part, Membership.mem, Finpartition.parts, Finpartition.existsUnique_mem, Finset.choose_property
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∉ s
⊢ a ∈ P.part a ↔ a ∈ s

Tactic:
simp [P.part_eq_empty.2, ha]

Premises used: Iff.mpr, Finpartition.part_eq_empty
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
mp : P.part a = t → a ∈ t
mpr : a ∈ t → P.part a = t
⊢ P.part a = t ↔ a ∈ t

Tactic:
constructor
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ht : P.part a ∈ P.parts
⊢ a ∈ P.part a

Tactic:
simp_all
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
mpr : P.part a ∈ P.parts
mpr₁ : t ∈ P.parts
mpr₂ : a ∈ P.part a
mpr₃ : a ∈ t
⊢ P.part a = t

Tactic:
apply P.eq_of_mem_parts (a := a)

Premises used: Finpartition.eq_of_mem_parts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ P.part a ∈ P.parts

Tactic:
simp [*, P.le ht hat]

Premises used: Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ t ∈ P.parts

Tactic:
simp [*, P.le ht hat]

Premises used: Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ a ∈ P.part a

Tactic:
simp [*, P.le ht hat]

Premises used: Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ a ∈ t

Tactic:
simp [*, P.le ht hat]

Premises used: Finpartition.le
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ P.part a = t

Tactic:
(P.part_eq_iff_mem ht).2 hat

Premises used: Iff.mpr, Finpartition.part_eq_iff_mem
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a ∈ P.part b ↔ P.part a = P.part b

Tactic:
⟨fun c ↦ (P.part_eq_of_mem (P.part_mem.2 hb) c), fun c ↦ c ▸ P.mem_part ha⟩

Premises used: Iff.mpr, Finpartition.part_eq_of_mem, Eq.rec, Finpartition.part_mem, Iff.intro, Finpartition.mem_part
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ (↑P.parts : Set (Finset α))
obtain : ∀ (x : α) (hx : x ∈ p), p ∈ P.part '' (↑s : Set α)
⊢ p ∈ P.part '' (↑s : Set α)

Tactic:
obtain ⟨x, hx⟩ := P.nonempty_of_mem_parts hp

Premises used: Finpartition.nonempty_of_mem_parts
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ (↑P.parts : Set (Finset α))
x : α
hx : x ∈ p
⊢ x ∈ s

Tactic:
have hx' := mem_of_subset (P.le hp) hx
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ (↑P.parts : Set (Finset α))
x : α
hx : x ∈ p
hx' : x ∈ s
w : α
left : x ∈ (↑s : Set α)
right : P.part x = p
⊢ p ∈ P.part '' (↑s : Set α)

Tactic:
use x, hx', (P.existsUnique_mem hx').unique ⟨P.part_mem.2 hx', P.mem_part hx'⟩ ⟨hp, hx⟩

Premises used: Iff.mpr, Finpartition.part_mem, And.intro, Finpartition.existsUnique_mem, ExistsUnique.unique, Finpartition.mem_part
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
obtain :
  ∀ (r : Set α) (hrs : r ⊆ (↑s : Set α)) (hr : Set.BijOn P.part r (↑P.parts : Set (Finset α))),
    ∃ r ⊆ s, Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))
⊢ ∃ r ⊆ s, Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))

Tactic:
obtain ⟨r, hrs, hr⟩ := P.part_surjOn.exists_bijOn_subset

Premises used: Set.SurjOn.exists_bijOn_subset, Finpartition.part_surjOn
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
r : Set α
hrs : r ⊆ (↑s : Set α)
hr : Set.BijOn P.part r (↑P.parts : Set (Finset α))
⊢ r.Finite

Tactic:
s.finite_toSet.subset hrs

Premises used: Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
r : Set α
hrs : r ⊆ (↑s : Set α)
hr : Set.BijOn P.part r (↑P.parts : Set (Finset α))
lift :
  ∀ (r : Finset α) (hrs : (↑r : Set α) ⊆ (↑s : Set α)) (hr : Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))),
    ∃ r ⊆ s, Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))
⊢ ∃ r ⊆ s, Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))

Tactic:
lift r to Finset α using s.finite_toSet.subset hrs

Premises used: Finset, Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Order.Partition.Finpartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
r : Finset α
hrs : (↑r : Set α) ⊆ (↑s : Set α)
hr : Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))
⊢ ∃ r ⊆ s, Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))

Tactic:
⟨r, mod_cast hrs, hr⟩

Premises used: SetLike.coe_subset_coe._simp_1, cast, And.intro, Exists.intro