awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.PartialSups
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.{u_3, u_1} (α := ι) (β := α) (⇑(partialSups f) : (a : ι) → α)

Tactic:
(partialSups f).monotone

Premises used: OrderHom.monotone, partialSups
-- Module: Mathlib.Order.PartialSups
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
h₁ : f = (⇑(partialSups f) : (a : ι) → α)
⊢ Monotone f

Tactic:
convert! (partialSups f).monotone using 1

Premises used: OrderHom.monotone, partialSups
-- Module: Mathlib.Order.PartialSups
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
⊢ f = (⇑(partialSups f) : (a : ι) → α)

Tactic:
(le_partialSups f).antisymm h

Premises used: LE.le.antisymm, le_partialSups
-- Module: Mathlib.Order.PartialSups
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
⊢ f = (⇑(partialSups f) : (a : ι) → α)

Tactic:
exact (le_partialSups f).antisymm h

Premises used: LE.le.antisymm, le_partialSups
-- Module: Mathlib.Order.PartialSups
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 : ι) → α)

Tactic:
⟨(le_partialSups f).trans, fun h ↦ ?_⟩

Premises used: Iff.intro, LE.le.trans, le_partialSups
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : Preorder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → α
g : ι →o α
refine : ∀ (h : f ≤ (⇑g : (a : ι) → α)), partialSups f ≤ g
⊢ partialSups f ≤ g ↔ f ≤ (⇑g : (a : ι) → α)

Tactic:
refine ⟨(le_partialSups f).trans, fun h ↦ ?_⟩
-- Module: Mathlib.Order.PartialSups
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 : ι) → α)
⊢ LE.le (α := ι →o α) (partialSups f) (partialSups (⇑g : (a : ι) → α))

Tactic:
partialSups_mono h

Premises used: partialSups_mono
-- Module: Mathlib.Order.PartialSups
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 : ι) → α)
h₁ : g = partialSups (⇑g : (a : ι) → α)
⊢ partialSups f ≤ g

Tactic:
convert! partialSups_mono h

Premises used: partialSups_mono
-- Module: Mathlib.Order.PartialSups
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 : ι) → α)
⊢ g = partialSups (⇑g : (a : ι) → α)

Tactic:
OrderHom.ext _ _ g.monotone.partialSups_eq.symm

Premises used: OrderHom.monotone, OrderHom.ext, Monotone.partialSups_eq, Eq.symm
-- Module: Mathlib.Order.PartialSups
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 : ι) → α)
⊢ g = partialSups (⇑g : (a : ι) → α)

Tactic:
exact OrderHom.ext _ _ g.monotone.partialSups_eq.symm

Premises used: OrderHom.monotone, OrderHom.ext, Monotone.partialSups_eq, Eq.symm
-- Module: Mathlib.Order.PartialSups
Goal:
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
τ : Type u_4
π : τ → Type u_5
inst_2 : (t : τ) → SemilatticeSup (π t)
f : ι → (t : τ) → π t
i : ι
t : τ
⊢ Eq.{u_5 + 1} (α := π t) ((partialSups f : (a : ι) → (t : τ) → π t) i t : π t)
    ((partialSups fun (x : ι) ↦ f x t : (a : ι) → π t) i : π t)

Tactic:
simp only [partialSups_apply, Finset.sup'_apply]

Premises used: partialSups_apply, Finset.sup'_apply
-- Module: Mathlib.Order.PartialSups
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
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 : β)
⊢ Eq (α := (a : ι) → β) (⇑(partialSups ((⇑g : (a : α) → β) ∘ f)) : (a : ι) → β)
    (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑g : (a : α) → β) (⇑(partialSups f) : (a : ι) → α))

Tactic:
funext _
-- Module: Mathlib.Order.PartialSups
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
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:
simp [partialSups]

Premises used: partialSups
-- Module: Mathlib.Order.PartialSups
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 : F
g : ι → α
i : ι
⊢ Eq.{u_2 + 1} (α := β) ((partialSups fun (j : ι) ↦ (f : (a : α) → β) (g j) : (a : ι) → β) i : β)
    ((f : (a : α) → β) ((partialSups g : (a : ι) → α) i : α) : β)

Tactic:
congr($(comp_partialSups ..) i)

