awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : CompleteLattice α
f : ι → ι' → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι'), f i j) (⨆ (j : ι'), ⨆ (i : ι), f i j)

Tactic:
le_antisymm (iSup_le fun i => iSup_mono fun j => le_iSup (fun i => f i j) i)
    (iSup_le fun _ => iSup_mono fun _ => le_iSup _ _)

Premises used: le_iSup, le_antisymm, iSup_le, iSup_mono
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι₁ : Sort u_8
ι₂ : Sort u_9
κ₁ : ι₁ → Sort u_10
κ₂ : ι₂ → Sort u_11
f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i₁ : ι₁), ⨆ (j₁ : κ₁ i₁), ⨆ (i₂ : ι₂), ⨆ (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂)
    (⨆ (i₂ : ι₂), ⨆ (j₂ : κ₂ i₂), ⨆ (i₁ : ι₁), ⨆ (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂)

Tactic:
simp only [@iSup_comm _ (κ₁ _), @iSup_comm _ ι₁]

Premises used: iSup_comm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
c : β
f : (x : β) → x = c → α
⊢ f c ⋯ ≤ f c ⋯

Tactic:
rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
b : β
f : (x : β) → b = x → α
⊢ f b ⋯ ≤ f b ⋯

Tactic:
rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
f : Subtype p → α
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)

Tactic:
le_antisymm (iSup_le fun ⟨i, h⟩ => @le_iSup₂ _ _ p _ (fun i h => f ⟨i, h⟩) i h)
    (iSup₂_le fun _ _ => le_iSup _ _)

Premises used: iSup₂_le, iSup, _private.0.iSup_subtype.match_1, le_iSup₂, le_iSup, LE.le, Subtype.mk, le_antisymm, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (⨆ (x : Subtype p), f (↑x : ι) ⋯)

Tactic:
(@iSup_subtype _ _ _ p fun x => f x.val x.property).symm

Premises used: iSup_subtype, Eq.symm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
s : Set ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : (↑s : Type u_8)), f (↑i : ι)) (⨆ t ∈ s, f t)

Tactic:
iSup_subtype

Premises used: iSup_subtype
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
⊢ Nonempty.{u_2 + 1} (↑s : Type u_2)

Tactic:
haveI : Nonempty s := Set.nonempty_coe_sort.mpr hs
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
rw : ⨆ (i : (↑s : Type u_2)), a = a
rw₁ rw₂ : a = a
⊢ ⨆ i ∈ s, a = a

Tactic:
rw [← iSup_subtype'', iSup_const]

