awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
rw : p ((Iic i).sup' ⋯ f) ↔ ∀ j ≤ i, p (f j)
rw₁ : (Iic i).sup' ⋯ (p ∘ f) ↔ ∀ j ≤ i, p (f j)
rw₂ : ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
⊢ p ((partialSups f : (a : ι) → α) i) ↔ ∀ j ≤ i, p (f j)
have rw₃ : (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)
Tactic: classical
  rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
  · change (Iic i).inf (p ∘ f) ↔ _
    simp [Finset.inf_eq_iInf]
  · intro x y
    rw [hp]
    rfl
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
⊢ upperBounds (Set.range.{u_1, u_3 + 1} (ι := ι) (⇑(partialSups f) : (a : ι) → α)) = upperBounds (Set.range f)
have h : ∀ (a : α),
  Membership.mem (γ := Set α) (upperBounds (Set.range.{u_1, u_3 + 1} (ι := ι) (⇑(partialSups f) : (a : ι) → α))) a ↔
    a ∈ upperBounds (Set.range f)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
a : α
⊢ Membership.mem (γ := Set α) (upperBounds (Set.range.{u_1, u_3 + 1} (ι := ι) (⇑(partialSups f) : (a : ι) → α))) a ↔
    a ∈ upperBounds (Set.range f)
have h : (∀ (i j : ι), j ≤ i → f j ≤ a) ↔ ∀ (i : ι), f i ≤ a
Tactic: simp only [mem_upperBounds, Set.forall_mem_range, partialSups_le_iff]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : Preorder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → α
h : (⇑(partialSups f) : (a : ι) → α) ≤ f
⊢ Monotone f
have h₁ : f = (⇑(partialSups f) : (a : ι) → α)
Tactic: convert! (partialSups f).monotone using 1
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : Preorder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → α
g : ι →o α
⊢ partialSups f ≤ g ↔ f ≤ (⇑g : (a : ι) → α)
have refine : ∀ (h : f ≤ (⇑g : (a : ι) → α)), partialSups f ≤ g
Tactic: refine ⟨(le_partialSups f).trans, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : Preorder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → α
g : ι →o α
h : f ≤ (⇑g : (a : ι) → α)
⊢ partialSups f ≤ g
have h₁ : g = partialSups (⇑g : (a : ι) → α)
Tactic: convert! partialSups_mono h
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : Preorder ι
inst_3 : LocallyFiniteOrderBot ι
F : Type u_4
inst_4 : FunLike F α β
inst_5 : SupHomClass F α β
f : ι → α
g : F
⊢ Eq (α := (a : ι) → β) (⇑(partialSups ((⇑g : (a : α) → β) ∘ f)) : (a : ι) → β)
    (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑g : (a : α) → β) (⇑(partialSups f) : (a : ι) → α))
have h : ∀ (x : ι),
  Eq.{u_2 + 1} (α := β) ((partialSups ((⇑g : (a : α) → β) ∘ f) : (a : ι) → β) x : β)
    (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑g : (a : α) → β) (⇑(partialSups f) : (a : ι) → α) x : β)
Tactic: funext _
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i : ι
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (Order.succ i) : α)
    ((partialSups f : (a : ι) → α) i ⊔ f (Order.succ i) : α)
have suffices : Iic (Order.succ i) = Iic i ∪ {Order.succ i}
Tactic: suffices Iic (Order.succ i) = Iic i ∪ {Order.succ i} by simp only [partialSups_apply, this,
    sup'_union nonempty_Iic ⟨_, mem_singleton_self _⟩ f, sup'_singleton]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i : ι
