awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
lift : ∀ (s : Finset ι) (h : ∃ x ∈ (↑s : Set ι), sSup ∅ ≤ f x), ⨆ i ∈ (↑s : Set ι), f i ∈ f '' (↑s : Set ι)
⊢ ⨆ i ∈ s, f i ∈ f '' s

Tactic:
lift s to Finset ι using hs

Premises used: Finset
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ (↑s : Set ι), sSup ∅ ≤ f x
⊢ ∃ x ∈ s, sSup ∅ ≤ f x

Tactic:
simp only [Finset.mem_coe] at h

Premises used: Finset.mem_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ (↑s : Set ι), f i ∈ f '' (↑s : Set ι)

Tactic:
simpa using Finset.ciSup_mem_image f h

Premises used: Finset.ciSup_mem_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
lift : ∀ (s : Finset ι) (h : ∃ x ∈ (↑s : Set ι), f x ≤ sInf ∅), ⨅ i ∈ (↑s : Set ι), f i ∈ f '' (↑s : Set ι)
⊢ ⨅ i ∈ s, f i ∈ f '' s

Tactic:
lift s to Finset ι using hs

Premises used: Finset
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ (↑s : Set ι), f x ≤ sInf ∅
⊢ ∃ x ∈ s, f x ≤ sInf ∅

Tactic:
simp only [Finset.mem_coe] at h

Premises used: Finset.mem_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ (↑s : Set ι), f i ∈ f '' (↑s : Set ι)

Tactic:
simpa using Finset.ciInf_mem_image f h

Premises used: Finset.ciInf_mem_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
mp : ⨆ i ∈ s, f i < a → ∀ x ∈ s, f x < a
mpr : (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a
⊢ ⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a

Tactic:
constructor
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x < a

Tactic:
h.trans_le' (le_csSup ?_ ?_)

Premises used: LT.lt.trans_le', le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
mp : BddAbove.{u_2} (α := α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i)
mp₁ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) (f x)
⊢ f x < a

Tactic:
refine h.trans_le' (le_csSup ?_ ?_)

Premises used: LT.lt.trans_le', le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ BddAbove.{u_2} (α := α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i)

Tactic:
(((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove

Premises used: Set.Finite.union, Set.Finite.subset, Set.Finite.image, EmptyCollection.emptyCollection, Set.Finite.bddAbove, Set.finite_singleton, SupSet.sSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
mp : (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sSup ∅}
⊢ BddAbove.{u_2} (α := α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i)

Tactic:
refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove

Premises used: Set.Finite.union, Set.Finite.subset, Set.Finite.image, EmptyCollection.emptyCollection, Set.Finite.bddAbove, Set.finite_singleton, SupSet.sSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
a_1 : α
mp : ∀ (x : ι) (h : (if x ∈ s then f x else sSup ∅) = a_1), a_1 = sSup ∅ ∨ ∃ x ∈ s, f x = a_1
⊢ Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) a_1 → a_1 ∈ f '' s ∪ {sSup ∅}

Tactic:
simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]

Premises used: Set.mem_range, Set.mem_image, forall_exists_index, ciSup_eq_ite, Set.mem_insert_iff, dite_eq_ite, Set.union_singleton
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
a_1 : α
⊢ ∀ (x : ι) (h : (if x ∈ s then f x else sSup ∅) = a_1), a_1 = sSup ∅ ∨ ∃ x ∈ s, f x = a_1

Tactic:
grind
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
mp : (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sSup ∅}
mp₁ : ∀ ⦃a : α⦄, Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) a → a ∈ f '' s ∪ {sSup ∅}
mp₂ : ∀ ⦃a : α⦄ (x : ι) (h : (if x ∈ s then f x else sSup ∅) = a), a = sSup ∅ ∨ ∃ x ∈ s, f x = a
⊢ BddAbove.{u_2} (α := α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i)

Tactic:
classical
      refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove
      intro
      simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind

Premises used: Set.Finite.union, Set.mem_range, Set.mem_image, forall_exists_index, Set.Finite.subset, Set.Finite.image, ciSup_eq_ite, Set.mem_insert_iff, dite_eq_ite, EmptyCollection.emptyCollection, Set.Finite.bddAbove, Set.union_singleton, Set.finite_singleton, SupSet.sSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ ∃ (y : ι), ⨆ (_ : y ∈ s), f y = f x

Tactic:
⟨x, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
mp : ⨆ (_ : x ∈ s), f x = f x
⊢ ∃ (y : ι), ⨆ (_ : y ∈ s), f y = f x

Tactic:
refine ⟨x, ?_⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ ⨆ (_ : x ∈ s), f x = f x

Tactic:
simp [hx]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i ∈ f '' s

Tactic:
have := hs.ciSup_mem_image _ h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
this : ⨆ i ∈ s, f i ∈ f '' s
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a

Tactic:
grind
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
mp : a < ⨅ i ∈ s, f i → ∀ x ∈ s, a < f x
mpr : (∀ x ∈ s, a < f x) → a < ⨅ i ∈ s, f i
⊢ a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x

Tactic:
constructor
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ a < f x

Tactic:
h.trans_le (csInf_le ?_ ?_)

Premises used: LT.lt.trans_le, csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
mp : BddBelow.{u_2} (α := α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i)
mp₁ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i) (f x)
⊢ a < f x

Tactic:
refine h.trans_le (csInf_le ?_ ?_)

Premises used: LT.lt.trans_le, csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ BddBelow.{u_2} (α := α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i)