Premises used: iSup_subtype'', iSup_const
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f g : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x ⊔ g x) ((⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x)

Tactic:
le_antisymm (iSup_le fun _ => sup_le_sup (le_iSup _ _) <| le_iSup _ _)
    (sup_le (iSup_mono fun _ => le_sup_left) <| iSup_mono fun _ => le_sup_right)

Premises used: sup_le_sup, le_sup_left, le_iSup, le_sup_right, le_antisymm, iSup_le, sup_le, iSup_mono
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
ι' : Type u_9
g : ι' → α
e : ι ≃ ι'
s : Set ι'
⊢ Eq.{u_1 + 1} (α := α)
    (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ((⇑e.symm : (a : ι') → ι) '' s) i), g ((e : (a : ι) → ι') i))
    (⨆ i ∈ s, g i)

Tactic:
simpa only [iSup_subtype'] using (image e.symm s).symm.iSup_comp (g := g ∘ (↑))

Premises used: iSup_subtype', Equiv.iSup_comp, Equiv.image, Equiv.symm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
s : Set ι
f : ι → α
i : ι
hi : i ∈ s
⊢ f i ≤ ⨆ i ∈ s, f i

Tactic:
le_iSup₂_of_le i hi le_rfl

Premises used: le_rfl, le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
s : Set ι
hs : s.Nonempty
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨅ i ∈ s, f i) (⨆ i ∈ s, f i)

Tactic:
(biInf_le _ hs.choose_spec).trans <| le_biSup _ hs.choose_spec

Premises used: Exists.choose_spec, LE.le.trans, le_biSup, biInf_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
inst_1 : Nonempty ι
f : ι → α
a : α
rw : (⨆ (x : ι), f x) ⊔ a = (⨆ (x : ι), f x) ⊔ ⨆ (x : ι), a
rw₁ rw₂ : (⨆ (x : ι), f x) ⊔ a = (⨆ (x : ι), f x) ⊔ a
⊢ (⨆ (x : ι), f x) ⊔ a = ⨆ (x : ι), f x ⊔ a

Tactic:
rw [iSup_sup_eq, iSup_const]

Premises used: iSup_sup_eq, iSup_const
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
inst_1 : Nonempty ι
f : ι → α
a : α
rw : a ⊔ ⨆ (x : ι), f x = (⨆ (x : ι), a) ⊔ ⨆ (x : ι), f x
rw₁ rw₂ : a ⊔ ⨆ (x : ι), f x = a ⊔ ⨆ (x : ι), f x
⊢ a ⊔ ⨆ (x : ι), f x = ⨆ (x : ι), a ⊔ f x

Tactic:
rw [iSup_sup_eq, iSup_const]

Premises used: iSup_sup_eq, iSup_const
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ (i : ι), p i
⊢ Nonempty.{max 1 u_4} { i : ι // p i }

Tactic:
haveI : Nonempty { i // p i } :=
    let ⟨i, hi⟩ := h
    ⟨⟨i, hi⟩⟩
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ (i : ι), p i
this : Nonempty.{max 1 u_4} { i : ι // p i }
rw : (⨆ (x : Subtype p), f (↑x : ι) ⋯) ⊔ a = ⨆ (i : ι), ⨆ (h : p i), f i h ⊔ a
rw₁ : (⨆ (x : Subtype p), f (↑x : ι) ⋯) ⊔ a = ⨆ (x : Subtype p), f (↑x : ι) ⋯ ⊔ a
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨆ (x : Subtype p), f (↑x : ι) ⋯ ⊔ a) (⨆ (x : Subtype p), f (↑x : ι) ⋯ ⊔ a)
⊢ (⨆ (i : ι), ⨆ (h : p i), f i h) ⊔ a = ⨆ (i : ι), ⨆ (h : p i), f i h ⊔ a

Tactic:
rw [iSup_subtype', iSup_subtype', iSup_sup]

Premises used: iSup_subtype', iSup_sup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ (i : ι), p i
⊢ a ⊔ ⨆ (i : ι), ⨆ (h : p i), f i h = ⨆ (i : ι), ⨆ (h : p i), a ⊔ f i h

Tactic:
simpa only [sup_comm] using @biSup_sup α _ _ p _ _ h

Premises used: sup_comm, biSup_sup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j) (⨆ (i : ι), f i)
a₁ : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j) (⨆ (i : ι), f i)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j) (⨆ (i : ι), f i)

Tactic:
iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

Premises used: iSup₂_le, le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j) (⨆ (i : ι), f i)

Tactic:
exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

Premises used: iSup₂_le, le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j)

Tactic:
iSup_le fun j ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
a : ∀ (j : ι), f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j)

Tactic:
refine iSup_le fun j ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
j : ι
a : ∀ (i : ι) (jlt : j < i), f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j
⊢ f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j

Tactic:
obtain ⟨i, jlt⟩ := exists_gt j

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
j i : ι
jlt : j < i
⊢ f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j

Tactic:
le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

Premises used: le_rfl, le_iSup_of_le, le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
j i : ι
jlt : j < i
⊢ f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j

Tactic:
exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

Premises used: le_iSup_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j) (⨆ (i : ι), f i)
a₁ : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j) (⨆ (i : ι), f i)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j) (⨆ (i : ι), f i)

Tactic:
iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

Premises used: iSup₂_le, le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j) (⨆ (i : ι), f i)

Tactic:
exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

Premises used: iSup₂_le, le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j)

Tactic:
iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

Premises used: le_rfl, le_iSup_of_le, iSup_le, le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j)

Tactic:
exact iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

Premises used: le_rfl, le_iSup_of_le, iSup_le, le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j) (⨆ (i : ι), f i)
a₁ : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j) (⨆ (i : ι), f i)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j) (⨆ (i : ι), f i)

Tactic:
iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

Premises used: iSup₂_le, le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j) (⨆ (i : ι), f i)

Tactic:
exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

Premises used: iSup₂_le, le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j)

Tactic:
iSup_le fun j ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
a : ∀ (j : ι), f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j)

Tactic:
refine iSup_le fun j ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
j : ι
a : ∀ (i : ι) (jlt : i < j), f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j
⊢ f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j

Tactic:
obtain ⟨i, jlt⟩ := exists_lt j

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
j i : ι
jlt : i < j
⊢ f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j

Tactic:
le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

