mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
⊢ (⋃ j, I.pi fun i ↦ s i j) = I.pi fun i ↦ ⋃ j, s i j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Sort v
κ : ι → Sort w
inst✝¹ : Order.Frame α
inst✝ : Finite ι
f : (a : ι) → κ a → α
this : ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
B : α
hB : ∀ y ∈ range f, y ≤ B
z : β
hy : ⨆ c, f (z, c) ∈ range fun b ↦ ⨆ c, f (b, c)
c : γ
⊢ f (z, c) ≤ B

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
⊢ BddAbove (range fun b ↦ ⨆ c, f (b, c))

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
b : β
B : α
hB : ∀ y ∈ range f, y ≤ B
⊢ ∀ y ∈ range fun c ↦ f (b, c), y ≤ B

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
b : β
⊢ BddAbove (range fun c ↦ f (b, c))

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ (fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩) ((fun a ↦ untopD ⊤ (map Subtype.val a)) ↑⟨a, h⟩) = ↑⟨a, h⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
⊢ (fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩) ((fun a ↦ untopD ⊤ (map Subtype.val a)) ⊤) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Sort v
κ : ι → Sort w
inst✝¹ : Order.Frame α
inst✝ : Finite ι
f : (a : ι) → κ a → α
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
⊢ (fun a ↦ untopD ⊤ (map Subtype.val a)) ((fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩) a) = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a✝ b✝ : WithTop { a // a ≠ ⊤ }
a b : { a // a ≠ ⊤ }
⊢ { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩, left_inv := ⋯,
          right_inv := ⋯ }
        ↑a ≤
      { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ↑b ↔
    ↑a ≤ ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a b✝ : WithTop { a // a ≠ ⊤ }
b : α
h : b ≠ ⊤
⊢ { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩, left_inv := ⋯,
          right_inv := ⋯ }
        ⊤ ≤
      { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ↑⟨b, h⟩ ↔
    ⊤ ≤ ↑⟨b, h⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a✝ b a : WithTop { a // a ≠ ⊤ }
⊢ { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩, left_inv := ⋯,
          right_inv := ⋯ }
        a ≤
      { toFun := fun a ↦ untopD ⊤ (map Subtype.val a), invFun := fun a ↦ if h : a = ⊤ then ⊤ else ↑⟨a, h⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⊤ ↔
    a ≤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type v
κ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
h : ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α), ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ subtypeOrderIso.symm a = ↑⟨a, h⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
⊢ ⇑(LatticeHom.id α).withTopWithBot = ⇑(BoundedLatticeHom.id (WithTop (WithBot α)))

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
⊢ Iic (⨅ i, f i) = ⋂ i, Iic (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ range some = Iio ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Icc ↑a ↑b = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ico ↑a ↑b = Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ioc ↑a ↑b = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ioo ↑a ↑b = Ioo a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ some ⁻¹' Iio ⊤ = univ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some ⁻¹' Ico ↑a ⊤ = Ici a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some ⁻¹' Ioo ↑a ⊤ = Ioi a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Ioi a = Ioo ↑a ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Ici a = Ico ↑a ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Iio a = Iio ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Iic a = Iic ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
i : ι
h : p i
⊢ f ⟨i, h⟩ = (fun i ↦ ⨆ (h : p i), f ⟨i, h⟩) i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ∃ x ∈ l.toFinset, sSup ∅ ≤ f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ⨆ x ∈ l, f x ∈ map f l

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Icc a b = Icc ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ∃ x ∈ l.toFinset, f x ≤ sInf ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ⨅ x ∈ l, f x ∈ map f l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type v
κ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
⊢ ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this✝ : Nonempty ι
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i ↦ ⨆ (h : p i), f ⟨i, h⟩) i
⊢ BddAbove (range fun i ↦ ⨆ (h : p i), f ⟨i, h⟩)

Tactic:
simp_rw [ciSup_eq_ite]

Goal state after:
case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this✝ : Nonempty ι
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i ↦ ⨆ (h : p i), f ⟨i, h⟩) i
⊢ BddAbove (range fun i ↦ if h : p i then f ⟨i, h⟩ else sSup ∅)
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ico a b = Ico ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ∃ x ∈ s.toFinset, sSup ∅ ≤ f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ioc a b = Ioc ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
i : ι
⊢ ⨆ (h : p i), f ⟨i, h⟩ ≤ iSup f

Tactic:
simp_rw [ciSup_eq_ite]

Goal state after:
case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
i : ι
⊢ (if h : p i then f ⟨i, h⟩ else sSup ∅) ≤ iSup f
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ioo a b = Ioo ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ x ∈ s, f x ∈ map f s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ioi ↑a = some '' Ioi a ∪ {⊤}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ici ↑a = some '' Ici a ∪ {⊤}

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ∃ x ∈ s.toFinset, f x ≤ sInf ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Nonempty α
I : Set β
S : β → Set α
H : I.Finite
⊢ BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ x ∈ s, f x ∈ map f s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
s : Set α
⊢ (s \ ⋃ x, Ioo ↑x.1 ↑x.2).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLinearOrder α
s : Set α
hfin : s.Finite
a : α
hne : a ≠ ⊥
hmem : a ∉ s
⊢ sSup s ≠ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Set β
f : β → α
hf : BddAbove (range fun i ↦ f ↑i)
hf' : sSup ∅ ≤ ⨆ i, f ↑i
⊢ sSup (f '' s) = ⨆ a ∈ s, f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: α : Type u_5
inst✝¹ : CompleteLinearOrder α
ι : Sort u_6
inst✝ : Finite ι
f : ι → α
a : α
hne : a ≠ ⊥
h : ∀ (x : ι), f x ≠ a
⊢ a ∉ range f

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup' H f ≤ a ↔ sSup (f '' ↑s) ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
⊢ s.sup' hs id = sSup ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
f : ι → α
⊢ univ.sup' ⋯ f = ⨆ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
f : ι → α
⊢ univ.inf' ⋯ f = ⨅ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t : Finset ι
this : ∀ (st : Finset ι), BddAbove (Set.range fun x ↦ ⨆ (_ : x ∈ st), f x)
⊢ ⨆ x ∈ s ∪ t, f x = max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ ⨆ i ∈ s, i = sSup s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
s : Finset α
hs : ↑s ⊆ ⋃ i, f i
⊢ ∃ i, ↑s ⊆ f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ i ∈ s, i = sInf s

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t : Finset ι
⊢ ⨆ x ∈ s ∪ t, f x = max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Finset ι
h : s.Nonempty
h' : (image f s).Nonempty
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Finset ι
h : s.Nonempty
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Set ι
h : s.Nonempty
hs : s.Finite
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set ι
a : α
f : ι → α
h : s.Nonempty
hs : s.Finite
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
l : List ι
f : ι → α
h : l ≠ []
⊢ ∃ x ∈ l, sSup ∅ ≤ f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j ↦ f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ i ∈ c, f i
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Multiset ι
f : ι → α
h : s ≠ 0
⊢ ∃ x ∈ s, sSup ∅ ≤ f x

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
⊢ BddAbove (range fun i ↦ g ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : s ⊆ ⋃₀ c
⊢ ∃ t ∈ c, s ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this✝ : Nonempty ↑s
i : ι
h : i ∈ s
this : f i ∈ f '' s
⊢ g ↑⟨f i, this⟩ = g (f ↑⟨i, h⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
⊢ ∃ t, g ↑t = g (f ↑⟨i, h⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
⊢ sSup ∅ ≤ ⨆ i, g ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → x = b → α
⊢ f b ⋯ ≤ ⨆ x, ⨆ (h : x = b), f x h

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → b = x → α
⊢ f b ⋯ ≤ ⨆ x, ⨆ (h : b = x), f x h

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
⊢ ⨆ (ih : p ∧ q), f ih = ⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrder α
a : α
inst✝ : Nonempty ι
f : ι → α
hb : BddAbove (range f)
⊢ a < iSup f ↔ ∃ i, a < f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrder α
a : α
inst✝ : Nonempty ι
f : ι → α
hb : BddBelow (range f)
⊢ iInf f < a ↔ ∃ i, f i < a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
b : ι
⊢ b ∈ {b}

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i.down

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: ι : Type u_5
s : Set ι
x : ι
hx : x ∈ s
⊢ ⟨x, ⋯⟩ ∈ {⟨x, hx⟩}

Tactic:
by

Goal state after: