awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a e : α
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 : α)) ⋯)
                    (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 α))) : α) ⋯)
                (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 α)
have a₁ : e ∈ P.part f ↔ e ∈ p
Tactic: dsimp only at mf ⊢
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Finset α
P : Finpartition s
a e : α
p : Finset α
mp : p ∈ P.parts
f : α
mf : f ∈ p
⊢ e ∈ P.part f ↔ e ∈ p
have a₁ : e ∈ p ↔ e ∈ p
Tactic: rw [P.part_eq_of_mem mp mf]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∃ (f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        Eq.{u_1 + 1} (α := ↥P.parts)
          (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
          (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))
have h : ∀ (a b : ↥s),
  P.part (↑a : α) = P.part (↑b : α) ↔
    Eq.{u_1 + 1} (α := ↥P.parts)
      (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
        ((P.equivSigmaParts.trans
              (Equiv.sigmaCongr (β₁ := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α)) (β₂ := fun (t : ↥P.parts) ↦
                Fin #(↑t : Finset α)) (Equiv.refl ↥P.parts) fun (t : ↥P.parts) ↦ (↑t : Finset α).equivFin) :
            (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α))
          a))
      (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
        ((P.equivSigmaParts.trans
              (Equiv.sigmaCongr (β₁ := fun (t : ↥P.parts) ↦ ↥(↑t : Finset α)) (β₂ := fun (t : ↥P.parts) ↦
                Fin #(↑t : Finset α)) (Equiv.refl ↥P.parts) fun (t : ↥P.parts) ↦ (↑t : Finset α).equivFin) :
            (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α))
          b))
Tactic: use P.equivSigmaParts.trans ((Equiv.refl _).sigmaCongr (fun t ↦ t.1.equivFin))
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∑ i ∈ P.parts, #i = #s
have h : ∑ i ∈ P.parts, #i = #(P.parts.biUnion id)
Tactic: convert! congr_arg Finset.card P.biUnion_parts
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∑ i ∈ P.parts, #i = #(P.parts.biUnion id)
have h : Eq (α := ℕ) (∑ i ∈ P.parts, #i) (∑ u ∈ P.parts, #(id u))
Tactic: rw [card_biUnion P.supIndep.pairwiseDisjoint]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
⊢ (↑(Finset.map { toFun := singleton, inj' := ⋯ : α ↪ Finset α } s) : Set (Finset α)).PairwiseDisjoint id
have rw : Set.PairwiseDisjoint (α := Finset α)
  ((⇑{ toFun := singleton, inj' := sorry : α ↪ Finset α } : (a : α) → Finset α) '' (↑s : Set α)) id
Tactic: rw [Finset.coe_map]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
⊢ (Finset.map { toFun := singleton, inj' := ⋯ : α ↪ Finset α } s).sup id = s
have rw : s.sup (id ∘ (⇑{ toFun := singleton, inj' := sorry : α ↪ Finset α } : (a : α) → Finset α)) = s
Tactic: rw [sup_map, id_comp, Embedding.coeFn_mk, Finset.sup_singleton_eq_self]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
rw : s.sup (id ∘ (⇑{ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α)) = s
⊢ (Finset.map { toFun := singleton, inj' := ⋯ : α ↪ Finset α } s).sup id = s
have rw₁ : s.sup (⇑{ toFun := singleton, inj' := sorry : α ↪ Finset α } : (a : α) → Finset α) = s
Tactic: rw [sup_map, id_comp, Embedding.coeFn_mk, Finset.sup_singleton_eq_self]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
rw : s.sup (id ∘ (⇑{ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α)) = s
rw₁ : s.sup (⇑{ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α) = s
⊢ (Finset.map { toFun := singleton, inj' := ⋯ : α ↪ Finset α } s).sup id = s
have rw₂ : s.sup singleton = s
Tactic: rw [sup_map, id_comp, Embedding.coeFn_mk, Finset.sup_singleton_eq_self]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P : Finpartition s_1
a : α
s : Finset α
rw : s.sup (id ∘ (⇑{ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α)) = s
rw₁ : s.sup (⇑{ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α) = s
rw₂ : s.sup singleton = s
⊢ (Finset.map { toFun := singleton, inj' := ⋯ : α ↪ Finset α } s).sup id = s
have rw₃ : s = s
Tactic: rw [sup_map, id_comp, Embedding.coeFn_mk, Finset.sup_singleton_eq_self]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P_1 : Finpartition s_1
a : α
s : Finset α
P : Finpartition s
t : Finset α
ht : Membership.mem (γ := Finset (Finset α)) (parts (a := s) ⊥) t
⊢ ∃ c ∈ P.parts, t ≤ c
have ht₁ : ∃ a ∈ s, {a} = t
Tactic: rw [mem_bot_iff] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t_1 u : Finset α
P_1 : Finpartition s_1
a : α
s : Finset α
P : Finpartition s
t : Finset α
ht : ∃ a ∈ s, {a} = t
⊢ ∃ c ∈ P.parts, t ≤ c
have obtain : ∀ (a : α) (ha : a ∈ s), ∃ c ∈ P.parts, {a} ≤ c
Tactic: obtain ⟨a, ha, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 t u : Finset α
P_1 : Finpartition s_1
a_1 : α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ ∃ c ∈ P.parts, {a} ≤ c
have obtain : ∀ (t : Finset α) (ht : t ∈ P.parts) (hat : a ∈ t), ∃ c ∈ P.parts, {a} ≤ c
Tactic: obtain ⟨t, ht, hat⟩ := 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
⊢ #P.parts ≤ #s
have rw : #P.parts ≤ card.{u_1} (α := Finset α) (parts (a := s) ⊥)
Tactic: rw [← card_bot s]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
⊢ #s % #P.parts ≤ #P.parts
have inl : ∀ (h : #P.parts = 0), #s % #P.parts ≤ #P.parts
Tactic: obtain h | h := (#P.parts).eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
inl : ∀ (h : #P.parts = 0), #s % #P.parts ≤ #P.parts
⊢ #s % #P.parts ≤ #P.parts
have inr : ∀ (h : #P.parts > 0), #s % #P.parts ≤ #P.parts
Tactic: obtain h | h := (#P.parts).eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % #P.parts ≤ #P.parts
have inl : #s % 0 ≤ 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % 0 ≤ 0
have h₁ : #s = 0
Tactic: rw [Finset.card_eq_zero, parts_eq_empty_iff, bot_eq_empty, ← Finset.card_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
h : #s = 0
⊢ #s % 0 ≤ 0
have inl : HMod.hMod (α := ℕ) 0 0 ≤ HMod.hMod (α := ℕ) 0 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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)
⊢ SupIndep (α := Finset α) (image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x) id
have simp : ∀ a ∈ x,
  ∀ a_2 ∈ x,
    ∀ (x_1 : α) (x_2 : x_1 ∈ x) (x_3 : α) (x_4 : x_3 ∈ x) (x_5 : (s : α → α → Prop) a x_3) (x : x_3 ∈ x)
      (h : (s : α → α → Prop) a_2 x_3), (s : α → α → Prop) a x_1 ↔ (s : α → α → Prop) a_2 x_1
Tactic: 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]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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)
⊢ SupIndep (α := Finset α) (image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x) id
have suffices : ∀ (a b c d : α), (s : α → α → Prop) a d → (s : α → α → Prop) b d → ((s : α → α → Prop) a c ↔ (s : α → α → Prop) b c)
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) ·)⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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)
⊢ sup (image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x) id = x
have h : ∀ (a : α), Membership.mem (γ := Finset α) (sup (image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x) id) a ↔ a ∈ x
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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 : α
⊢ Membership.mem (γ := Finset α) (sup (image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x) id) a ↔ a ∈ x
have h : (∃ i ∈ x, a ∈ x ∧ (s : α → α → Prop) i a) ↔ a ∈ x
Tactic: simp_rw [sup_image, id_comp, mem_sup, mem_filter]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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 : a ∈ x
w : α
⊢ ∃ i ∈ x, a ∈ x ∧ (s : α → α → Prop) i a
have h : a ∈ x ∧ a ∈ x ∧ (s : α → α → Prop) a a
Tactic: use a
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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)
⊢ ⊥ ∉ image (fun (a : α) ↦ {b ∈ x | (s : α → α → Prop) a b}) x
have suffices : ∀ x₁ ∈ x, ∃ x₂ ∈ x, (s : α → α → Prop) x₁ x₂
Tactic: suffices ∀ x₁ ∈ x, ∃ x₂ ∈ x, s x₁ x₂ by simpa [filter_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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 : x ∈ x_1
w : α
⊢ ∃ x₂ ∈ x_1, (s : α → α → Prop) x x₂
have h : x ∈ x_1 ∧ (s : α → α → Prop) x x
Tactic: use x
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Setoid α
x : Finset α
inst_1 : DecidableRel (α := α) (⇑s : α → α → Prop)
b : α
⊢ b ∈ part (ofSetSetoid s x) a ↔ a ∈ x ∧ b ∈ x ∧ (s : α → α → Prop) a b
have suffices : (∃ a₁ ∈ x, (b ∈ x ∧ (s : α → α → Prop) a₁ b) ∧ a ∈ x ∧ (s : α → α → Prop) a₁ 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]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
inst_1 : Fintype α
s : Setoid α
inst_2 : DecidableRel (α := α) (⇑s : α → α → Prop)
b : α
⊢ b ∈ part (s := univ) (ofSetoid s) a ↔ (s : α → α → Prop) a b
have suffices : b ∈ part (s := univ) (ofSetSetoid s univ) a ↔
  Membership.mem (γ := Finset α) univ a ∧ Membership.mem (γ := Finset α) univ b ∧ (s : α → α → Prop) a b
Tactic: suffices b ∈ (ofSetSetoid s univ).part a ↔ a ∈ univ ∧ b ∈ univ ∧ s a b by simpa
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ x = y
have 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
Tactic: rw [mem_coe, mem_image] at hx hy
Cleared hypotheses: hx, y, hy, h, z, hz1, hz2
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ x = y
have 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
Tactic: obtain ⟨Q, hQ, rfl⟩ := hx
Cleared hypotheses: x, hx, h, hz1
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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})
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = y
have 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}
Tactic: obtain ⟨R, hR, rfl⟩ := hy
Cleared hypotheses: y, hy, hz2, h
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
have 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}
Tactic: subst h'
Cleared hypotheses: R, hR, hz2, h, h'
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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}
⊢ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} = {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
have suffices : Q = R
Tactic: suffices h' : Q = R by
              subst h'
              exact of_eq_true (eq_self {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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}
⊢ Q = R
have 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
Tactic: rw [id, mem_filter] at hz1 hz2
Cleared hypotheses: hz1, R, hR, hz2, h
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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}
⊢ Q = R
have 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
Tactic: rw [mem_powerset] at hQ hR
Cleared hypotheses: hQ, hz1, R, hR, hz2, h
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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}
⊢ Q = R
have h₁ : ∀ (i : Finset α), i ∈ Q ↔ i ∈ R
Tactic: ext i
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
have h₁ : ∀ (hi : i ∈ Q), i ∈ R
Tactic: refine ⟨fun hi ↦ ?_, fun hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ i ∈ Q ↔ i ∈ R
have h₂ : ∀ (hi : i ∈ R), i ∈ Q
Tactic: refine ⟨fun hi ↦ ?_, fun hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ i ∈ R
have h₁ : z ∈ i
Tactic: rwa [hz2.2 _ (hQ hi), ← hz1.2 _ (hQ hi)]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ i ∈ Q
have h₁ : z ∈ i
Tactic: rwa [hz1.2 _ (hR hi), ← hz2.2 _ (hR hi)]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
have 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
Tactic: refine (Finset.sup_le fun t ht ↦ ?_).antisymm fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
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
⊢ sup (image (fun (Q : Finset (Finset α)) ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) id = s
have 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
Tactic: refine (Finset.sup_le fun t ht ↦ ?_).antisymm fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
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
⊢ id t ≤ s
have ht₁ : ∃ a ∈ F.powerset, {i ∈ s | ∀ t ∈ F, t ∈ a ↔ i ∈ t} = t
Tactic: rw [mem_image] at ht
Cleared hypotheses: ht