Premises used: le_rfl, le_iSup_of_le, le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
j i : ι
jlt : i < j
⊢ f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j

Tactic:
exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

Premises used: le_iSup_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j) (⨆ (i : ι), f i)
a₁ : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j) (⨆ (i : ι), f i)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j) (⨆ (i : ι), f i)

Tactic:
iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

Premises used: iSup₂_le, le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j) (⨆ (i : ι), f i)

Tactic:
exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

Premises used: iSup₂_le, le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j)

Tactic:
iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

Premises used: le_rfl, le_iSup_of_le, iSup_le, le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j)

Tactic:
exact iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

Premises used: le_rfl, le_iSup_of_le, iSup_le, le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : Preorder β
f : β → α
hf : Monotone f
b : β
⊢ ⨆ (b' : β), ⨆ (_ : b' ≤ b), f b' = f b

Tactic:
le_antisymm (iSup₂_le_iff.2 (fun _ hji ↦ hf hji))
    (le_iSup_of_le b (ge_of_eq (iSup_pos le_rfl)))

Premises used: Iff.mpr, le_rfl, ge_of_eq, iSup_pos, le_antisymm, le_iSup_of_le, iSup₂_le_iff
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : Preorder β
f : β → α
hf : Antitone f
b : β
⊢ ⨅ (b' : β), ⨅ (_ : b' ≤ b), f b' = f b

Tactic:
le_antisymm (iInf₂_le_of_le b le_rfl le_rfl)
    (le_iInf₂ fun _ hji ↦ hf hji)

Premises used: le_rfl, iInf₂_le_of_le, le_iInf₂, le_antisymm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : False → α
⊢ iSup s = ⊥

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : True → α
⊢ iSup s = s trivial

Tactic:
iSup_pos trivial

Premises used: trivial, iSup_pos
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
f : Exists p → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : Exists p), f x) (⨆ (i : ι), ⨆ (h : p i), f ⋯)

Tactic:
le_antisymm (iSup_le fun ⟨i, h⟩ => @le_iSup₂ _ _ _ _ (fun _ _ => _) i h)
    (iSup₂_le fun _ _ => le_iSup _ _)

Premises used: iSup₂_le, _private.0.iSup_exists.match_1, iSup, le_iSup₂, le_iSup, LE.le, le_antisymm, Exists.intro, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
p q : Prop
s : p ∧ q → α
⊢ iSup s = ⨆ (h₁ : p), ⨆ (h₂ : q), s ⋯

Tactic:
le_antisymm (iSup_le fun ⟨i, h⟩ => @le_iSup₂ _ _ _ _ (fun _ _ => _) i h)
    (iSup₂_le fun _ _ => le_iSup _ _)

Premises used: iSup₂_le, iSup, le_iSup₂, le_iSup, LE.le, le_antisymm, And.intro, iSup_le, _private.0.iSup_and.match_1
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
p q : Prop
s : p → q → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h₁ : p), ⨆ (h₂ : q), s h₁ h₂) (⨆ (h : p ∧ q), s ⋯ ⋯)

Tactic:
Eq.symm iSup_and

Premises used: Eq.symm, iSup_and
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
p q : Prop
s : p ∨ q → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : p ∨ q), s x) ((⨆ (i : p), s ⋯) ⊔ ⨆ (j : q), s ⋯)

Tactic:
le_antisymm
    (iSup_le fun i =>
      match i with
      | Or.inl _ => le_sup_of_le_left <| le_iSup (fun _ => s _) _
      | Or.inr _ => le_sup_of_le_right <| le_iSup (fun _ => s _) _)
    (sup_le (iSup_comp_le _ _) (iSup_comp_le _ _))

Premises used: iSup, le_sup_of_le_left, le_iSup, LE.le, le_antisymm, Max.max, le_sup_of_le_right, iSup_le, sup_le, Or.inl, _private.0.iSup_or.match_1, iSup_comp_le, Or.inr
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
inst_1 : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
rw :
  Eq.{u_1 + 1} (α := α) (⨆ (i : ι), if h : p i then f i h else g i h)
    (⨆ (x : ι), (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), if h : p i then f i h else g i h)
    ((⨆ (i : ι), ⨆ (h : p i), f i h) ⊔ ⨆ (i : ι), ⨆ (h : ¬p i), g i h)

Tactic:
rw [← iSup_sup_eq]