Premises used: comp_partialSups, id, congrFun
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i : ι
this : Iic (Order.succ i) = Iic i ∪ {Order.succ i}
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (Order.succ i) : α)
    ((partialSups f : (a : ι) → α) i ⊔ f (Order.succ i) : α)

Tactic:
simp only [partialSups_apply, this,
    sup'_union nonempty_Iic ⟨_, mem_singleton_self _⟩ f, sup'_singleton]

Premises used: partialSups_apply, Finset.mem_singleton_self, Finset.sup'_singleton, Exists.intro, Finset.sup'_union, Finset.nonempty_Iic
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i : ι
suffices : Iic (Order.succ i) = Iic i ∪ {Order.succ i}
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) (Order.succ i) : α)
    ((partialSups f : (a : ι) → α) i ⊔ f (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]
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i : ι
h : ∀ (a : ι), a ∈ Iic (Order.succ i) ↔ a ∈ Iic i ∪ {Order.succ i}
⊢ Iic (Order.succ i) = Iic i ∪ {Order.succ i}

Tactic:
ext
-- Module: Mathlib.Order.PartialSups
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 ∈ Iic (Order.succ i) ↔ a ∈ Iic i ∪ {Order.succ i}

Tactic:
simp only [mem_Iic, mem_union, mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_Iic, Finset.mem_union
-- Module: Mathlib.Order.PartialSups
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
h₁ : a ≤ i ∨ a = Order.succ i → a ≤ Order.succ i
⊢ a ≤ Order.succ i ↔ a ≤ i ∨ a = Order.succ i

Tactic:
constructor
-- Module: Mathlib.Order.PartialSups
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

Tactic:
fun h ↦ (Order.le_succ_iff_eq_or_le.mp h).symm

Premises used: Or.symm, Iff.mp, Order.le_succ_iff_eq_or_le
-- Module: Mathlib.Order.PartialSups
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

Tactic:
exact fun h ↦ (Order.le_succ_iff_eq_or_le.mp h).symm

Premises used: Or.symm, Iff.mp, Order.le_succ_iff_eq_or_le
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i a : ι
⊢ a ≤ i ∨ a = Order.succ i → a ≤ Order.succ i

Tactic:
fun h ↦ h.elim (le_trans · <| Order.le_succ _) le_of_eq

Premises used: Order.le_succ, le_of_eq, Or.elim, le_trans
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : LinearOrder ι
inst_2 : LocallyFiniteOrderBot ι
inst_3 : SuccOrder ι
f : ι → α
i a : ι
⊢ a ≤ i ∨ a = Order.succ i → a ≤ Order.succ i

Tactic:
exact fun h ↦ h.elim (le_trans · <| Order.le_succ _) le_of_eq
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
simp : sup' (Iic ⊥) ⋯ f = f ⊥
⊢ (partialSups f : (a : ι) → α) ⊥ = f ⊥

Tactic:
simp only [partialSups_apply]

Premises used: partialSups_apply
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
this : Eq (α := Finset ι) (Iic ⊥) {⊥}
⊢ sup' (Iic ⊥) ⋯ f = f ⊥

Tactic:
simp only [this, sup'_singleton]

Premises used: Finset.sup'_singleton
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
suffices : Eq (α := Finset ι) (Iic ⊥) {⊥}
⊢ sup' (Iic ⊥) ⋯ f = f ⊥

Tactic:
suffices Iic (⊥ : ι) = {⊥} by simp only [this, sup'_singleton]
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : PartialOrder ι
inst_2 : LocallyFiniteOrder ι
inst_3 : OrderBot ι
f : ι → α
⊢ Eq (α := Finset ι) (Iic ⊥) {⊥}

Tactic:
simp only [← coe_eq_singleton, coe_Iic, Set.Iic_bot]

Premises used: Finset.coe_eq_singleton, Finset.coe_Iic, Set.Iic_bot
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
inst : SemilatticeSup α
f : ℕ → α
⊢ (partialSups f : (a : ℕ) → α) 0 = f 0

Tactic:
partialSups_bot f

Premises used: partialSups_bot
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
inst : SemilatticeSup α
f : ℕ → α
n : ℕ
x : α
⊢ (partialSups f : (a : ℕ) → α) n ≤ x ↔ (range (n + 1)).sup' ⋯ f ≤ x

Tactic:
simp [Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
f : ℕ → α
n : ℕ
x : α
⊢ (partialSups f : (a : ℕ) → α) n ≤ x ↔ (range (n + 1)).sup f ≤ x

Tactic:
simp [Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : DistribLattice α
inst_3 : OrderBot α
f : ι → α
i : ι
x : α
⊢ Disjoint ((partialSups f : (a : ι) → α) i) x ↔ ∀ j ≤ i, Disjoint (f j) x

Tactic:
partialSups_iff_forall (Disjoint · x) disjoint_sup_left

Premises used: Disjoint, partialSups_iff_forall, disjoint_sup_left
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : DistribLattice α
inst_3 : OrderBot α
f : ι → α
i : ι
x : α
⊢ Disjoint x ((partialSups f : (a : ι) → α) i) ↔ ∀ j ≤ i, Disjoint x (f j)

Tactic:
partialSups_iff_forall (Disjoint x) disjoint_sup_right

Premises used: disjoint_sup_right, Disjoint, partialSups_iff_forall
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : DistribLattice α
inst_3 : OrderBot α
f : ι → α
h : Pairwise (Disjoint on f)
i j : ι
hij : i < j
⊢ Disjoint ((partialSups f : (a : ι) → α) i) (f j)

Tactic:
disjoint_partialSups_left.2 fun _ hk ↦ h (hk.trans_lt hij).ne

Premises used: Iff.mpr, disjoint_partialSups_left, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
i : ι
simp : (Iic i).sup' ⋯ f = ⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι)
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) i : α) (⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι) : α)

Tactic:
simp only [partialSups_apply]

Premises used: partialSups_apply
-- Module: Mathlib.Order.PartialSups
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 : ι)
a₁ : ⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι) ≤ (Iic i).sup' ⋯ f
⊢ (Iic i).sup' ⋯ f = ⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
i j : ι
hj : j ∈ Iic i
⊢ j ∈ Set.Iic i

Tactic:
simpa only [Set.mem_Iic, mem_Iic] using hj

Premises used: Finset.mem_Iic, Set.mem_Iic
-- Module: Mathlib.Order.PartialSups
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 : ι)

