awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : ¬BddAbove (range f)
pos : LE.le.{u_1} (α := α) (sSup ∅) (max (sSup ∅) (⨆ (x : ι), g x))
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))

Tactic:
rw [ciSup_of_not_bddAbove hf, ciSup_of_not_bddAbove <| mt bbdAbove_range_left_of_sup hf]

Premises used: mt, ciSup_of_not_bddAbove, bbdAbove_range_left_of_sup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : ¬BddAbove (range f)
⊢ LE.le.{u_1} (α := α) (sSup ∅) (max (sSup ∅) (⨆ (x : ι), g x))

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : ¬BddAbove (range f)
⊢ LE.le.{u_1} (α := α) (sSup ∅) (max (sSup ∅) (⨆ (x : ι), g x))

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
pos :
  ∀ (hg : ¬BddAbove (range g)),
    LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
neg :
  ∀ (hg : BddAbove (range g)), LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))

Tactic:
by_cases! hg : ¬BddAbove (range g)

Premises used: BddAbove, Set.range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
pos : LE.le.{u_1} (α := α) (sSup ∅) (max (⨆ (x : ι), f x) (sSup ∅))
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))

Tactic:
rw [ciSup_of_not_bddAbove hg, ciSup_of_not_bddAbove <| mt bbdAbove_range_right_of_sup hg]

Premises used: mt, ciSup_of_not_bddAbove, bbdAbove_range_right_of_sup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ LE.le.{u_1} (α := α) (sSup ∅) (max (⨆ (x : ι), f x) (sSup ∅))

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ LE.le.{u_1} (α := α) (sSup ∅) (max (⨆ (x : ι), f x) (sSup ∅))

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))

Tactic:
ciSup_sup_eq hf hg |>.le

Premises used: Eq.le, ciSup_sup_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))

Tactic:
exact ciSup_sup_eq hf hg |>.le

Premises used: Eq.le, ciSup_sup_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
⊢ LE.le.{u_1} (α := α) (min (⨅ (x : ι), f x) (⨅ (x : ι), g x)) (⨅ (x : ι), min (f x) (g x))

Tactic:
ciSup_sup_le (α := αᵒᵈ)

Premises used: iInf, ciSup_sup_le, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
b : α
inst_1 : Nonempty ι
f : ι → α
h : b < iSup f
⊢ ∃ (i : ι), b < f i

Tactic:
let ⟨_, ⟨i, rfl⟩, h⟩ := exists_lt_of_lt_csSup (range_nonempty f) h
  ⟨i, h⟩

Premises used: Exists, _private.0.exists_lt_of_lt_ciSup.match_1, exists_lt_of_lt_csSup, Set.range_nonempty, LT.lt, Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
a : α
inst_1 : Nonempty ι
f : ι → α
h : iInf f < a
⊢ ∃ (i : ι), f i < a

Tactic:
exists_lt_of_lt_ciSup (α := αᵒᵈ) h

Premises used: exists_lt_of_lt_ciSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
a : α
inst_1 : Nonempty ι
f : ι → α
hb : BddAbove (range f)
⊢ a < iSup f ↔ ∃ (i : ι), a < f i

Tactic:
simpa only [mem_range, exists_exists_eq_and] using lt_csSup_iff hb (range_nonempty _)

Premises used: Set.mem_range, lt_csSup_iff, Set.range_nonempty, exists_exists_eq_and
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
a : α
inst_1 : Nonempty ι
f : ι → α
hb : BddBelow (range f)
⊢ iInf f < a ↔ ∃ (i : ι), f i < a

Tactic:
simpa only [mem_range, exists_exists_eq_and] using csInf_lt_iff hb (range_nonempty _)

Premises used: Set.mem_range, csInf_lt_iff, Set.range_nonempty, exists_exists_eq_and
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : (i : ι) → p i → α
h : ¬BddAbove.{u_1} (α := α) (range.{u_1, max 1 u_4} fun (i : Subtype p) ↦ f (↑i : ι) ⋯)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)