⊢ Iic (Order.succ i) = Iic i ∪ {Order.succ i}
have h : ∀ (a : ι), a ∈ Iic (Order.succ i) ↔ a ∈ Iic i ∪ {Order.succ i}
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i a : ι
⊢ a ∈ Iic (Order.succ i) ↔ a ∈ Iic i ∪ {Order.succ i}
have h : a ≤ Order.succ i ↔ a ≤ i ∨ a = Order.succ i
Tactic: simp only [mem_Iic, mem_union, mem_singleton]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i a : ι
⊢ a ≤ Order.succ i ↔ a ≤ i ∨ a = Order.succ i
have h : a ≤ Order.succ i → a ≤ i ∨ a = Order.succ i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i a : ι
h : a ≤ Order.succ i → a ≤ i ∨ a = Order.succ i
⊢ a ≤ Order.succ i ↔ a ≤ i ∨ a = Order.succ i
have h₁ : a ≤ i ∨ a = Order.succ i → a ≤ Order.succ i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
⊢ (partialSups f : (a : ι) → α) ⊥ = f ⊥
have simp : sup' (Iic ⊥) sorry f = f ⊥
Tactic: simp only [partialSups_apply]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
⊢ sup' (Iic ⊥) ⋯ f = f ⊥
have suffices : Eq (α := Finset ι) (Iic ⊥) {⊥}
Tactic: suffices Iic (⊥ : ι) = {⊥} by simp only [this, sup'_singleton]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) i : α) (⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι) : α)
have simp : (Iic i).sup' sorry f = ⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι)
Tactic: simp only [partialSups_apply]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ (Iic i).sup' ⋯ f = ⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι)
have a : (Iic i).sup' sorry f ≤ ⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
i : ι
a : (Iic i).sup' ⋯ f ≤ ⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι)
⊢ (Iic i).sup' ⋯ f = ⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι)
have a₁ : ⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι) ≤ (Iic i).sup' sorry f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
have pos : ∀ (hι : Nonempty ι), Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
Tactic: by_cases hι : Nonempty ι
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
pos : ∀ (hι : Nonempty ι), Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
have neg : ∀ (hι : ¬Nonempty ι), Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
Tactic: by_cases hι : Nonempty ι
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
have pos : ∀ (i : ι), LE.le.{u_1} (α := α) ((partialSups f : (a : ι) → α) i : α) (⨆ (i : ι), f i : α)
Tactic: refine (ciSup_le fun i ↦ ?_).antisymm (ciSup_mono ?_ <| le_partialSups f)
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
pos : ∀ (i : ι), LE.le.{u_1} (α := α) ((partialSups f : (a : ι) → α) i : α) (⨆ (i : ι), f i : α)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
have pos₁ : BddAbove.{u_1} (α := α) (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i)
Tactic: refine (ciSup_le fun i ↦ ?_).antisymm (ciSup_mono ?_ <| le_partialSups f)
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
have pos : ∀ (h : BddAbove (Set.range f)), Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
Tactic: by_cases h : BddAbove (Set.range f)
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLinearOrder α
f : ι → α
pos :
  ∀ (h : BddAbove (Set.range f)), Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
have neg : ∀ (h : ¬BddAbove (Set.range f)), Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
Tactic: by_cases h : BddAbove (Set.range f)
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
have neg : Eq.{u_1 + 1} (α := α) (sSup (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i)) (⨆ (i : ι), f i)
Tactic: rw [iSup, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,
      ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _
        (bddAbove_range_partialSups.not.mpr h)]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
neg : Eq.{u_1 + 1} (α := α) (sSup (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i)) (⨆ (i : ι), f i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
have neg₁ : Eq.{u_1 + 1} (α := α) (sSup (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i))
  (sSup (Set.range fun (i : ι) ↦ f i))
Tactic: rw [iSup, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,
      ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _
        (bddAbove_range_partialSups.not.mpr h)]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
neg : Eq.{u_1 + 1} (α := α) (sSup (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i)) (⨆ (i : ι), f i)
neg₁ :
  Eq.{u_1 + 1} (α := α) (sSup (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i))
    (sSup (Set.range fun (i : ι) ↦ f i))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
have neg₂ : Eq.{u_1 + 1} (α := α) (sSup (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i)) (sSup ∅)
Tactic: rw [iSup, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,
      ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _
        (bddAbove_range_partialSups.not.mpr h)]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
neg : Eq.{u_1 + 1} (α := α) (sSup (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i)) (⨆ (i : ι), f i)
neg₁ :
  Eq.{u_1 + 1} (α := α) (sSup (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i))
    (sSup (Set.range fun (i : ι) ↦ f i))
neg₂ : Eq.{u_1 + 1} (α := α) (sSup (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i)) (sSup ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)
have neg₃ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
Tactic: rw [iSup, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,
      ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _
        (bddAbove_range_partialSups.not.mpr h)]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : CompleteLattice α
f g : ι → α
h : LE.le (α := ι →o α) (partialSups f) (partialSups g)
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), g i)
have rw : LE.le.{u_1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), (partialSups g : (a : ι) → α) i)
Tactic: rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : CompleteLattice α
f g : ι → α
h : Eq (α := ι →o α) (partialSups f) (partialSups g)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), g i)
have simp_rw : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), g i)
Tactic: simp_rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g, h]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : CompleteLattice α
f g : ι → α
h : Eq (α := ι →o α) (partialSups f) (partialSups g)
simp_rw : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), g i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), g i)
have simp_rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), (partialSups g : (a : ι) → α) i)
Tactic: simp_rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g, h]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i : ι
⊢ ∃ j ≤ i, (partialSups f : (a : ι) → α) i = f j
have obtain : ∀ (j : ι) (hj_mem : j ∈ Iic i) (hj_le : ∀ k ∈ Iic i, f k ≤ f j), ∃ j ≤ i, (partialSups f : (a : ι) → α) i = f j
Tactic: obtain ⟨j, hj_mem, hj_le⟩ : ∃ j ∈ Finset.Iic i, ∀ k ∈ Finset.Iic i, f k ≤ f j :=
    Finset.exists_max_image _ _ ⟨i, Finset.mem_Iic.mpr le_rfl⟩