Tactic:
exact sup'_le _ _ fun j hj ↦ Finite.le_ciSup_of_le
      ⟨j, by simpa only [Set.mem_Iic, mem_Iic] using hj⟩ le_rfl

Premises used: Finset.sup'_le, Finite.le_ciSup_of_le
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
i : ι
x : (↑(Set.Iic i) : Type u_3)
j : ι
hj : j ∈ Set.Iic i
⊢ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Iic i) j hj) : ι) ∈ Iic i

Tactic:
simpa only [mem_Iic, Set.mem_Iic] using hj

Premises used: Finset.mem_Iic, Set.mem_Iic
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨆ (i_1 : (↑(Set.Iic i) : Type u_3)), f (↑i_1 : ι) ≤ (Iic i).sup' ⋯ f

Tactic:
exact ciSup_le fun ⟨j, hj⟩ ↦ le_sup' f (by simpa only [mem_Iic, Set.mem_Iic] using hj)

Premises used: ciSup_le
-- Module: Mathlib.Order.PartialSups
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)
neg : ∀ (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)

Tactic:
by_cases hι : Nonempty ι

Premises used: Nonempty
-- Module: Mathlib.Order.PartialSups
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)

Tactic:
(ciSup_le fun i ↦ ?_).antisymm (ciSup_mono ?_ <| le_partialSups f)

Premises used: LE.le.antisymm, le_partialSups, ciSup_le, ciSup_mono
-- Module: Mathlib.Order.PartialSups
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 : α)
pos₁ : BddAbove.{u_1} (α := α) (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)

Tactic:
refine (ciSup_le fun i ↦ ?_).antisymm (ciSup_mono ?_ <| le_partialSups f)

Premises used: LE.le.antisymm, le_partialSups, ciSup_le, ciSup_mono
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
i : ι
⊢ LE.le.{u_1} (α := α) ((partialSups f : (a : ι) → α) i : α) (⨆ (i : ι), f i : α)

Tactic:
simpa only [partialSups_eq_ciSup_Iic] using ciSup_le fun i ↦ le_ciSup h _

