awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
⊢ sSup (s \ {⊥}) = sSup s

Tactic:
(sSup_le_sSup diff_subset).antisymm <|
    sSup_le_sSup_of_subset_insert_bot <| subset_insert_diff_singleton _ _

Premises used: Set.diff_subset, LE.le.antisymm, sSup_le_sSup_of_subset_insert_bot, Set.subset_insert_diff_singleton, sSup_le_sSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
a b : α
⊢ sSup {a, b} = a ⊔ b

Tactic:
(@isLUB_pair α _ a b).sSup_eq

Premises used: isLUB_pair, IsLUB.sSup_eq
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
⊢ sSup s = ⊥ ↔ ∀ a ∈ s, a = ⊥

Tactic:
⟨fun h _ ha => bot_unique <| h ▸ le_sSup ha, fun h =>
    bot_unique <| sSup_le fun a ha => le_bot_iff.2 <| h a ha⟩

Premises used: le_bot_iff, Iff.mpr, Eq.rec, Iff.intro, bot_unique, le_sSup, sSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
rw : (∀ a ∈ s, a = ⊥) ↔ s = ∅ ∨ s = {⊥}
rw₁ : (∀ a ∈ s, a = ⊥) ↔ s ⊆ {⊥}
rw₂ rw₃ : (∀ a ∈ s, a = ⊥) ↔ ∀ y ∈ s, y = ⊥
⊢ sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}

Tactic:
rw [sSup_eq_bot, ← subset_singleton_iff_eq, subset_singleton_iff]

Premises used: sSup_eq_bot, Set.subset_singleton_iff, Set.subset_singleton_iff_eq
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
rw : s.Nonempty ∧ ∀ x ∈ s, x = ⊥
⊢ s = {⊥}

Tactic:
rw [Set.eq_singleton_iff_nonempty_unique_mem]

Premises used: Set.eq_singleton_iff_nonempty_unique_mem
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ ∀ a ∈ s, a = ⊥

Tactic:
rw [sSup_eq_bot] at h_sup

Premises used: sSup_eq_bot
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
h_sup₁ : ∀ a ∈ s, a = ⊥
⊢ s.Nonempty

Tactic:
rw [sSup_eq_bot] at h_sup

Premises used: sSup_eq_bot
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
h_sup : ∀ a ∈ s, a = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥

Tactic:
⟨hne, h_sup⟩

Premises used: And.intro
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
h_sup : ∀ a ∈ s, a = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥

Tactic:
exact ⟨hne, h_sup⟩
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
b : α
h₁ : ∀ a ∈ s, a ≤ b
h₂ : ∀ w < b, ∃ a ∈ s, w < a
⊢ sSup s = b

Tactic:
(sSup_le h₁).eq_of_not_lt fun h =>
    let ⟨_, ha, ha'⟩ := h₂ _ h
    ((le_sSup ha).trans_lt ha').false

Premises used: False, _private.0.sSup_eq_of_forall_le_of_forall_lt_exists_gt.match_1, LE.le.eq_of_not_lt, LT.lt.false, le_sSup, sSup_le, LE.le.trans_lt, SupSet.sSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : SupSet α
f : ι → α
⊢ sSup (range f) = iSup f

Tactic:
rfl

Premises used: iSup, rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : SupSet α
s : Set α
rw : sSup s = sSup (range fun (a : (↑s : Type u_1)) ↦ (↑a : α))
rw₁ rw₂ : sSup s = sSup s
⊢ sSup s = ⨆ (a : (↑s : Type u_1)), (↑a : α)

Tactic:
rw [iSup, Subtype.range_coe]

Premises used: iSup, Subtype.range_coe
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : SupSet α
f g : ι → α
h : ∀ (i : ι), f i = g i
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), g i)

Tactic:
congr_arg _ <| funext h

Premises used: congr_arg, funext
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : SupSet α
f g : ι → α
p : ι → Prop
h : ∀ (i : ι), p i → f i = g i
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (_ : p i), f i) (⨆ (i : ι), ⨆ (_ : p i), g i)

Tactic:
iSup_congr fun i ↦ iSup_congr (h i)

Premises used: iSup_congr
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (hi : p i), f i hi) (⨆ (i : ι), ⨆ (hi : p i), g i hi)

