awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ Disjoint (id b) (P.parts.sup id)
have rwa : Disjoint (id b) a
Tactic: rwa [sup_parts, disjoint_comm]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
rwa : Disjoint (id b) a
⊢ Disjoint (id b) (P.parts.sup id)
have rwa₁ : Disjoint a (id b)
Tactic: rwa [sup_parts, disjoint_comm]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ (insert b P.parts).sup id = c
have rwa : id b ⊔ P.parts.sup id = c
Tactic: rwa [sup_insert, P.sup_parts, id, _root_.sup_comm]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
rwa : id b ⊔ P.parts.sup id = c
⊢ (insert b P.parts).sup id = c
have rwa₁ : id b ⊔ a = c
Tactic: rwa [sup_insert, P.sup_parts, id, _root_.sup_comm]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
inst_3 : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
rwa : id b ⊔ P.parts.sup id = c
rwa₁ : id b ⊔ a = c
⊢ (insert b P.parts).sup id = c
have rwa₂ : b ⊔ a = c
Tactic: rwa [sup_insert, P.sup_parts, id, _root_.sup_comm]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b_1 c : α
P : Finpartition a
b : α
⊢ sup (image (fun (x : α) ↦ x \ b) P.parts) id = a \ b
have rw : P.parts.sup (id ∘ fun (x : α) ↦ x \ b) = a \ b
Tactic: rw [sup_image, id_comp, Finset.sup_sdiff_right, ← Function.id_def, P.sup_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ sup (image (fun (x : α) ↦ x \ b) P.parts) id = a \ b
have rw₁ : (P.parts.sup fun (x : α) ↦ x \ b) = a \ b
Tactic: rw [sup_image, id_comp, Finset.sup_sdiff_right, ← Function.id_def, P.sup_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ sup (image (fun (x : α) ↦ x \ b) P.parts) id = a \ b
have rw₂ : (P.parts.sup fun (x : α) ↦ x) \ b = a \ b
Tactic: rw [sup_image, id_comp, Finset.sup_sdiff_right, ← Function.id_def, P.sup_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ sup (image (fun (x : α) ↦ x \ b) P.parts) id = a \ b
have rw₃ : P.parts.sup id \ b = a \ b
Tactic: rw [sup_image, id_comp, Finset.sup_sdiff_right, ← Function.id_def, P.sup_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ sup (image (fun (x : α) ↦ x \ b) P.parts) id = a \ b
have rw₄ : a \ b = a \ b
Tactic: rw [sup_image, id_comp, Finset.sup_sdiff_right, ← Function.id_def, P.sup_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b c : α
P : Finpartition a
⊢ c ∈ (P.avoid b).parts ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c
have simp : (∃ x ∈ P.parts, ¬c = ⊥ ∧ x \ b = c) ↔ ∃ 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 ≠ ⊥)]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
have refine : ∀ (d : α), d \ b = c → (¬c = ⊥ ↔ ¬d ≤ b)
Tactic: refine exists_congr fun d ↦ and_congr_right' <| and_congr_left ?_
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
d : α
⊢ ¬d \ b = ⊥ ↔ ¬d ≤ b
have rw : ¬d ≤ b ↔ ¬d ≤ b
Tactic: rw [sdiff_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a = b
⊢ (P.extendOfLE ⋯).parts = P.parts
have subst : (P.extendOfLE sorry).parts = P.parts
Tactic: subst hab
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
⊢ P.parts ⊆ (P.extendOfLE hab).parts
have unfold : P.parts ⊆
  parts (a := b)
    (if hr : b \ a = ⊥ then Eq.rec (motive := fun (x : α) (h : a = x) ↦ Finpartition x) P sorry else P.extend hr sorry sorry)
Tactic: unfold extendOfLE
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
⊢ 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 ⋯ ⋯)
have pos : ∀ (hr : b \ a = ⊥), P.parts ⊆ parts (a := b) (Eq.rec (motive := fun (x : α) (h : a = x) ↦ Finpartition x) P sorry)
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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 ⋯)
⊢ 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 ⋯ ⋯)
have neg : ∀ (hr : ¬b \ a = ⊥), P.parts ⊆ (P.extend hr sorry sorry).parts
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
hr : b \ a = ⊥
⊢ P.parts ⊆ parts (a := b) (Eq.rec (motive := fun (x : α) (h : a = x) ↦ Finpartition x) P ⋯)
have pos : ∀ (hab : a ≤ a) (hr : a \ a = ⊥), P.parts ⊆ P.parts
Tactic: cases le_antisymm (sdiff_eq_bot_iff.mp hr) hab
Cleared hypotheses: b, hab, hr
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
inst_1 : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
p : α
hp : p ∈ (P.extendOfLE hab).parts
⊢ p ∈ P.parts ∨ p = b \ a
have pos : ∀ (h : a < b), p ∈ P.parts ∨ p = b \ a
Tactic: by_cases h : a < b
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ p ∈ P.parts ∨ p = b \ a
have neg : ∀ (h : ¬a < b), p ∈ P.parts ∨ p = b \ a
Tactic: by_cases h : a < b
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
have neg : p ∈ P.parts
Tactic: left
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ ∃ t ∈ P.parts, a ∈ t
have ha₁ : a ∈ P.parts.sup id
Tactic: simp_rw [← P.sup_parts] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ ∃! t : Finset α, t ∈ P.parts ∧ a ∈ t
have obtain : ∀ (t : Finset α) (ht : t ∈ P.parts) (ht' : a ∈ t), ∃! t : Finset α, t ∈ P.parts ∧ a ∈ t
Tactic: obtain ⟨t, ht, ht'⟩ := P.exists_mem ha
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
have refine : ∀ (y : Finset α), (fun (t : Finset α) ↦ t ∈ P.parts ∧ a ∈ t) y → y = t
Tactic: refine ⟨t, ⟨ht, ht'⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ parts.SupIndep id
have simp : (↑parts : Set (Finset α)).PairwiseDisjoint id
Tactic: simp only [supIndep_iff_pairwiseDisjoint]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ (Disjoint on id) a b
have rw : ∀ ⦃a_2 : α⦄, a_2 ∈ id a → a_2 ∉ id b
Tactic: rw [Function.onFun, Finset.disjoint_left]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ parts.sup id = s
have h₁ : ∀ (i : α), i ∈ parts.sup id ↔ i ∈ s
Tactic: ext i
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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 : α
⊢ i ∈ parts.sup id ↔ i ∈ s
have h₁ : (∃ i_1 ∈ parts, i ∈ i_1) ↔ i ∈ s
Tactic: simp only [mem_sup, id_eq]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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 : α
⊢ (∃ i_1 ∈ parts, i ∈ i_1) ↔ i ∈ s
have h₁ : (∃ i_1 ∈ parts, i ∈ i_1) → i ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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_1 ∈ parts, i ∈ i_1) ↔ i ∈ s
have h₂ : i ∈ s → ∃ i_1 ∈ parts, i ∈ i_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
⊢ P.part a ∈ P.parts ↔ a ∈ s
have pos : ∀ (ha : a ∈ s), P.part a ∈ P.parts ↔ a ∈ s
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
pos : ∀ (ha : a ∈ s), P.part a ∈ P.parts ↔ a ∈ s
⊢ P.part a ∈ P.parts ↔ a ∈ s
have neg : ∀ (ha : a ∉ s), P.part a ∈ P.parts ↔ a ∈ s
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
⊢ (P.part a).Nonempty ↔ a ∈ s
have contrapose! : P.part a = ∅ ↔ a ∉ s
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
⊢ P.part a ⊆ s
have pos : ∀ (ha : a ∈ s), P.part a ⊆ s
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
pos : ∀ (ha : a ∈ s), P.part a ⊆ s
⊢ P.part a ⊆ s
have neg : ∀ (ha : a ∉ s), P.part a ⊆ s
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
⊢ a ∈ P.part a ↔ a ∈ s
have pos : ∀ (ha : a ∈ s), a ∈ P.part a ↔ a ∈ s
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a : α
pos : ∀ (ha : a ∈ s), a ∈ P.part a ↔ a ∈ s
⊢ a ∈ P.part a ↔ a ∈ s
have neg : ∀ (ha : a ∉ s), a ∈ P.part a ↔ a ∈ s
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
⊢ P.part a = t ↔ a ∈ t
have mp : P.part a = t → a ∈ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
mp : P.part a = t → a ∈ t
⊢ P.part a = t ↔ a ∈ t
have mpr : a ∈ t → P.part a = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ P.part a = t
have mpr : P.part a ∈ P.parts
Tactic: apply P.eq_of_mem_parts (a := a)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ P.part a = t
have mpr₂ : a ∈ P.part a
Tactic: apply P.eq_of_mem_parts (a := a)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ (↑P.parts : Set (Finset α))
⊢ p ∈ P.part '' (↑s : Set α)
have obtain : ∀ (x : α) (hx : x ∈ p), p ∈ P.part '' (↑s : Set α)
Tactic: obtain ⟨x, hx⟩ := P.nonempty_of_mem_parts hp
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ (↑P.parts : Set (Finset α))
x : α
hx : x ∈ p
⊢ p ∈ P.part '' (↑s : Set α)
have hx' : x ∈ s
Tactic: have hx' := mem_of_subset (P.le hp) hx
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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 : α
⊢ p ∈ P.part '' (↑s : Set α)
have left : x ∈ (↑s : Set α)
Tactic: use x, hx', (P.existsUnique_mem hx').unique ⟨P.part_mem.2 hx', P.mem_part hx'⟩ ⟨hp, hx⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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 α)
⊢ p ∈ P.part '' (↑s : Set α)
have right : P.part x = p
Tactic: use x, hx', (P.existsUnique_mem hx').unique ⟨P.part_mem.2 hx', P.mem_part hx'⟩ ⟨hp, hx⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∃ r ⊆ s, Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))
have 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 α))
Tactic: obtain ⟨r, hrs, hr⟩ := P.part_surjOn.exists_bijOn_subset
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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 ⊆ s, Set.BijOn P.part (↑r : Set α) (↑P.parts : Set (Finset α))
have 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 α))
Tactic: lift r to Finset α using s.finite_toSet.subset hrs
Cleared hypotheses: r, hrs, hr
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
⊢ a ∈ P.part b ↔ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p
have mp : a ∈ P.part b → ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
mp : a ∈ P.part b → ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p
⊢ a ∈ P.part b ↔ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p
have mpr : (∃ p ∈ P.parts, a ∈ p ∧ b ∈ p) → a ∈ P.part b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
h : a ∈ P.part b
⊢ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p
have this : b ∈ s
Tactic: have : b ∈ s := P.part_nonempty.1 ⟨a, h⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
h : a ∈ P.part b
this : b ∈ s
⊢ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p
have mp : P.part b ∈ P.parts
Tactic: refine ⟨_, ?_, h, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
h : a ∈ P.part b
this : b ∈ s
mp : P.part b ∈ P.parts
⊢ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p
have mp₁ : b ∈ P.part b
Tactic: refine ⟨_, ?_, h, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
p : Finset α
hp : p ∈ P.parts
hap : a ∈ p
hbp : b ∈ p
⊢ a ∈ P.part b
have hp₁ : P.part b ∈ P.parts
Tactic: obtain rfl : P.part b = p := P.part_eq_of_mem hp hbp
Cleared hypotheses: p, hp, hap, hbp
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
p : Finset α
hp : p ∈ P.parts
hap : a ∈ p
hbp : b ∈ p
hp₁ : P.part b ∈ P.parts
hap₁ : a ∈ P.part b
⊢ a ∈ P.part b
have hbp₁ : b ∈ P.part b
Tactic: obtain rfl : P.part b = p := P.part_eq_of_mem hp hbp
Cleared hypotheses: p, hp, hap, hbp
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : (t : ↥P.parts) × ↥(↑t : Finset α)
⊢ (fun (x : ↥s) ↦
        (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
            (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯)
            (Subtype.mk (p := fun (x_1 : α) ↦
              x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯) : Finset α)) (↑x : α)
              ⋯) :
          (t : ↥P.parts) × ↥(↑t : Finset α)))
      ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
          Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) ⋯)
        x) =
    x