-- Lean 4 proof step from Mathlib.Order.PartialSups (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ∈ Iic i
hj_le : ∀ k ∈ Iic i, f k ≤ f j
⊢ ∃ j ≤ i, (partialSups f : (a : ι) → α) i = f j
have hj_mem₁ : j ≤ i
Tactic: simp only [Finset.mem_Iic] at hj_mem hj_le
Cleared hypotheses: hj_mem, hj_le
-- Lean 4 proof step from Mathlib.Order.PartialSups (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ∈ Iic i
hj_le : ∀ k ∈ Iic i, f k ≤ f j
hj_mem₁ : j ≤ i
⊢ ∃ j ≤ i, (partialSups f : (a : ι) → α) i = f j
have hj_le₁ : ∀ k ≤ i, f k ≤ f j
Tactic: simp only [Finset.mem_Iic] at hj_mem hj_le
Cleared hypotheses: hj_mem, hj_le
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ ∃ j ≤ i, (partialSups f : (a : ι) → α) i = f j
have right : (partialSups f : (a : ι) → α) i = f j
Tactic: use j, hj_mem
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ (partialSups f : (a : ι) → α) i = f j
have right : (partialSups f : (a : ι) → α) i ≤ f j
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
right : (partialSups f : (a : ι) → α) i ≤ f j
⊢ (partialSups f : (a : ι) → α) i = f j
have right₁ : f j ≤ (partialSups f : (a : ι) → α) i
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s_1 t x y z : α
S : Set α
inst : CompleteLattice α
P Q : Partition s_1
s : α
p p' : Partition s
h : p.parts = p'.parts
⊢ p = p'
have mk : ∀ (parts : Set α) (sSupIndep' : sSupIndep parts) (bot_notMem' : ⊥ ∉ parts) (sSup_eq' : sSup parts = s)
  (h :
    { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s }.parts =
      p'.parts),
  { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s } = p'
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s_1 t x y z : α
S : Set α
inst : CompleteLattice α
P Q : Partition s_1
s : α
p' : Partition s
parts : Set α
sSupIndep' : sSupIndep parts
bot_notMem' : ⊥ ∉ parts
sSup_eq' : sSup parts = s
h :
  { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s }.parts =
    p'.parts
⊢ { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s } = p'
have mk : ∀ (parts_1 : Set α) (sSupIndep'_1 : sSupIndep parts_1) (bot_notMem'_1 : ⊥ ∉ parts_1) (sSup_eq'_1 : sSup parts_1 = s)
  (h :
    { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s }.parts =
      { parts := parts_1, sSupIndep' := sSupIndep'_1, bot_notMem' := bot_notMem'_1, sSup_eq' := sSup_eq'_1 :
          Partition s }.parts),
  { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' : Partition s } =
    { parts := parts_1, sSupIndep' := sSupIndep'_1, bot_notMem' := bot_notMem'_1, sSup_eq' := sSup_eq'_1 }
Tactic: cases p'
Cleared hypotheses: p', h
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s : α
inst : CompleteLattice α
P : Partition s
⊢ ⨆ x ∈ P, x = s
have simp_rw : Eq.{u_1 + 1} (α := α) (⨆ x ∈ P, x) (⨆ a ∈ (↑P : Set α), a)
Tactic: simp_rw [← P.sSup_eq, sSup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (hypothesis)
Goal:
α : Type u_1
inst : CompleteLattice α
P : Partition (α := α) ⊥
x : α
hxP : x ∈ P
⊢ False
have hxP₁ : ⊥ ∈ P
Tactic: obtain rfl := le_bot_iff.mp <| P.le_of_mem hxP
Cleared hypotheses: x, hxP
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s t x y z : α
S : Set α
inst : CompleteLattice α
P_1 Q : Partition s
P : Partition (α := α) ⊥
⊢ P = removeBot ∅ ⋯ ⋯
have hP : ∀ (x : α), x ∈ P ↔ Membership.mem (γ := Partition (α := α) ⊥) (removeBot ∅ sorry sorry) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s t x_1 y z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q R : Partition s
hPQ : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hQR : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ R, x ≤ y
x : α
hxP : x ∈ P
⊢ ∃ y ∈ R, x ≤ y
have obtain : ∀ (y : α) (hy : y ∈ Q) (hxy : x ≤ y), ∃ y ∈ R, x ≤ y
Tactic: obtain ⟨y, hy, hxy⟩ := hPQ hxP
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q R : Partition s
hPQ : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hQR : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ R, x ≤ y
x : α
hxP : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
⊢ ∃ y ∈ R, x ≤ y
have obtain : ∀ (z : α) (hz : z ∈ R) (hyz : y ≤ z), ∃ y ∈ R, x ≤ y
Tactic: obtain ⟨z, hz, hyz⟩ := hQR hy
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s t x y z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
⊢ P = Q
have refine_1 : ∀ (x : α) (h : x ∈ P), x ∈ Q
Tactic: refine Partition.ext fun x ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s t x y z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
refine_1 : ∀ (x : α) (h : x ∈ P), x ∈ Q
⊢ P = Q
have refine_2 : ∀ (x : α) (h : x ∈ Q), x ∈ P
Tactic: refine Partition.ext fun x ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s t x_1 y z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ P
⊢ x ∈ Q
have refine_1 : ∀ (y : α) (hy : y ∈ Q) (hxy : x ≤ y), x ∈ Q
Tactic: obtain ⟨y, hy, hxy⟩ := hp h
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
⊢ x ∈ Q
have refine_1 : ∀ (x' : α) (hx' : x' ∈ P) (hyx' : y ≤ x'), x ∈ Q
Tactic: obtain ⟨x', hx', hyx'⟩ := hq hy
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (hypothesis)
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
x' : α
hx' : x' ∈ P
hyx' : y ≤ x'
hx'₁ : x ∈ P
⊢ x ∈ Q
have hyx'₁ : y ≤ x
Tactic: obtain rfl := P.pairwiseDisjoint.eq_of_le h hx' (P.ne_bot_of_mem h) (hxy.trans hyx')
Cleared hypotheses: x', hx', hyx'
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s t x_1 y z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ Q
⊢ x ∈ P
have refine_2 : ∀ (y : α) (hy : y ∈ P) (hxy : x ≤ y), x ∈ P
Tactic: obtain ⟨y, hy, hxy⟩ := hq h
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (goal)
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ Q
y : α
hy : y ∈ P
hxy : x ≤ y
⊢ x ∈ P
have refine_2 : ∀ (x' : α) (hx' : x' ∈ Q) (hyx' : y ≤ x'), x ∈ P
Tactic: obtain ⟨x', hx', hyx'⟩ := hp hy
-- Lean 4 proof step from Mathlib.Order.Partition.Basic (hypothesis)
Goal:
α : Type u_1
s t x_1 y_1 z : α
S : Set α
inst : CompleteLattice α
P_1 Q_1 P Q : Partition s
hp : ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y
hq : ∀ ⦃x : α⦄, x ∈ Q → ∃ y ∈ P, x ≤ y
x : α
h : x ∈ Q
y : α
hy : y ∈ P
hxy : x ≤ y
x' : α
hx' : x' ∈ Q
hyx' : y ≤ x'
hx'₁ : x ∈ Q
⊢ x ∈ P
have hyx'₁ : y ≤ x
Tactic: obtain rfl := Q.pairwiseDisjoint.eq_of_le h hx' (Q.ne_bot_of_mem h) (hxy.trans hyx')
Cleared hypotheses: x', hx', hyx'