Tactic:
simp_all
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
simp : Eq.{u_1 + 1} (α := α) (sSup (range fun (x : ι) ↦ g (f x))) (sSup (range fun (y : ι') ↦ g y))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), g (f x)) (⨆ (y : ι'), g y)

Tactic:
simp only [iSup.eq_1]

Premises used: iSup.eq_1
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
e_a : Eq.{u_1 + 1} (α := Set α) (range fun (x : ι) ↦ g (f x)) (range fun (y : ι') ↦ g y)
⊢ Eq.{u_1 + 1} (α := α) (sSup (range fun (x : ι) ↦ g (f x))) (sSup (range fun (y : ι') ↦ g y))

Tactic:
congr
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ Eq.{u_1 + 1} (α := Set α) (range fun (x : ι) ↦ g (f x)) (range fun (y : ι') ↦ g y)

Tactic:
hf.range_comp g

Premises used: Function.Surjective.range_comp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ Eq.{u_1 + 1} (α := Set α) (range fun (x : ι) ↦ g (f x)) (range fun (y : ι') ↦ g y)

Tactic:
exact hf.range_comp g

Premises used: Function.Surjective.range_comp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
g : ι' → α
e : ι ≃ ι'
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), g ((e : (a : ι) → ι') x)) (⨆ (y : ι'), g y)

Tactic:
e.surjective.iSup_comp _

Premises used: Function.Surjective.iSup_comp, Equiv.surjective
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), g (h x)) (⨆ (y : ι'), g y)

Tactic:
h1.iSup_comp g

Premises used: Function.Surjective.iSup_comp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
h₁ : ∀ (x : ι), f x = g (h x)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x) (⨆ (y : ι'), g y)

Tactic:
convert! h1.iSup_comp g

Premises used: Function.Surjective.iSup_comp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
x : ι
⊢ f x = g (h x)

Tactic:
(h2 _).symm

Premises used: Eq.symm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
x : ι
⊢ f x = g (h x)

Tactic:
exact (h2 _).symm

Premises used: Eq.symm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → α
g : ι' → α
e : ι ≃ ι'
h : ∀ (x : ι), g ((e : (a : ι) → ι') x) = f x
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x) (⨆ (y : ι'), g y)

Tactic:
e.surjective.iSup_congr _ h

Premises used: Function.Surjective.iSup_congr, Equiv.surjective
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : SupSet α
p q : Prop
f₁ : p → α
f₂ : q → α
pq : p ↔ q
f : ∀ (x : q), f₁ ⋯ = f₂ x
obtain : ∀ {f₂ : p → α} (pq : p ↔ p) (f : ∀ (x : p), f₁ ⋯ = f₂ x), iSup f₁ = iSup f₂
⊢ iSup f₁ = iSup f₂

Tactic:
obtain rfl := propext pq

Premises used: propext, rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : SupSet α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ ⋯ = f₂ x
e_s : ∀ (x : p), f₁ x = f₂ x
⊢ iSup f₁ = iSup f₂

Tactic:
congr with x
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : SupSet α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ ⋯ = f₂ x
x : p
⊢ f₁ x = f₂ x

Tactic:
apply f
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : SupSet α
f : PLift ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f { down := i }) (⨆ (i : PLift ι), f i)

Tactic:
(PLift.up_surjective.iSup_congr _) fun _ => rfl

Premises used: PLift.up_surjective, Function.Surjective.iSup_congr, rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : SupSet α
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : PLift ι), f i.down) (⨆ (i : ι), f i)

Tactic:
(PLift.down_surjective.iSup_congr _) fun _ => rfl

Premises used: Function.Surjective.iSup_congr, PLift.down_surjective, rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : SupSet α
g : β → α
f : ι → β
rw : Eq.{u_1 + 1} (α := α) (sSup (range fun (b : (↑(range f) : Type u_2)) ↦ g (↑b : β))) (⨆ (i : ι), g (f i))
rw₁ :
  Eq.{u_1 + 1} (α := α) (sSup (range fun (b : (↑(range f) : Type u_2)) ↦ g (↑b : β)))
    (sSup (range fun (i : ι) ↦ g (f i)))
rw₂ : sSup (g '' range f) = sSup (range fun (i : ι) ↦ g (f i))
rw₃ rw₄ : Eq.{u_1 + 1} (α := α) (sSup (range fun (x : ι) ↦ g (f x))) (sSup (range fun (i : ι) ↦ g (f i)))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (b : (↑(range f) : Type u_2)), g (↑b : β)) (⨆ (i : ι), g (f i))

Tactic:
rw [iSup, iSup, ← image_eq_range, ← range_comp']

Premises used: iSup, Set.image_eq_range, Set.range_comp'
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : SupSet α
s : Set β
f : β → α
rw : sSup (f '' s) = sSup (range fun (a : (↑s : Type u_2)) ↦ f (↑a : β))
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := α) (sSup (range fun (x : (↑s : Type u_2)) ↦ f (↑x : β)))
    (sSup (range fun (a : (↑s : Type u_2)) ↦ f (↑a : β)))
⊢ sSup (f '' s) = ⨆ (a : (↑s : Type u_2)), f (↑a : β)

Tactic:
rw [iSup, image_eq_range]

Premises used: iSup, Set.image_eq_range
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
i : ι
⊢ f i ≤ iSup f

Tactic:
le_sSup ⟨i, rfl⟩

Premises used: iSup, Exists.intro, le_sSup, rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
inst_1 : Nonempty ι
⊢ LE.le.{u_1} (α := α) (⨅ (i : ι), f i) (⨆ (i : ι), f i)

Tactic:
(iInf_le _ (Classical.arbitrary _)).trans <| le_iSup _ (Classical.arbitrary _)

Premises used: le_iSup, Classical.arbitrary, LE.le.trans, iInf_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
⊢ IsLUB (range f) (⨆ (j : ι), f j)

Tactic:
isLUB_sSup _

Premises used: iSup, isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
a : α
h : IsLUB (range f) a
⊢ ⨆ (j : ι), f j = a

Tactic:
h.sSup_eq

Premises used: iSup, IsLUB.sSup_eq
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
a : α
i : ι
h : a ≤ f i
⊢ a ≤ iSup f

Tactic:
h.trans <| le_iSup _ i

Premises used: le_iSup, LE.le.trans
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLattice α
f : (i : ι) → κ i → α
i : ι
j : κ i
⊢ f i j ≤ ⨆ (i : ι), ⨆ (j : κ i), f i j

Tactic:
le_iSup_of_le i <| le_iSup (f i) j

Premises used: le_iSup, le_iSup_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLattice α
a : α
f : (i : ι) → κ i → α
i : ι
j : κ i
h : a ≤ f i j
⊢ a ≤ ⨆ (i : ι), ⨆ (j : κ i), f i j

Tactic:
h.trans <| le_iSup₂ i j

Premises used: le_iSup₂, LE.le.trans
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
a : α
h : ∀ (i : ι), f i ≤ a
⊢ iSup f ≤ a

Tactic:
sSup_le fun _ ⟨i, Eq⟩ => Eq ▸ h i

Premises used: iSup, Eq.rec, LE.le, sSup_le, _private.0.iSup_le.match_1
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLattice α
a : α
f : (i : ι) → κ i → α
h : ∀ (i : ι) (j : κ i), f i j ≤ a
⊢ ⨆ (i : ι), ⨆ (j : κ i), f i j ≤ a

Tactic:
iSup_le fun i => iSup_le <| h i

Premises used: iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
κ : ι → Sort u_8
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (x : κ i), f i) (⨆ (i : ι), f i)

Tactic:
iSup₂_le fun i _ => le_iSup f i

Premises used: iSup₂_le, le_iSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f g : ι → α
h : ∀ (i : ι), f i ≤ g i
⊢ iSup f ≤ iSup g

Tactic:
iSup_le fun i => le_iSup_of_le i <| h i

Premises used: le_iSup_of_le, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLattice α
f g : (i : ι) → κ i → α
h : ∀ (i : ι) (j : κ i), f i j ≤ g i j
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), f i j) (⨆ (i : ι), ⨆ (j : κ i), g i j)

Tactic:
iSup_mono fun i => iSup_mono <| h i

Premises used: iSup_mono
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : CompleteLattice α
f : ι → α
g : ι' → α
h : ∀ (i : ι), ∃ (i' : ι'), f i ≤ g i'
⊢ iSup f ≤ iSup g

Tactic:
iSup_le fun i => Exists.elim (h i) le_iSup_of_le

Premises used: le_iSup_of_le, iSup_le, Exists.elim
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : CompleteLattice α
f : (i : ι) → κ i → α
g : (i' : ι') → κ' i' → α
h : ∀ (i : ι) (j : κ i), ∃ (i' : ι') (j' : κ' i'), f i j ≤ g i' j'
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), f i j) (⨆ (i : ι'), ⨆ (j : κ' i), g i j)

Tactic:
iSup₂_le fun i j =>
    let ⟨i', j', h⟩ := h i j
    le_iSup₂_of_le i' j' h

Premises used: iSup₂_le, iSup, LE.le, _private.0.iSup₂_mono'.match_1, le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : CompleteLattice α
a : α
h : ι → ι'
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), a) (⨆ (x : ι'), a)

Tactic:
iSup_le <| le_iSup _ ∘ h

Premises used: Function.comp, le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : CompleteLattice α
f : ι → ι' → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨅ (j : ι'), f i j) (⨅ (j : ι'), ⨆ (i : ι), f i j)

Tactic:
iSup_le fun i => iInf_mono fun j => le_iSup (fun i => f i j) i

Premises used: le_iSup, iInf_mono, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
p q : ι → Prop
hpq : ∀ (i : ι), p i → q i
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (_ : p i), f i) (⨆ (i : ι), ⨆ (_ : q i), f i)

Tactic:
iSup_mono fun i => iSup_const_mono (hpq i)

Premises used: iSup_const_mono, iSup_mono
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
a : α
⊢ iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a

Tactic:
(isLUB_le_iff isLUB_iSup).trans forall_mem_range

Premises used: Set.forall_mem_range, isLUB_iSup, isLUB_le_iff, Iff.trans
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLattice α
a : α
f : (i : ι) → κ i → α
⊢ ⨆ (i : ι), ⨆ (j : κ i), f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a

Tactic:
simp_rw [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
⊢ sSup s = ⨆ a ∈ s, a

Tactic:
le_antisymm (sSup_le le_iSup₂) (iSup₂_le fun _ => le_sSup)

Premises used: iSup₂_le, le_iSup₂, le_antisymm, le_sSup, sSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
⊢ sSup (lowerBounds s) = sInf s

Tactic:
(isLUB_sSup _).unique (isGLB_sInf _).isLUB

Premises used: isGLB_sInf, IsGreatest.isLUB, IsLUB.unique, isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : CompleteLattice α
s : ι → α
inst_1 : CompleteLattice β
f : α → β
hf : Monotone f
⊢ ⨆ (i : ι), f (s i) ≤ f (iSup s)

Tactic:
iSup_le fun _ => hf <| le_iSup _ _

Premises used: le_iSup, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : CompleteLattice α
s : ι → α
inst_1 : CompleteLattice β
f : α → β
hf : Antitone f
⊢ ⨆ (i : ι), f (s i) ≤ f (iInf s)

Tactic:
hf.dual_left.le_map_iSup

Premises used: iInf, iSup, Monotone.le_map_iSup, Antitone.dual_left, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
hf : Monotone f
s : (i : ι) → κ i → α
⊢ ⨆ (i : ι), ⨆ (j : κ i), f (s i j) ≤ f (⨆ (i : ι), ⨆ (j : κ i), s i j)

Tactic:
iSup₂_le fun _ _ => hf <| le_iSup₂ _ _

Premises used: iSup₂_le, le_iSup₂
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
hf : Antitone f
s : (i : ι) → κ i → α
⊢ ⨆ (i : ι), ⨆ (j : κ i), f (s i j) ≤ f (⨅ (i : ι), ⨅ (j : κ i), s i j)

Tactic:
hf.dual_left.le_map_iSup₂ _

Premises used: iInf, iSup, Monotone.le_map_iSup₂, Antitone.dual_left, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
rw : ⨆ a ∈ s, f a ≤ f (⨆ a ∈ s, a)
⊢ ⨆ a ∈ s, f a ≤ f (sSup s)

Tactic:
rw [sSup_eq_iSup]

Premises used: sSup_eq_iSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (⨆ a ∈ s, a)

Tactic:
hf.le_map_iSup₂ _

Premises used: Monotone.le_map_iSup₂
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (⨆ a ∈ s, a)

Tactic:
exact hf.le_map_iSup₂ _

Premises used: Monotone.le_map_iSup₂
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
s : Set α
f : α → β
hf : Antitone f
⊢ ⨆ a ∈ s, f a ≤ f (sInf s)

Tactic:
hf.dual_left.le_map_sSup

Premises used: Set.Mem, Antitone.dual_left, Monotone.le_map_sSup, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α ≃o β
x_1 : ι → α
x : α
⊢ LE.le.{u_2} (α := β) ((f : (a : α) → β) (⨆ (i : ι), x_1 i) : β) ((f : (a : α) → β) x : β) ↔
    LE.le.{u_2} (α := β) (⨆ (i : ι), (f : (a : α) → β) (x_1 i) : β) ((f : (a : α) → β) x : β)

Tactic:
simp only [f.le_iff_le, iSup_le_iff]

Premises used: OrderIso.le_iff_le, iSup_le_iff
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α ≃o β
x_1 : (i : ι) → κ i → α
x : α
⊢ LE.le.{u_2} (α := β) ((f : (a : α) → β) (⨆ (i : ι), ⨆ (j : κ i), x_1 i j) : β) ((f : (a : α) → β) x : β) ↔
    LE.le.{u_2} (α := β) (⨆ (i : ι), ⨆ (j : κ i), (f : (a : α) → β) (x_1 i j) : β) ((f : (a : α) → β) x : β)

Tactic:
simp only [f.le_iff_le, iSup_le_iff]

Premises used: OrderIso.le_iff_le, iSup_le_iff
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α ≃o β
s : Set α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (f : (a : α) → β) a : β)

Tactic:
simp only [sSup_eq_iSup, OrderIso.map_iSup]

Premises used: OrderIso.map_iSup, sSup_eq_iSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
ι' : Sort u_8
f : ι' → α
g : ι → ι'
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), f (g x)) (⨆ (y : ι'), f y)

Tactic:
iSup_mono' fun _ => ⟨_, le_rfl⟩

Premises used: le_rfl, iSup_mono', Exists.intro
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : CompleteLattice α
inst_1 : Preorder β
f : β → α
hf : Monotone f
s : ι → β
hs : ∀ (x : β), ∃ (i : ι), x ≤ s i
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f (s x)) (⨆ (y : β), f y)

Tactic:
le_antisymm (iSup_comp_le _ _) (iSup_mono' fun x => (hs x).imp fun _ hi => hf hi)

Premises used: iSup_mono', Exists.imp, le_antisymm, iSup_comp_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
a : α
⊢ ⨆ (x : ι), a ≤ a

Tactic:
iSup_le fun _ => le_rfl

Premises used: le_rfl, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
a : α
inst_1 : Nonempty ι
rw : sSup (range fun (x : ι) ↦ a) = a
rw₁ : sSup {a} = a
rw₂ rw₃ : a = a
⊢ ⨆ (x : ι), a = a

Tactic:
rw [iSup, range_const, sSup_singleton]

Premises used: iSup, sSup_singleton, Set.range_const
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
inst_1 : Unique ι
f : ι → α
⊢ ⨆ (i : ι), f i = f default

Tactic:
simp only [congr_arg f (Unique.eq_default _), iSup_const]

Premises used: Unique.eq_default, congr_arg, iSup_const
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), ⊥) ⊥

Tactic:
bot_unique iSup_const_le

Premises used: bot_unique, iSup_const_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
s : ι → α
⊢ iSup s = ⊥ ↔ ∀ (i : ι), s i = ⊥

Tactic:
sSup_eq_bot.trans forall_mem_range

Premises used: sSup_eq_bot, Set.forall_mem_range, iSup, Iff.trans
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
s : ι → α
⊢ LT.lt.{u_1} (α := α) ⊥ (⨆ (i : ι), s i) ↔ ∃ (i : ι), ⊥ < s i

Tactic:
simp [bot_lt_iff_ne_bot]

Premises used: bot_lt_iff_ne_bot
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), f i j) ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
p : Prop
f : p → α
hp : p
⊢ ⨆ (h : p), f h = f hp