have a₁ : ∀ (e : α),
  Membership.mem (γ := Finset α)
      (↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
            ((fun (x : ↥s) ↦
                (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                    (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) sorry)
                    (Subtype.mk (p := fun (x_1 : α) ↦
                      x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) sorry) : Finset α))
                      (↑x : α) sorry) :
                  (t : ↥P.parts) × ↥(↑t : Finset α)))
              ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                  Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) sorry)
                x))) :
        Finset α)
      e ↔
    e ∈ (↑(x.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))) : Finset α)
Tactic: ext e
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : (t : ↥P.parts) × ↥(↑t : Finset α)
e : α
⊢ Membership.mem (γ := Finset α)
      (↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
            ((fun (x : ↥s) ↦
                (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                    (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯)
                    (Subtype.mk (p := fun (x_1 : α) ↦
                      x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) ⋯) : Finset α))
                      (↑x : α) ⋯) :
                  (t : ↥P.parts) × ↥(↑t : Finset α)))
              ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                  Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) ⋯)
                x))) :
        Finset α)
      e ↔
    e ∈ (↑(x.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))) : Finset α)
have a₁ : ∀ (p : Finset α) (mp : p ∈ P.parts) (f : α)
  (mf : f ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp) : Finset α)),
  Membership.mem (γ := Finset α)
      (↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
            ((fun (x : ↥s) ↦
                (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                    (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) sorry)
                    (Subtype.mk (p := fun (x_1 : α) ↦
                      x_1 ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) (P.part (↑x : α)) sorry) : Finset α))
                      (↑x : α) sorry) :
                  (t : ↥P.parts) × ↥(↑t : Finset α)))
              ((fun (x : (t : ↥P.parts) × ↥(↑t : Finset α)) ↦
                  Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(x.snd (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))) : α) sorry)
                (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
                  (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp)
                  (Subtype.mk (p := fun (x : α) ↦
                    x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp) : Finset α)) f mf))))) :
        Finset α)
      e ↔
    e ∈
      (↑(Sigma.fst (β := fun (a : ↥P.parts) ↦ ↥(↑a : Finset α))
            (Sigma.mk (β := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α))
              (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp)
              (Subtype.mk (p := fun (x : α) ↦
                x ∈ (↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p mp) : Finset α)) f mf))) :
        Finset α)
Tactic: obtain ⟨⟨p, mp⟩, ⟨f, mf⟩⟩ := x
Cleared hypotheses: x