Premises used: iSup_sup_eq
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
inst_1 : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
e_s : ∀ (i : ι), Eq.{u_1 + 1} (α := α) (if h : p i then f i h else g i h) ((⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), if h : p i then f i h else g i h)
    (⨆ (x : ι), (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h)

Tactic:
congr 1 with i
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
inst_1 : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
pos : ∀ (h : p i), f i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
neg : ∀ (h : ¬p i), g i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
⊢ Eq.{u_1 + 1} (α := α) (if h : p i then f i h else g i h) ((⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h)

Tactic:
split_ifs with h
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
inst_1 : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
h : p i
⊢ f i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h

Tactic:
simp [h]
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
inst_1 : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
h : ¬p i
⊢ g i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h

Tactic:
simp [h]
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), if p i then f i else g i)
    ((⨆ (i : ι), ⨆ (_ : p i), f i) ⊔ ⨆ (i : ι), ⨆ (_ : ¬p i), g i)

Tactic:
iSup_dite _ _ _

Premises used: iSup_dite, ite
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : CompleteLattice α
g : β → α
f : ι → β
rw : Eq.{u_1 + 1} (α := α) (⨆ (i : (↑(range f) : Type u_2)), g (↑i : β)) (⨆ (i : ι), g (f i))
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), g (f i)) (⨆ (i : ι), g (f i))
⊢ Eq.{u_1 + 1} (α := α) (⨆ b ∈ range f, g b) (⨆ (i : ι), g (f i))

Tactic:
rw [← iSup_subtype'', iSup_range']

Premises used: iSup_subtype'', iSup_range'
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
s : Set β
f : β → α
rw : sSup (f '' s) = ⨆ (i : (↑s : Type u_2)), f (↑i : β)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (⨆ (a : (↑s : Type u_2)), f (↑a : β)) (⨆ (i : (↑s : Type u_2)), f (↑i : β))
⊢ sSup (f '' s) = ⨆ a ∈ s, f a

Tactic:
rw [← iSup_subtype'', sSup_image']

Premises used: iSup_subtype'', sSup_image'
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α ≃o β
s : Set α
rw : Eq.{u_2 + 1} (α := β) (⨆ a ∈ s, (f : (a : α) → β) a) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s))
rw₁ : Eq.{u_2 + 1} (α := β) (sSup ((⇑f : (a : α) → β) '' s)) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s))
rw₂ rw₃ : Eq.{u_2 + 1} (α := β) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s)) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s))
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (sSup s) : β) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s) : β)

Tactic:
rw [map_sSup, ← sSup_image, f.image_eq_preimage_symm]

Premises used: sSup_image, OrderIso.map_sSup, OrderIso.image_eq_preimage_symm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : β), ⨆ (_ : Membership.mem (γ := Set β) ∅ x), f x) ⊥

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : β), ⨆ (_ : Membership.mem (γ := Set β) univ x), f x) (⨆ (x : β), f x)

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
s t : Set β
simp_rw : Eq.{u_1 + 1} (α := α) (⨆ (x : β), ⨆ (_ : x ∈ s ∨ x ∈ t), f x) ((⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x)
simp_rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (x : β), (⨆ (_ : x ∈ s), f x) ⊔ ⨆ (_ : x ∈ t), f x) ((⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x)
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ s ∪ t, f x) ((⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x)

Tactic:
simp_rw [mem_union, iSup_or, iSup_sup_eq]

Premises used: Set.mem_union, iSup_sup_eq, iSup_or
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
p : β → Prop
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : β), f i) ((⨆ (i : β), ⨆ (_ : p i), f i) ⊔ ⨆ (i : β), ⨆ (_ : ¬p i), f i)

Tactic:
simpa [Classical.em] using @iSup_union _ _ _ f { i | p i } { i | ¬p i }

Premises used: Classical.em, iSup_union
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
i₀ : β
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : β), f i) ((⨆ (i : β), ⨆ (_ : i = i₀), f i) ⊔ ⨆ (i : β), ⨆ (_ : ¬i = i₀), f i)

Tactic:
iSup_split f (fun i => i = i₀)

Premises used: iSup_split, Eq
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
i₀ : β
h : f i₀ = ⨆ (i : β), ⨆ (_ : i = i₀), f i
⊢ ⨆ (i : β), f i = f i₀ ⊔ ⨆ (i : β), ⨆ (_ : i ≠ i₀), f i

Tactic:
convert! iSup_split f (fun i => i = i₀)

Premises used: iSup_split, Eq
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
i₀ : β
⊢ f i₀ = ⨆ (i : β), ⨆ (_ : i = i₀), f i

Tactic:
simp