Premises used: le_ciSup, partialSups_eq_ciSup_Iic, ciSup_le
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
pos pos₁ pos₂ pos₃ : BddAbove (Set.range f)
⊢ BddAbove.{u_1} (α := α) (Set.range fun (i : ι) ↦ (partialSups f : (a : ι) → α) i)

Tactic:
rwa [bddAbove_range_partialSups]

Premises used: bddAbove_range_partialSups
-- Module: Mathlib.Order.PartialSups
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)

Tactic:
congr_arg _ (funext (not_nonempty_iff.mp hι).elim)

Premises used: IsEmpty.elim, congr_arg, not_nonempty_iff, funext, Iff.mp
-- Module: Mathlib.Order.PartialSups
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)

Tactic:
exact congr_arg _ (funext (not_nonempty_iff.mp hι).elim)

Premises used: IsEmpty.elim, congr_arg, not_nonempty_iff, funext, Iff.mp
-- Module: Mathlib.Order.PartialSups
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)
neg :
  ∀ (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)

Tactic:
by_cases h : BddAbove (Set.range f)

Premises used: BddAbove, Set.range
-- Module: Mathlib.Order.PartialSups
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)

Tactic:
ciSup_partialSups_eq h

Premises used: ciSup_partialSups_eq
-- Module: Mathlib.Order.PartialSups
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)

Tactic:
exact ciSup_partialSups_eq h

Premises used: ciSup_partialSups_eq
-- Module: Mathlib.Order.PartialSups
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 ∅)
neg₃ neg₄ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (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)]

Premises used: Iff.mpr, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove, Iff.not, bddAbove_range_partialSups
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : CompleteLattice α
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), f i)

Tactic:
ciSup_partialSups_eq <| OrderTop.bddAbove _

Premises used: OrderTop.bddAbove, ciSup_partialSups_eq
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : CompleteLattice α
f : ι → α
i : ι
⊢ Eq.{u_1 + 1} (α := α) ((partialSups f : (a : ι) → α) i : α) (⨆ (j : ι), ⨆ (_ : j ≤ i), f j : α)

Tactic:
simpa only [iSup_subtype] using partialSups_eq_ciSup_Iic f i

Premises used: iSup_subtype, partialSups_eq_ciSup_Iic
-- Module: Mathlib.Order.PartialSups
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)
rw : LE.le.{u_1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), (partialSups g : (a : ι) → α) i)
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), g i)

Tactic:
rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g]

Premises used: iSup_partialSups_eq
-- Module: Mathlib.Order.PartialSups
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 : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), (partialSups g : (a : ι) → α) i)

Tactic:
iSup_mono h

Premises used: iSup_mono
-- Module: Mathlib.Order.PartialSups
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 : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), (partialSups g : (a : ι) → α) i)

Tactic:
exact iSup_mono h

Premises used: iSup_mono
-- Module: Mathlib.Order.PartialSups
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)
simp_rw₁ :
  Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (partialSups f : (a : ι) → α) i) (⨆ (i : ι), (partialSups g : (a : ι) → α) i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), g i)

Tactic:
simp_rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g, h]

Premises used: iSup_partialSups_eq
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
s : ℕ → Set α
n : ℕ
⊢ (partialSups s : (a : ℕ) → Set α) n = ⋃₀ (↑(image s (range (n + 1))) : Set (Set α))

Tactic:
simp [partialSups_eq_biSup, Nat.lt_succ_iff]

Premises used: partialSups_eq_biSup, Nat.lt_succ_iff
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
s : ℕ → Set α
n : ℕ
⊢ Eq (α := Set α) ((partialSups s : (a : ℕ) → Set α) n : Set α) (⋃ i ∈ range (n + 1), s i : Set α)

Tactic:
simp [partialSups_eq_biSup, Nat.lt_succ_iff]

Premises used: partialSups_eq_biSup, Nat.lt_succ_iff
-- Module: Mathlib.Order.PartialSups
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : LinearOrder α
f : ι → α
i : ι
⊢ ∃ j ∈ Iic i, ∀ k ∈ Iic i, f k ≤ f j

Tactic:
Finset.exists_max_image _ _ ⟨i, Finset.mem_Iic.mpr le_rfl⟩

Premises used: Iff.mpr, le_rfl, Finset.mem_Iic, Finset.exists_max_image, Exists.intro