Tactic:
(((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow

Premises used: Set.Finite.union, Set.Finite.subset, Set.Finite.image, Set.Finite.bddBelow, EmptyCollection.emptyCollection, Set.finite_singleton, InfSet.sInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
mp : (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sInf ∅}
⊢ BddBelow.{u_2} (α := α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i)

Tactic:
refine (((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow

Premises used: Set.Finite.union, Set.Finite.subset, Set.Finite.image, Set.Finite.bddBelow, EmptyCollection.emptyCollection, Set.finite_singleton, InfSet.sInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
a_1 : α
mp : ∀ (x : ι) (h : (if x ∈ s then f x else sInf ∅) = a_1), a_1 = sInf ∅ ∨ ∃ x ∈ s, f x = a_1
⊢ Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i) a_1 → a_1 ∈ f '' s ∪ {sInf ∅}

Tactic:
simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]

Premises used: Set.mem_range, Set.mem_image, forall_exists_index, ciInf_eq_ite, Set.mem_insert_iff, dite_eq_ite, Set.union_singleton
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
a_1 : α
⊢ ∀ (x : ι) (h : (if x ∈ s then f x else sInf ∅) = a_1), a_1 = sInf ∅ ∨ ∃ x ∈ s, f x = a_1

Tactic:
grind
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
mp : (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sInf ∅}
mp₁ : ∀ ⦃a : α⦄, Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i) a → a ∈ f '' s ∪ {sInf ∅}
mp₂ : ∀ ⦃a : α⦄ (x : ι) (h : (if x ∈ s then f x else sInf ∅) = a), a = sInf ∅ ∨ ∃ x ∈ s, f x = a
⊢ BddBelow.{u_2} (α := α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i)

Tactic:
classical
      refine (((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow
      intro
      simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind

Premises used: Set.Finite.union, Set.mem_range, Set.mem_image, forall_exists_index, ciInf_eq_ite, Set.Finite.subset, Set.Finite.image, Set.Finite.bddBelow, Set.mem_insert_iff, dite_eq_ite, EmptyCollection.emptyCollection, Set.union_singleton, Set.finite_singleton, InfSet.sInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ ∃ (y : ι), ⨅ (_ : y ∈ s), f y = f x

Tactic:
⟨x, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
mp : ⨅ (_ : x ∈ s), f x = f x
⊢ ∃ (y : ι), ⨅ (_ : y ∈ s), f y = f x

Tactic:
refine ⟨x, ?_⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h_1 : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ ⨅ (_ : x ∈ s), f x = f x

Tactic:
simp [hx]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
⊢ ⨅ i ∈ s, f i ∈ f '' s

Tactic:
have := hs.ciInf_mem_image _ h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
this : ⨅ i ∈ s, f i ∈ f '' s
⊢ ∃ x ∈ s, f x = ⨅ i ∈ s, f i

Tactic:
simp only [mem_image] at this

Premises used: Set.mem_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
this : ∃ x ∈ s, f x = ⨅ i ∈ s, f i
mpr : ∀ (w : ι) (hmem : w ∈ s) (hx : f w = ⨅ i ∈ s, f i), a < ⨅ i ∈ s, f i
⊢ a < ⨅ i ∈ s, f i

Tactic:
obtain ⟨_, hmem, hx⟩ := this
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
w : ι
hmem : w ∈ s
hx : f w = ⨅ i ∈ s, f i
mpr : a < f w
⊢ a < ⨅ i ∈ s, f i

Tactic:
rw [← hx]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
w : ι
hmem : w ∈ s
hx : f w = ⨅ i ∈ s, f i
⊢ a < f w

Tactic:
H _ hmem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
w : ι
hmem : w ∈ s
hx : f w = ⨅ i ∈ s, f i
⊢ a < f w

Tactic:
exact H _ hmem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ∃ x ∈ l.toFinset, sSup ∅ ≤ f x

Tactic:
simpa using h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : 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:
simpa using l.toFinset.ciSup_mem_image f (by simpa using h)

Premises used: Finset.ciSup_mem_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : 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:
classical
  simpa using l.toFinset.ciSup_mem_image f (by simpa using h)
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ∃ x ∈ l.toFinset, f x ≤ sInf ∅

Tactic:
simpa using h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : 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:
simpa using l.toFinset.ciInf_mem_image f (by simpa using h)

Premises used: Finset.ciInf_mem_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : 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:
classical
  simpa using l.toFinset.ciInf_mem_image f (by simpa using h)
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ∃ x ∈ s.toFinset, sSup ∅ ≤ f x

Tactic:
simpa using h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : 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:
simpa using s.toFinset.ciSup_mem_image f (by simpa using h)

Premises used: Finset.ciSup_mem_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : 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:
classical
  simpa using s.toFinset.ciSup_mem_image f (by simpa using h)
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ∃ x ∈ s.toFinset, f x ≤ sInf ∅

Tactic:
simpa using h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : 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:
simpa using s.toFinset.ciInf_mem_image f (by simpa using h)

Premises used: Finset.ciInf_mem_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : 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:
classical
  simpa using s.toFinset.ciInf_mem_image f (by simpa using h)
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : Nonempty ι
inst_2 : Finite ι
f : ι → α
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
Nonempty.csSup_mem (range_nonempty f) (finite_range f)

Premises used: Set.Mem, iSup, setOf, Set.finite_range, Set.Nonempty.csSup_mem, Set.range_nonempty, Set.range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : Nonempty ι
inst_2 : Finite ι
f : ι → α
⊢ ∃ (i : ι), f i = ⨅ (i : ι), f i

Tactic:
Nonempty.csInf_mem (range_nonempty f) (finite_range f)

Premises used: iInf, Set.Mem, setOf, Set.finite_range, Set.range_nonempty, Set.range, Set.Nonempty.csInf_mem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLattice α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup' H f ≤ a ↔ sSup (f '' (↑s : Set ι)) ≤ a

Tactic:
simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (H.to_set.image f)]

Premises used: csSup_le_iff, Set.Finite.image, Set.Nonempty.image, Finset.finite_toSet, Set.Finite.bddAbove, Finset.Nonempty.to_set
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLattice α
s : Finset ι
H : s.Nonempty
f : ι → α
⊢ s.inf' H f = sInf (f '' (↑s : Set ι))

Tactic:
sup'_eq_csSup_image (α := αᵒᵈ) _ H _

Premises used: Finset.inf', Finset.sup'_eq_csSup_image, WithTop.some, WithTop.untop, OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
rw : sSup (id '' (↑s : Set α)) = sSup (↑s : Set α)
rw₁ rw₂ : sSup (↑s : Set α) = sSup (↑s : Set α)
⊢ s.sup' hs id = sSup (↑s : Set α)

Tactic:
rw [sup'_eq_csSup_image s hs, Set.image_id]

Premises used: Finset.sup'_eq_csSup_image, Set.image_id
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
⊢ s.inf' hs id = sInf (↑s : Set α)

Tactic:
sup'_id_eq_csSup (α := αᵒᵈ) _ hs

Premises used: Finset.inf', setOf, WithTop.some, WithTop.untop, Finset.sup'_id_eq_csSup, OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : Fintype ι
inst_2 : Nonempty ι
f : ι → α
⊢ sup' univ ⋯ f = ⨆ (i : ι), f i

Tactic:
simp [sup'_eq_csSup_image, iSup]

Premises used: iSup, Finset.sup'_eq_csSup_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : Fintype ι
inst_2 : Nonempty ι
f : ι → α
⊢ inf' univ ⋯ f = ⨅ (i : ι), f i

Tactic:
simp [inf'_eq_csInf_image, iInf]

Premises used: iInf, Finset.inf'_eq_csInf_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : Fintype ι
f : ι → α
⊢ sup univ f = ⨆ (i : ι), f i

Tactic:
le_antisymm
    (Finset.sup_le fun _ _ => le_ciSup (finite_range _).bddAbove _)
    (ciSup_le' fun _ => Finset.le_sup (mem_univ _))

Premises used: Finset.mem_univ, Set.finite_range, ciSup_le', Finset.sup_le, le_antisymm, le_ciSup, Set.Finite.bddAbove, Finset.le_sup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : DecidableEq ι
f : ι → α
s t : Finset ι
this : ∀ (st : Finset ι), BddAbove.{u_2} (α := α) (Set.range fun (x : ι) ↦ ⨆ (_ : x ∈ st), f x)
⊢ Eq.{u_2 + 1} (α := α) (⨆ x ∈ s ∪ t, f x) (max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x))

Tactic:
simp [ciSup_or', ciSup_sup_eq, this]

Premises used: ciSup_or', ciSup_sup_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : DecidableEq ι
f : ι → α
s t : Finset ι
suffices : ∀ (st : Finset ι), BddAbove.{u_2} (α := α) (Set.range fun (x : ι) ↦ ⨆ (_ : x ∈ st), f x)
⊢ Eq.{u_2 + 1} (α := α) (⨆ x ∈ s ∪ t, f x) (max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x))

Tactic:
suffices ∀ st : Finset ι, BddAbove <| .range fun x ↦ ⨆ (_ : x ∈ st), f x by
    simp [ciSup_or', ciSup_sup_eq, this]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : DecidableEq ι
f : ι → α
s t : Finset ι
⊢ ∀ (st : Finset ι), BddAbove.{u_2} (α := α) (Set.range fun (x : ι) ↦ ⨆ (_ : x ∈ st), f x)

Tactic:
fun st ↦ ⟨st.sup f, fun a ⟨i, ha⟩ ↦ ha ▸ ?_⟩

Premises used: Eq.rec, LE.le, BddAbove, Set.Nonempty, Exists.intro, Finset.sup, _private.0.Finset.ciSup_union.match_1
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : DecidableEq ι
f : ι → α
s t : Finset ι
refine :
  ∀ (st : Finset ι) (a : α),
    Membership.mem (γ := Set α) (Set.range fun (x : ι) ↦ ⨆ (_ : x ∈ st), f x) a →
      ∀ (i : ι) (ha : (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i = a),
        (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i ≤ st.sup f
⊢ ∀ (st : Finset ι), BddAbove.{u_2} (α := α) (Set.range fun (x : ι) ↦ ⨆ (_ : x ∈ st), f x)

Tactic:
refine fun st ↦ ⟨st.sup f, fun a ⟨i, ha⟩ ↦ ha ▸ ?_⟩