Tactic:
ciSup_of_not_bddAbove fun ⟨u, hu⟩ ↦ h ⟨u, fun _ ⟨x, hx⟩ ↦ hx ▸ hu ⟨x, ciSup_pos x.prop⟩⟩

Premises used: False, Eq.rec, LE.le, ciSup_pos, _private.0.cbiSup_of_not_bddAbove.match_1, Subtype.prop, Exists.intro, ciSup_of_not_bddAbove, Subtype.val, _private.0.cbiSup_of_not_bddAbove.match_2
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : (i : ι) → p i → α
h : ¬BddBelow.{u_1} (α := α) (range.{u_1, max 1 u_4} fun (i : Subtype p) ↦ f (↑i : ι) ⋯)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ι), ⨅ (h : p i), f i h) (sInf ∅)

Tactic:
ciInf_of_not_bddBelow fun ⟨u, hu⟩ ↦ h ⟨u, fun _ ⟨x, hx⟩ ↦ hx ▸ hu ⟨x, ciInf_pos x.prop⟩⟩

Premises used: False, ciInf_of_not_bddBelow, Eq.rec, LE.le, _private.0.cbiInf_of_not_bddBelow.match_1, _private.0.cbiSup_of_not_bddAbove.match_1, Subtype.prop, Exists.intro, Subtype.val, ciInf_pos
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
inl :
  ∀ (le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f),
    ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
inr :
  ∀ (gt : iSup.{u_1, max 1 u_4} f < sSup ∅),
    ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)

Tactic:
rcases le_or_gt (sSup ∅) (iSup f) with le | gt

Premises used: iSup, le_or_gt, EmptyCollection.emptyCollection, SupSet.sSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
inl : ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)

Tactic:
rw [max_eq_left le]

Premises used: max_eq_left
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
pos :
  ∀ (bdd : BddAbove (range.{u_1, max 1 u_4} f)),
    ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
neg :
  ∀ (bdd : ¬BddAbove (range.{u_1, max 1 u_4} f)),
    ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f

Tactic:
by_cases bdd : BddAbove (range f)

Premises used: BddAbove, Set.range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
bdd : BddAbove (range.{u_1, max 1 u_4} f)
pos pos₁ : iSup.{u_1, max 1 u_4} f = iSup.{u_1, max 1 u_4} f
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f

Tactic:
rw [← ciSup_subtype bdd le]

Premises used: ciSup_subtype
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
bdd : ¬BddAbove (range.{u_1, max 1 u_4} f)
neg : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)) (sSup ∅)
neg₁ neg₂ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f

Tactic:
rw [ciSup_of_not_bddAbove bdd, cbiSup_of_not_bddAbove bdd]

Premises used: ciSup_of_not_bddAbove, cbiSup_of_not_bddAbove
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
inr :
  ∀ (i : ι) (hi : ¬p i), ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)

Tactic:
have ⟨i, hi⟩ := not_forall.mp hp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
⊢ Nonempty ι

Tactic:
have : Nonempty ι := ⟨i⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
⊢ BddAbove (range.{u_1, max 1 u_4} f)

Tactic:
have bdd : BddAbove (range f) := not_not.mp fun h ↦ gt.ne (ciSup_of_not_bddAbove h)
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
inr : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)) (sSup ∅)
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)

Tactic:
rw [max_eq_right gt.le]

Premises used: LT.lt.le, max_eq_right
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)) (sSup ∅)

Tactic:
ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j ↦ ?_) ?_

Premises used: ciSup_eq_of_forall_le_of_forall_lt_exists_gt
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
inr : ∀ (j : ι), LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)
inr₁ : ∀ w < sSup ∅, ∃ (i : ι), w < ⨆ (h : p i), f (Subtype.mk (p := p) i h)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)) (sSup ∅)

Tactic:
refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j ↦ ?_) ?_

Premises used: ciSup_eq_of_forall_le_of_forall_lt_exists_gt
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
j : ι
pos : ∀ (hj : p j), LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)
neg : ∀ (hj : ¬p j), LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)
⊢ LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)

Tactic:
by_cases hj : p j
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
j : ι
hj : p j
⊢ LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)

