mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ BddAbove (range fun i ↦ ⨆ (_ : i ∈ s), f i)

pp: case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨆ (_ : i ∈ s), f i

Tactic:
·

Goal state after:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ BddAbove (range fun i ↦ ⨆ (_ : i ∈ s), f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨆ (_ : i ∈ s), f i

Tactic:
·

Goal state after:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨆ (_ : i ∈ s), f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a

Tactic:
·

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
a : α
h : a ∈ lowerBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨅ j, f i j
i : ι
hx : (fun i ↦ ⨅ j, f i j) i = x
h✝ : IsEmpty (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun i ↦ ⨅ j, f i j) i

pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
a : α
h : a ∈ lowerBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨅ j, f i j
i : ι
hx : (fun i ↦ ⨅ j, f i j) i = x
h✝ : Nonempty (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun i ↦ ⨅ j, f i j) i

Tactic:
·

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow (⋃ i, range (f i))
a : α
h : a ∈ lowerBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨅ j, f i j
i : ι
hx : (fun i ↦ ⨅ j, f i j) i = x
h✝ : IsEmpty (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun i ↦ ⨅ j, f i j) i
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp
ι : 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

pp: case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ (∀ x ∈ s, a < f x) → a < ⨅ i ∈ s, f i

Tactic:
·

Goal state after:
case mp
ι : 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
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝ : Nonempty β
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝ : IsEmpty β
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ BddBelow (range fun i ↦ ⨅ (_ : i ∈ s), f i)

pp: case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨅ (_ : i ∈ s), f i

Tactic:
·

Goal state after:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ BddBelow (range fun i ↦ ⨅ (_ : i ∈ s), f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : IsEmpty γ
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : IsEmpty γ
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨅ (_ : i ∈ s), f i

Tactic:
·

Goal state after:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨅ (_ : i ∈ s), f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

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

Tactic:
·

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ (∀ x ∈ s, a < f x) → a < ⨅ i ∈ s, f i
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:
dsimp only; split_ifs <;> simp [*]

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

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

pp: case inr
α : 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)
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
·

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : IsEmpty (Subtype p)
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩
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 ι
⊢ ∀ (x : Subtype p), f x ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

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:
·

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 ι
⊢ ∀ (x : Subtype p), f x ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩
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:
·

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, ⨆ (h : p i), f ⟨i, h⟩ ≤ iSup f
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : 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

pp: case neg
α : 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
⊢ sSup ∅ ≤ iSup f

Tactic:
·

Goal state after:
case pos
α : 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
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : 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
⊢ sSup ∅ ≤ iSup f

Tactic:
·

Goal state after:
case neg
α : 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
⊢ sSup ∅ ≤ iSup f
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

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

pp: case inr
α : Type u_5
inst✝ : CompleteLinearOrder α
s : Set α
hfin : s.Finite
a : α
hne : a ≠ ⊥
hmem : a ∉ s
hnonempty : s.Nonempty
⊢ sSup s ≠ a

Tactic:
·

Goal state after:
case inl
α : Type u_5
inst✝ : CompleteLinearOrder α
a : α
hne : a ≠ ⊥
hfin : ∅.Finite
hmem : a ∉ ∅
⊢ sSup ∅ ≠ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ sSup ∅ ≤ ⨆ i, ↑i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ i, ↑i ≤ sInf ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

pp: case inr
α : 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
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ ⨆ i ∈ f '' ∅, g i = ⨆ x ∈ ∅, g (f x)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
·

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

Tactic:
·

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
·

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : ¬BddAbove (range f)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)

Tactic:
·

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
·

Goal state after:
case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : ¬BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f

Tactic:
·

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : ¬BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f

Tactic:
·

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : ¬BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f
Module: Mathlib.Order.CompleteLattice.Finset

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

pp: case refine_2
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ t, ⨆ i ∈ t, s i ≤ ⨆ i, s i

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ i, s i ≤ ⨆ t, ⨆ i ∈ t, s i
Module: Mathlib.Order.CompleteLattice.Finset

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

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ t, ⨆ i ∈ t, s i ≤ ⨆ i, s i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

pp: case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ∀ w < sSup ∅, ∃ i, w < ⨆ (h : p i), f ⟨i, h⟩

Tactic:
·

Goal state after:
case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
hj : p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
hj : ¬p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

Tactic:
·

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
hj : p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
hj : ¬p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

Tactic:
·

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
hj : ¬p j
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅
Module: Mathlib.Order.Cover

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

pp: case inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ∀ w < sSup ∅, ∃ i, w < ⨆ (h : p i), f ⟨i, h⟩

Tactic:
·

Goal state after:
case inr.refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ∀ w < sSup ∅, ∃ i, w < ⨆ (h : p i), f ⟨i, h⟩
Module: Mathlib.Order.Cover

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b

pp: case inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case mp
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ⨅ i, f i = n → (∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i

pp: case mpr
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ((∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i) → ⨅ i, f i = n

Tactic:
·

Goal state after:
case mp
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ⨅ i, f i = n → (∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ {a, b} ⊆ {b, a}

Tactic:
pair_comm

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ {b, a} ⊆ {b, a}
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case mpr
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ((∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i) → ⨅ i, f i = n

Tactic:
·

Goal state after:
case mpr
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ((∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i) → ⨅ i, f i = n
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Iic a ∪ ∅ = Iic a

Tactic:
union_empty

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Iic a = Iic a
Module: Mathlib.Order.Cover

Goal state before:
pp: case pos
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s

pp: case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s

Tactic:
·

Goal state after:
case pos
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s
Module: Mathlib.Order.Cover

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s

Tactic:
·

Goal state after:
case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s