awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (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))
g : ↥P.parts ≃ Fin #P.parts
hg :
  ∀ (t : ↥P.parts),
    #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
z : (a : ↥s) → ℕ :=
  fun (a : ↥s) ↦
    #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ)
gl :
  ∀ (a : ↥s),
    (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ) <
      #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
⊢ ∃ (f : ↥s ≃ Fin #s),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
have bij : Function.Bijective z'
Tactic: have bij : z'.Bijective := by
    refine (bijective_iff_injective_and_card z').mpr ⟨fun a b e ↦ ?_, by simp⟩
    simp_rw [z', z, Fin.mk.injEq, mul_comm #P.parts] at e
    haveI : NeZero #P.parts := ⟨((Nat.zero_le _).trans_lt (gl a)).ne'⟩
    change (#P.parts).divModEquiv.symm (_, _) = (#P.parts).divModEquiv.symm (_, _) at e
    simp only [Equiv.apply_eq_iff_eq, Prod.mk.injEq] at e
    apply_fun f
    exact Sigma.ext e.2 <| (Fin.heq_ext_iff (by rw [e.2])).mpr e.1
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (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))
g : ↥P.parts ≃ Fin #P.parts
hg :
  ∀ (t : ↥P.parts),
    #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
z : (a : ↥s) → ℕ :=
  fun (a : ↥s) ↦
    #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ)
gl :
  ∀ (a : ↥s),
    (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ) <
      #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
bij : Function.Bijective z'
⊢ ∃ (f : ↥s ≃ Fin #s),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
have h : ∀ (a b : ↥s),
  P.part (↑a : α) = P.part (↑b : α) ↔
    (↑((Equiv.ofBijective z' bij : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts =
      (↑((Equiv.ofBijective z' bij : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
Tactic: use Equiv.ofBijective _ bij
-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
hs : s ≠ ∅
⊢ IsEquipartition.{u_1} (α := α) (s := s) (indiscrete hs)
have rw : Set.EquitableOn (α := Finset α) {s} Finset.card
Tactic: rw [IsEquipartition, indiscrete_parts, coe_singleton]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : u ⊆ Finset.map (↑e : α ≃ β).toEmbedding P.parts
x : β
hb : x ∈ Finset.map (↑e : α ≃ β).toEmbedding P.parts
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
⊢ x_1 ≤ ⊥
have rw : ∀ (hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts) (x : β)
  (hb : x ∈ Finset.map (↑e : α ≃ β).toEmbedding P.parts) (hbu : x ∉ u) (x_2 : β) (hx : x_2 ≤ id x)
  (hxu : x_2 ≤ u.sup id), x_2 ≤ ⊥
Tactic: rw [← map_symm_subset] at hu
Cleared hypotheses: hu, x, hb, hbu, x_1, hx, hxu
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hb : x ∈ Finset.map (↑e : α ≃ β).toEmbedding P.parts
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
⊢ x_1 ≤ ⊥
have hb₁ : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
Tactic: simp only [mem_map_equiv] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
⊢ x_1 ≤ ⊥
have refine_2 : ∀ (this : LE.le.{u_1} (α := α) ((e.symm : (a : β) → α) x_1 : α) (⊥ : α)), x_1 ≤ ⊥
Tactic: have := P.supIndep hu hb (by simp [hbu]) (map_rel e.symm hx) ?_
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
refine_2 : ∀ (this : LE.le.{u_1} (α := α) ((e.symm : (a : β) → α) x_1 : α) (⊥ : α)), x_1 ≤ ⊥
⊢ x_1 ≤ ⊥
have refine_1 : (e.symm : (a : β) → α) x_1 ≤ (Finset.map (↑e : α ≃ β).symm.toEmbedding u).sup id
Tactic: have := P.supIndep hu hb (by simp [hbu]) (map_rel e.symm hx) ?_
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
this : LE.le.{u_1} (α := α) ((e.symm : (a : β) → α) x_1 : α) (⊥ : α)
⊢ x_1 ≤ ⊥
have this₁ : LE.le.{u_1} (α := α) ((e.symm : (a : β) → α) x_1 : α) ((e.symm : (a : β) → α) ⊥ : α)
Tactic: rw [← e.symm.map_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
⊢ (e.symm : (a : β) → α) x_1 ≤ (Finset.map (↑e : α ≃ β).symm.toEmbedding u).sup id
have h : (Finset.map (↑e : α ≃ β).symm.toEmbedding u).sup id = (e.symm : (a : β) → α) (u.sup id)
Tactic: convert! e.symm.map_rel_iff.mpr hxu
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : Finset.map (↑e : α ≃ β).symm.toEmbedding u ⊆ P.parts
x : β
hbu : x ∉ u
x_1 : β
hx : x_1 ≤ id x
hxu : x_1 ≤ u.sup id
hb : Membership.mem (α := α) P.parts (((↑e : α ≃ β).symm : (a : β) → α) x : α)
⊢ (Finset.map (↑e : α ≃ β).symm.toEmbedding u).sup id = (e.symm : (a : β) → α) (u.sup id)
have h : Eq.{u_1 + 1} (α := α) (u.sup (id ∘ (⇑(↑e : α ≃ β).symm.toEmbedding : (a : β) → α)))
  (u.sup ((⇑e.symm : (a : β) → α) ∘ id))
Tactic: rw [map_finset_sup, sup_map]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ ⊥ ∉ Finset.map (↑e : α ≃ β).toEmbedding P.parts
have rw : (((↑e : α ≃ β).symm : (a : β) → α) ⊥ : α) ∉ P.parts
Tactic: rw [mem_map_equiv]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
β : Type u_2
inst_2 : Lattice β
inst_3 : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ (((↑e : α ≃ β).symm : (a : β) → α) ⊥ : α) ∉ P.parts
have h : Eq.{u_1 + 1} (α := α) (((↑e : α ≃ β).symm : (a : β) → α) ⊥ : α) (⊥ : α)
Tactic: convert! P.bot_notMem
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ False
have refine : ⊥ ∈ P.parts
Tactic: refine P.bot_notMem (?_)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥
have simp_rw : P.parts = ∅ ↔ P.parts.sup id = ⊥
Tactic: simp_rw [← P.sup_parts]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ P.parts.sup id = ⊥
have refine_1 : ∀ (h : P.parts = ∅), P.parts.sup id = ⊥
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ eq_empty_iff_forall_notMem.2 fun b hb ↦ P.bot_notMem ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
refine_1 : ∀ (h : P.parts = ∅), P.parts.sup id = ⊥
⊢ P.parts = ∅ ↔ P.parts.sup id = ⊥
have refine_2 : ∀ (h : P.parts.sup id = ⊥) (b : α) (hb : b ∈ P.parts), ⊥ ∈ P.parts
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ eq_empty_iff_forall_notMem.2 fun b hb ↦ P.bot_notMem ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ P.parts.sup id = ⊥
have refine_1 : Eq.{u_1 + 1} (α := α) (sup ∅ id) ⊥
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : P.parts.sup id = ⊥
b : α
hb : b ∈ P.parts
⊢ ⊥ ∈ P.parts
have refine_2 : id b ∈ P.parts
Tactic: rwa [← le_bot_iff.1 ((le_sup hb).trans h.le)]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
⊢ P.parts.Nonempty ↔ a ≠ ⊥
have contrapose! : P.parts = ∅ ↔ a = ⊥
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
P : Finpartition (α := α) ⊥
⊢ P = default
have parts : ∀ (a : α), a ∈ P.parts ↔ Membership.mem (γ := Finset α) (parts (a := ⊥) default) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
⊢ Nonempty.{u_1 + 1} (Finpartition a)
have pos : ∀ (h : a = ⊥), Nonempty.{u_1 + 1} (Finpartition a)
Tactic: by_cases h : a = ⊥
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
pos : ∀ (h : a = ⊥), Nonempty.{u_1 + 1} (Finpartition a)
⊢ Nonempty.{u_1 + 1} (Finpartition a)
have neg : ∀ (h : ¬a = ⊥), Nonempty.{u_1 + 1} (Finpartition a)
Tactic: by_cases h : a = ⊥
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
⊢ Nonempty.{u_1 + 1} (Finpartition a)
have pos : Nonempty.{u_1 + 1} (Finpartition (α := α) ⊥)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
ha : IsAtom a
P : Finpartition a
⊢ P = indiscrete ⋯
have h : ∀ b ∈ P.parts, b = a
Tactic: have h : ∀ b ∈ P.parts, b = a := fun _ hb ↦
      (ha.le_iff.mp <| P.le hb).resolve_left (P.ne_bot hb)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ b ∈ P.parts, b = a
⊢ P = indiscrete ⋯
have parts : ∀ (b : α), b ∈ P.parts ↔ b ∈ (indiscrete sorry).parts
Tactic: ext b
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
ha : IsAtom a
P : Finpartition a
h : ∀ b ∈ P.parts, b = a
b : α
⊢ b ∈ P.parts ↔ b ∈ (indiscrete ⋯).parts
have parts : b = a → b ∈ P.parts
Tactic: refine Iff.trans ⟨h b, ?_⟩ mem_singleton.symm
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
b : α
P_1 : Finpartition b
ha : IsAtom b
P : Finpartition b
h : ∀ b_1 ∈ P.parts, b_1 = b
⊢ b ∈ P.parts
have parts : ∀ (c : α) (hc : c ∈ P.parts), b ∈ P.parts
Tactic: obtain ⟨c, hc⟩ := P.parts_nonempty ha.1
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P x Q R : Finpartition a
hPQ : x ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x.parts
⊢ ∃ c ∈ R.parts, b ≤ c
have obtain : ∀ (c : α) (hc : c ∈ Q.parts) (hbc : b ≤ c), ∃ c ∈ R.parts, b ≤ c
Tactic: obtain ⟨c, hc, hbc⟩ := hPQ hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P x Q R : Finpartition a
hPQ : x ≤ Q
hQR : Q ≤ R
b : α
hb : b ∈ x.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ ∃ c ∈ R.parts, b ≤ c
have obtain : ∀ (d : α) (hd : d ∈ R.parts) (hcd : c ≤ d), ∃ c ∈ R.parts, b ≤ c
Tactic: obtain ⟨d, hd, hcd⟩ := hQR hc
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
⊢ P = Q
have parts : ∀ (b : α), b ∈ P.parts ↔ b ∈ Q.parts
Tactic: ext b
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
⊢ b ∈ P.parts ↔ b ∈ Q.parts
have parts : ∀ (hb : b ∈ P.parts), b ∈ Q.parts
Tactic: refine ⟨fun hb ↦ ?_, fun hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
parts : ∀ (hb : b ∈ P.parts), b ∈ Q.parts
⊢ b ∈ P.parts ↔ b ∈ Q.parts
have parts₁ : ∀ (hb : b ∈ Q.parts), b ∈ P.parts
Tactic: refine ⟨fun hb ↦ ?_, fun hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
⊢ b ∈ Q.parts
have parts : ∀ (c : α) (hc : c ∈ Q.parts) (hbc : b ≤ c), b ∈ Q.parts
Tactic: obtain ⟨c, hc, hbc⟩ := hPQ hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
⊢ b ∈ Q.parts
have parts : ∀ (d : α) (hd : d ∈ P.parts) (hcd : c ≤ d), b ∈ Q.parts
Tactic: obtain ⟨d, hd, hcd⟩ := hQP hc
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ b ∈ Q.parts
have parts : c ≤ b
Tactic: rwa [hbc.antisymm]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
⊢ b ∈ P.parts
have parts : ∀ (c : α) (hc : c ∈ P.parts) (hbc : b ≤ c), b ∈ P.parts
Tactic: obtain ⟨c, hc, hbc⟩ := hQP hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
⊢ b ∈ P.parts
have parts : ∀ (d : α) (hd : d ∈ Q.parts) (hcd : c ≤ d), b ∈ P.parts
Tactic: obtain ⟨d, hd, hcd⟩ := hPQ hc
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ b ∈ P.parts
have parts : c ≤ b
Tactic: rwa [hbc.antisymm]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : Decidable (a = ⊥)
P : Finpartition a
⊢ P ≤ if ha : a = ⊥ then copy (Finpartition.empty α) ⋯ else indiscrete ha
have pos : ∀ (h : a = ⊥), P ≤ copy (Finpartition.empty α) sorry
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : Decidable (a = ⊥)
P : Finpartition a
pos : ∀ (h : a = ⊥), P ≤ copy (Finpartition.empty α) ⋯
⊢ P ≤ if ha : a = ⊥ then copy (Finpartition.empty α) ⋯ else indiscrete ha
have neg : ∀ (h : ¬a = ⊥), P ≤ indiscrete h
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
inst_2 : Decidable (a = ⊥)
b : α
hb : Membership.mem (γ := Finset α) (parts (a := a) ⊤) b
⊢ Membership.mem (γ := Finset α) {a} b
have hb₁ : Membership.mem (γ := Finset α) (parts (a := a) (if ha : a = ⊥ then copy (Finpartition.empty α) sorry else indiscrete ha)) b
Tactic: have hb : b ∈ Finpartition.parts (dite _ _ _) := hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
inst_2 : Decidable (a = ⊥)
b : α
hb_1 : Membership.mem (γ := Finset α) (parts (a := a) ⊤) b
hb :
  Membership.mem (γ := Finset α) (parts (a := a) (if ha : a = ⊥ then copy (Finpartition.empty α) ⋯ else indiscrete ha))
    b
⊢ Membership.mem (γ := Finset α) {a} b
have pos : ∀ (h : a = ⊥) (hb : b ∈ (copy (Finpartition.empty α) sorry).parts), Membership.mem (γ := Finset α) {a} b
Tactic: split_ifs at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
inst_2 : Decidable (a = ⊥)
b : α
hb_1 : Membership.mem (γ := Finset α) (parts (a := a) ⊤) b
hb :
  Membership.mem (γ := Finset α) (parts (a := a) (if ha : a = ⊥ then copy (Finpartition.empty α) ⋯ else indiscrete ha))
    b
pos : ∀ (h : a = ⊥) (hb : b ∈ (copy (Finpartition.empty α) ⋯).parts), Membership.mem (γ := Finset α) {a} b
⊢ Membership.mem (γ := Finset α) {a} b
have neg : ∀ (h : ¬a = ⊥) (hb : b ∈ (indiscrete h).parts), Membership.mem (γ := Finset α) {a} b
Tactic: split_ifs at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
⊢ Membership.mem (γ := Finset (Finpartition s))
    (image
      (fun (ps : Finset (Finset α)) ↦
        if h : ps.sup id = s ∧ ⊥ ∉ ps ∧ ps.SupIndep id then
          { parts := ps, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
        else ⊤)
      s.powerset.powerset)
    P
have refine_1 : P.parts ∈ s.powerset.powerset
Tactic: refine mem_image.mpr ⟨P.parts, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
refine_1 : P.parts ∈ s.powerset.powerset
⊢ Membership.mem (γ := Finset (Finpartition s))
    (image
      (fun (ps : Finset (Finset α)) ↦
        if h : ps.sup id = s ∧ ⊥ ∉ ps ∧ ps.SupIndep id then
          { parts := ps, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
        else ⊤)
      s.powerset.powerset)
    P
have refine_2 : (if h : P.parts.sup id = s ∧ ⊥ ∉ P.parts ∧ P.parts.SupIndep id then
    { parts := P.parts, supIndep := sorry, sup_parts := sorry, bot_notMem := sorry }
  else ⊤) =
  P
Tactic: refine mem_image.mpr ⟨P.parts, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P.parts ∈ s.powerset.powerset
have refine_1 : P.parts ⊆ s.powerset
Tactic: rw [mem_powerset]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a : α
P_1 : Finpartition a
inst_2 : DecidableEq α
s : Finset α
P : Finpartition s
p : Finset α
hp : p ∈ P.parts
⊢ p ∈ s.powerset
have refine_1 : p ⊆ s
Tactic: rw [mem_powerset]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
⊢ ∃ c ∈ P.parts, c ≤ b
have by_contra : ∀ (H : ¬∃ c ∈ P.parts, c ≤ b), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ False
have refine : Disjoint b a
Tactic: refine Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) ?_)
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ Disjoint b a
have this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
Tactic: have : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q := by grind [h _]
-- Lean 4 proof step from Mathlib.Order.Partition.Finpartition (hypothesis)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
this : ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q
⊢ Disjoint b a
have this₁ : P.parts.sup id ≤ (Q.parts.erase b).sup id
Tactic: have : P.parts.sup id ≤ (Q.parts.erase b).sup id := by grind [Finset.le_sup, Finset.sup_le_iff]