Tactic:
((ciSup_pos hj).trans_le (le_ciSup bdd ⟨j, hj⟩)).trans gt.le

Premises used: LT.lt.le, Eq.trans_le, ciSup_pos, LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
j : ι
hj : p j
⊢ LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)

Tactic:
exact ((ciSup_pos hj).trans_le (le_ciSup bdd ⟨j, hj⟩)).trans gt.le

Premises used: LT.lt.le, Eq.trans_le, ciSup_pos, LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
j : ι
hj : ¬p j
⊢ LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)

Tactic:
(ciSup_neg hj).le

Premises used: Eq.le, ciSup_neg
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
j : ι
hj : ¬p j
⊢ LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)

Tactic:
exact (ciSup_neg hj).le

Premises used: Eq.le, ciSup_neg
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
⊢ ∀ w < sSup ∅, ∃ (i : ι), w < ⨆ (h : p i), f (Subtype.mk (p := p) i h)

Tactic:
fun w hw ↦ ⟨i, hw.trans_eq (ciSup_neg hi).symm⟩

Premises used: LT.lt.trans_eq, Exists.intro, Eq.symm, ciSup_neg
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
⊢ ∀ w < sSup ∅, ∃ (i : ι), w < ⨆ (h : p i), f (Subtype.mk (p := p) i h)

Tactic:
exact fun w hw ↦ ⟨i, hw.trans_eq (ciSup_neg hi).symm⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
⊢ ⨅ (i : ι), ⨅ (h : p i), f (Subtype.mk (p := p) i h) = min (iInf.{u_1, max 1 u_4} f) (sInf ∅)

Tactic:
cbiSup_eq_of_not_forall (α := αᵒᵈ) hp

Premises used: iInf, cbiSup_eq_of_not_forall, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : OrderBot α
f : ι → α
hs : ⊥ ∈ range f
⊢ iInf f = ⊥

Tactic:
csInf_eq_bot_of_bot_mem hs

Premises used: iInf, csInf_eq_bot_of_bot_mem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : OrderTop α
f : ι → α
hs : ⊤ ∈ range f
⊢ iSup f = ⊤

Tactic:
csSup_eq_top_of_top_mem hs

Premises used: iSup, csSup_eq_top_of_top_mem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Nonempty ι
f : ι → α
⊢ iInf f ∈ range f

Tactic:
csInf_mem (range_nonempty f)