Tactic:
le_antisymm (iSup_le fun _ => le_rfl) (le_iSup _ _)

Premises used: le_rfl, le_iSup, le_antisymm, iSup_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
p : Prop
f : p → α
hp : ¬p
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) ⊥

Tactic:
le_antisymm (iSup_le fun h => (hp h).elim) bot_le

Premises used: False.elim, le_antisymm, iSup_le, bot_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
b : α
f : ι → α
h₁ : ∀ (i : ι), f i ≤ b
h₂ : ∀ w < b, ∃ (i : ι), w < f i
⊢ ⨆ (i : ι), f i = b

Tactic:
sSup_eq_of_forall_le_of_forall_lt_exists_gt (forall_mem_range.mpr h₁) fun w hw =>
    exists_range_iff.mpr <| h₂ w hw

Premises used: Iff.mpr, Set.forall_mem_range, iSup, Set.exists_range_iff, sSup_eq_of_forall_le_of_forall_lt_exists_gt
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
p : Prop
inst_1 : Decidable p
a : p → α
pos : ∀ (h : p), Eq.{u_1 + 1} (α := α) (⨆ (h : p), a h) (if h : p then a h else ⊥)
neg : ∀ (h : ¬p), Eq.{u_1 + 1} (α := α) (⨆ (h : p), a h) (if h : p then a h else ⊥)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), a h) (if h : p then a h else ⊥)

Tactic:
by_cases h : p
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
p : Prop
inst_1 : Decidable p
a : p → α
h : p
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), a h) (if h : p then a h else ⊥)

Tactic:
simp [h]
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
p : Prop
inst_1 : Decidable p
a : p → α
h : ¬p
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), a h) (if h : p then a h else ⊥)

Tactic:
simp [h]
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
p : Prop
inst_1 : Decidable p
a : α
⊢ ⨆ (_ : p), a = if p then a else ⊥

Tactic:
iSup_eq_dif fun _ => a

Premises used: iSup_eq_dif, ite