Premises used: csInf_mem, iInf, Set.Mem, Set.range_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Nonempty ι
f : ι → α
n : α
have : ∀ (this : OrderBot α), ⨅ (i : ι), f i = n ↔ (∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i
⊢ ⨅ (i : ι), f i = n ↔ (∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i

Tactic:
have : OrderBot α := WellFoundedLT.toOrderBot α
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Nonempty ι
f : ι → α
n : α
this : OrderBot α
mp : ⨅ (i : ι), f i = n → (∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i
mpr : ((∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i) → ⨅ (i : ι), f i = n
⊢ ⨅ (i : ι), f i = n ↔ (∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i

Tactic:
constructor
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Nonempty ι
f : ι → α
this : OrderBot α
⊢ (∃ (i : ι), f i = ⨅ (i : ι), f i) ∧ ∀ (i : ι), ⨅ (i : ι), f i ≤ f i

Tactic:
⟨ciInf_mem f, ciInf_le (OrderBot.bddBelow ..)⟩

Premises used: ciInf_mem, ciInf_le, And.intro, OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Nonempty ι
f : ι → α
this : OrderBot α
⊢ (∃ (i : ι), f i = ⨅ (i : ι), f i) ∧ ∀ (i : ι), ⨅ (i : ι), f i ≤ f i

Tactic:
exact ⟨ciInf_mem f, ciInf_le (OrderBot.bddBelow ..)⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Nonempty ι
f : ι → α
this : OrderBot α
i : ι
h : ∀ (i_1 : ι), f i ≤ f i_1
⊢ ⨅ (i : ι), f i = f i

Tactic:
le_antisymm (ciInf_le (OrderBot.bddBelow ..) _) (le_ciInf h)

Premises used: le_ciInf, le_antisymm, ciInf_le, OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Nonempty ι
f : ι → α
this : OrderBot α
i : ι
h : ∀ (i_1 : ι), f i ≤ f i_1
⊢ ⨅ (i : ι), f i = f i

Tactic:
exact le_antisymm (ciInf_le (OrderBot.bddBelow ..) _) (le_ciInf h)

Premises used: le_ciInf, le_antisymm, ciInf_le, OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : IsEmpty ι
f : ι → α
rw : Eq.{u_1 + 1} (α := α) (sSup ∅) ⊥
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) ⊥ ⊥
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) ⊥

Tactic:
rw [iSup_of_empty', csSup_empty]

Premises used: csSup_empty, iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
f : False → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : False), f i) ⊥

Tactic:
ciSup_of_empty f

Premises used: ciSup_of_empty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
s : ι → α
a : α
h : BddAbove (range s)
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

Tactic:
simp [iSup, h, le_csSup_iff', upperBounds]

Premises used: iSup, upperBounds, le_csSup_iff'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : Nonempty ι
f : ι → α
a : α
⊢ a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i

Tactic:
le_ciInf_iff (OrderBot.bddBelow _)

Premises used: OrderBot.bddBelow, le_ciInf_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
i : ι
⊢ iInf f ≤ f i

Tactic:
ciInf_le (OrderBot.bddBelow _) _

Premises used: ciInf_le, OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
c : ι
⊢ f c ≤ a → iInf f ≤ a

Tactic:
ciInf_le_of_le (OrderBot.bddBelow _) _

Premises used: ciInf_le_of_le, OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
h : BddAbove (range f)
a : α
⊢ ⨆ (i : ι), f i ≤ a ↔ ∀ (i : ι), f i ≤ a

Tactic:
(csSup_le_iff' h).trans forall_mem_range

Premises used: Set.forall_mem_range, iSup, csSup_le_iff', Iff.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : ∀ (i : ι), f i ≤ a
⊢ ⨆ (i : ι), f i ≤ a

Tactic:
csSup_le' <| forall_mem_range.2 h

Premises used: Iff.mpr, csSup_le', Set.forall_mem_range, iSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), ⊥) ⊥

Tactic:
le_bot_iff.mp (ciSup_le' fun _ ↦ bot_le)

Premises used: le_bot_iff, ciSup_le', Iff.mp, bot_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
a : α
f : ι → α
h : BddAbove (range f)
⊢ a < iSup f ↔ ∃ (i : ι), a < f i

Tactic:
simpa only [not_le, not_forall] using (ciSup_le_iff' h).not

Premises used: not_le, Iff.not, ciSup_le_iff', Classical.not_forall
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : a < ⨆ (i : ι), f i
contrapose! : ∀ (h : ∀ (i : ι), f i ≤ a), ⨆ (i : ι), f i ≤ a
⊢ ∃ (i : ι), a < f i

Tactic:
contrapose! h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : ∀ (i : ι), f i ≤ a
⊢ ⨆ (i : ι), f i ≤ a

Tactic:
ciSup_le' h

Premises used: ciSup_le'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : ∀ (i : ι), f i ≤ a
⊢ ⨆ (i : ι), f i ≤ a

Tactic:
exact ciSup_le' h

Premises used: ciSup_le'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
ι' : Sort u_5
f : ι → α
g : ι' → α
hg : BddAbove (range g)
h : ∀ (i : ι), ∃ (i' : ι'), f i ≤ g i'
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i' : ι'), g i')

Tactic:
ciSup_le' fun i ↦ h i |>.elim <| le_ciSup_of_le hg

Premises used: le_ciSup_of_le, ciSup_le', Exists.elim
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
p : ι → Prop
f : Exists p → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)

Tactic:
le_antisymm ciSup_exists_le <| ciSup_le' fun i ↦ ciSup_le' fun hi ↦ ?_

Premises used: ciSup_le', le_antisymm, ciSup_exists_le