awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : ¬S ⊆ {⊤}
neg :
  ∀ (haS : ⊤ ∈ S),
    LE.le (α := WithTop (WithBot α))
      (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ⊤
neg₁ :
  ∀ (a : WithBot α) (haS : (↑a : WithTop (WithBot α)) ∈ S),
    (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ≤
      (↑a : WithTop (WithBot α))
⊢ (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ≤ a

Tactic:
cases a
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
haS : ⊤ ∈ S
⊢ LE.le (α := WithTop (WithBot α))
    (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
haS : ⊤ ∈ S
⊢ LE.le (α := WithTop (WithBot α))
    (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a : WithBot α
haS : (↑a : WithTop (WithBot α)) ∈ S
neg : sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) ≤ a
⊢ (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ≤
    (↑a : WithTop (WithBot α))

Tactic:
apply WithTop.coe_le_coe.2

Premises used: Iff.mpr, WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a : WithBot α
haS : (↑a : WithTop (WithBot α)) ∈ S
⊢ sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) ≤ a

Tactic:
csInf_le ?_ haS

Premises used: csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a : WithBot α
haS : (↑a : WithTop (WithBot α)) ∈ S
neg : BddBelow (α := WithBot α) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)
⊢ sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) ≤ a

Tactic:
refine csInf_le ?_ haS

Premises used: csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a : WithBot α
haS : (↑a : WithTop (WithBot α)) ∈ S
h : Membership.mem (γ := Set (WithBot α)) (lowerBounds ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) ⊥
⊢ BddBelow (α := WithBot α) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)

Tactic:
use ⊥
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a : WithBot α
haS : (↑a : WithTop (WithBot α)) ∈ S
b : WithBot α
h : Membership.mem (γ := Set (WithBot α)) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) b → ⊥ ≤ b
⊢ Membership.mem (γ := Set (WithBot α)) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) b → ⊥ ≤ b

Tactic:
_
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a : WithBot α
haS : (↑a : WithTop (WithBot α)) ∈ S
b : WithBot α
h : Membership.mem (γ := Set (WithBot α)) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) b
⊢ ⊥ ≤ b

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a : WithBot α
haS : (↑a : WithTop (WithBot α)) ∈ S
b : WithBot α
h : Membership.mem (γ := Set (WithBot α)) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) b
⊢ ⊥ ≤ b

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
this : InfSet α :=
  { sInf := fun (s : Set α) ↦ if hs : s.Nonempty then WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ s hs else ⊥ }
s : Set α
h_1 : BddBelow s
hn : s.Nonempty
simp : IsGLB s (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ s hn)
⊢ IsGLB s (sInf s)

Tactic:
simp only [dif_pos hn]

Premises used: dif_pos
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
this : InfSet α :=
  { sInf := fun (s : Set α) ↦ if hs : s.Nonempty then WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ s hs else ⊥ }
s : Set α
h_1 : BddBelow s
hn : s.Nonempty
⊢ IsGLB s (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ s hn)

Tactic:
IsLeast.isGLB ⟨h.wf.min_mem s hn, fun _ hx ↦ h.wf.min_le hx⟩

Premises used: WellFounded.min_mem, IsLeast.isGLB, WellFounded.min_le, IsWellFounded.wf, And.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
this : InfSet α :=
  { sInf := fun (s : Set α) ↦ if hs : s.Nonempty then WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ s hs else ⊥ }
s : Set α
h_1 : BddBelow s
hn : s.Nonempty
⊢ IsGLB s (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ s hn)

Tactic:
exact IsLeast.isGLB ⟨h.wf.min_mem s hn, fun _ hx ↦ h.wf.min_le hx⟩

Premises used: WellFounded.min_mem, IsLeast.isGLB, WellFounded.min_le, IsWellFounded.wf, And.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
s : Set α
H : ¬BddAbove s
⊢ ¬(upperBounds s).Nonempty

Tactic:
rw [BddAbove] at H

Premises used: BddAbove
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
s : Set α
H : ¬(upperBounds s).Nonempty
⊢ sSup s = sSup ∅

Tactic:
simp [sSup, H, bot_unique (WellFounded.min_le _ (mem_univ _))]

Premises used: WellFounded.min_le, Set.mem_univ, bot_unique, SupSet.sSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
⊢ Eq.{u_5 + 1} (α := α) (sSup ∅) ⊥

Tactic:
simp [sSup, bot_unique (WellFounded.min_le _ (mem_univ _))]

Premises used: WellFounded.min_le, Set.mem_univ, bot_unique, SupSet.sSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ sSup (↑s : Set α) = s.max' h

Tactic:
eq_of_forall_ge_iff fun _ => (csSup_le_iff s.bddAbove h.to_set).trans (s.max'_le_iff h).symm

Premises used: csSup_le_iff, Finset.max'_le_iff, Finset.bddAbove, eq_of_forall_ge_iff, Iff.trans, Finset.Nonempty.to_set, Iff.symm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ sInf (↑s : Set α) = s.min' h

Tactic:
@Finset.Nonempty.csSup_eq_max' αᵒᵈ _ s h

Premises used: Finset.min', Finset.inf', setOf, WithTop.some, Finset.Nonempty.csSup_eq_max', WithTop.untop, OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
rw : s.max' h ∈ s
⊢ sSup (↑s : Set α) ∈ s

Tactic:
rw [h.csSup_eq_max']

Premises used: Finset.Nonempty.csSup_eq_max'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ s.max' h ∈ s

Tactic:
s.max'_mem _

Premises used: Finset.max'_mem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ s.max' h ∈ s

Tactic:
exact s.max'_mem _

Premises used: Finset.max'_mem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ sInf (↑s : Set α) ∈ s

Tactic:
@Finset.Nonempty.csSup_mem αᵒᵈ _ _ h

Premises used: Set.Mem, setOf, Finset.Nonempty.csSup_mem, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
h : s.Nonempty
hs : s.Finite
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
h : s.Nonempty
hs : s.Finite
lift : ∀ (s : Finset α) (h : (↑s : Set α).Nonempty), sSup (↑s : Set α) ∈ (↑s : Set α)
⊢ sSup s ∈ s

Tactic:
lift s to Finset α using hs

Premises used: Finset
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Finset α
h : (↑s : Set α).Nonempty
⊢ sSup (↑s : Set α) ∈ (↑s : Set α)

Tactic:
Finset.Nonempty.csSup_mem h

Premises used: Finset.Nonempty.csSup_mem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Finset α
h : (↑s : Set α).Nonempty
⊢ sSup (↑s : Set α) ∈ (↑s : Set α)

Tactic:
exact Finset.Nonempty.csSup_mem h

Premises used: Finset.Nonempty.csSup_mem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
h : s.Nonempty
hs : s.Finite
⊢ sInf s ∈ s

Tactic:
@Set.Nonempty.csSup_mem αᵒᵈ _ _ h hs

Premises used: Set.Mem, Set.Nonempty.csSup_mem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
a : α
hs : s.Finite
h : s.Nonempty
⊢ sSup s < a ↔ ∀ x ∈ s, x < a

Tactic:
⟨fun h _ hx => (le_csSup hs.bddAbove hx).trans_lt h, fun H => H _ <| h.csSup_mem hs⟩

Premises used: Set.Nonempty.csSup_mem, Iff.intro, le_csSup, Set.Finite.bddAbove, LE.le.trans_lt, SupSet.sSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
a : α
hs : s.Finite
h : s.Nonempty
⊢ a < sInf s ↔ ∀ x ∈ s, a < x

Tactic:
@Set.Finite.csSup_lt_iff αᵒᵈ _ _ _ hs h

Premises used: Set.Mem, Set.Finite.csSup_lt_iff, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
rw : sSup (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) = sSup (f '' (↑s : Set ι))
⊢ ⨆ i ∈ s, f i = (image f s).max' h'

Tactic:
rw [iSup, ← h'.csSup_eq_max', coe_image]

Premises used: iSup, Finset.coe_image, Finset.Nonempty.csSup_eq_max'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ sSup (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) = sSup (f '' (↑s : Set ι))

Tactic:
csSup_eq_csSup_of_forall_exists_le ?_ ?_

Premises used: csSup_eq_csSup_of_forall_exists_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
refine_1 :
  ∀ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x → ∃ y ∈ f '' (↑s : Set ι), x ≤ y
refine_2 :
  ∀ y ∈ f '' (↑s : Set ι), ∃ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x ∧ y ≤ x
⊢ sSup (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) = sSup (f '' (↑s : Set ι))

Tactic:
refine csSup_eq_csSup_of_forall_exists_le ?_ ?_

Premises used: csSup_eq_csSup_of_forall_exists_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
refine_1 : ∀ (a : ι), ∃ a_1 ∈ s, (if a ∈ s then f a else sSup ∅) ≤ f a_1
⊢ ∀ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x → ∃ y ∈ f '' (↑s : Set ι), x ≤ y

Tactic:
simp only [ciSup_eq_ite, dite_eq_ite, Set.mem_range, Set.mem_image, mem_coe,
      exists_exists_and_eq_and, forall_exists_index, forall_apply_eq_imp_iff]

Premises used: Set.mem_range, Set.mem_image, forall_exists_index, exists_exists_and_eq_and, ciSup_eq_ite, dite_eq_ite, forall_apply_eq_imp_iff, 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
h' : (image f s).Nonempty
i : ι
pos : i ∈ s → ∃ a ∈ s, f i ≤ f a
neg : i ∉ s → ∃ a ∈ s, sSup ∅ ≤ f a
⊢ ∃ a ∈ s, (if i ∈ s then f i else sSup ∅) ≤ f a

Tactic:
split_ifs
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h_1 : i ∈ s
⊢ i ∈ s

Tactic:
assumption
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h_1 : i ∈ s
⊢ ∃ a ∈ s, f i ≤ f a

Tactic:
exact ⟨_, by assumption, le_rfl⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h_1 : i ∉ s
⊢ ∃ a ∈ s, sSup ∅ ≤ f a

Tactic:
assumption
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
refine_2 : ∀ a ∈ s, ∃ (a_2 : ι), f a ≤ if a_2 ∈ s then f a_2 else sSup ∅
⊢ ∀ y ∈ f '' (↑s : Set ι), ∃ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x ∧ y ≤ x

Tactic:
simp only [Set.mem_image, mem_coe, ciSup_eq_ite, dite_eq_ite, Set.mem_range,
      exists_exists_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Premises used: Set.mem_range, and_imp, Set.mem_image, forall_exists_index, exists_exists_eq_and, ciSup_eq_ite, dite_eq_ite, Finset.mem_coe, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
hi : i ∈ s
⊢ ∃ (a : ι), f i ≤ if a ∈ s then f a else sSup ∅

Tactic:
⟨i, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
hi : i ∈ s
refine_2 : f i ≤ if i ∈ s then f i else sSup ∅
⊢ ∃ (a : ι), f i ≤ if a ∈ s then f a else sSup ∅

Tactic:
refine ⟨i, ?_⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
hi : i ∈ s
⊢ f i ≤ if i ∈ s then f i else sSup ∅

Tactic:
simp [hi]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
rw : sSup (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) = (image f s).max' h'
rw₁ : sSup (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) = sSup (↑(image f s) : Set α)
rw₂ rw₃ rw₄ : sSup (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) = sSup (f '' (↑s : Set ι))
refine_1 :
  ∀ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x → ∃ y ∈ f '' (↑s : Set ι), x ≤ y
refine_2 refine_2₁ :
  ∀ y ∈ f '' (↑s : Set ι), ∃ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x ∧ y ≤ x
⊢ ⨆ i ∈ s, f i = (image f s).max' h'

Tactic:
classical
  rw [iSup, ← h'.csSup_eq_max', coe_image]
  refine csSup_eq_csSup_of_forall_exists_le ?_ ?_
  · simp only [ciSup_eq_ite, dite_eq_ite, Set.mem_range, Set.mem_image, mem_coe,
      exists_exists_and_eq_and, forall_exists_index, forall_apply_eq_imp_iff]
    intro i
    split_ifs
    · exact ⟨_, by assumption, le_rfl⟩
    · assumption
  · simp only [Set.mem_image, mem_coe, ciSup_eq_ite, dite_eq_ite, Set.mem_range,
      exists_exists_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    intro i hi
    refine ⟨i, ?_⟩
    simp [hi]

Premises used: Set.mem_range, iSup, and_imp, Set.mem_image, forall_exists_index, Finset.coe_image, Finset.Nonempty.csSup_eq_max', exists_exists_eq_and, exists_exists_and_eq_and, ciSup_eq_ite, dite_eq_ite, forall_apply_eq_imp_iff, Finset.mem_coe, forall_apply_eq_imp_iff₂, csSup_eq_csSup_of_forall_exists_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
rw :
  Eq (α := αᵒᵈ) (⨆ (i : ι), (OrderDual.toDual : (a : α) → αᵒᵈ) (⨅ (_ : i ∈ s), f i))
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)
⊢ ⨅ i ∈ s, f i = (image f s).min' h'

Tactic:
rw [← OrderDual.toDual_inj, toDual_min', toDual_iInf]

Premises used: Finset.toDual_min', OrderDual.toDual_inj, toDual_iInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
simp :
  Eq (α := αᵒᵈ) (⨆ i ∈ s, (OrderDual.toDual : (a : α) → αᵒᵈ) (f i))
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)
⊢ Eq (α := αᵒᵈ) (⨆ (i : ι), (OrderDual.toDual : (a : α) → αᵒᵈ) (⨅ (_ : i ∈ s), f i))
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)

Tactic:
simp only [toDual_iInf]

Premises used: toDual_iInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
rw :
  Eq (α := αᵒᵈ) (max' (image (fun (i : ι) ↦ (OrderDual.toDual : (a : α) → αᵒᵈ) (f i)) s) ⋯)
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)
⊢ Eq (α := αᵒᵈ) (⨆ i ∈ s, (OrderDual.toDual : (a : α) → αᵒᵈ) (f i))
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)

Tactic:
rw [ciSup_eq_max'_image _ h]

Premises used: Finset.ciSup_eq_max'_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
simp :
  Eq (α := αᵒᵈ) (max' (image (fun (i : ι) ↦ (OrderDual.toDual : (a : α) → αᵒᵈ) (f i)) s) ⋯)
    (max' (image ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) s) ⋯)
⊢ Eq (α := αᵒᵈ) (max' (image (fun (i : ι) ↦ (OrderDual.toDual : (a : α) → αᵒᵈ) (f i)) s) ⋯)
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)

Tactic:
simp only [image_image]

Premises used: Finset.image_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ Eq (α := αᵒᵈ) (max' (image (fun (i : ι) ↦ (OrderDual.toDual : (a : α) → αᵒᵈ) (f i)) s) ⋯)
    (max' (image ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) s) ⋯)

Tactic:
congr
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
rw :
  Eq (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) (⨅ i ∈ s, f i) : αᵒᵈ)
    ((OrderDual.toDual : (a : α) → αᵒᵈ) ((image f s).min' h') : αᵒᵈ)
rw₁ :
  Eq (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) (⨅ i ∈ s, f i) : αᵒᵈ)
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯ : αᵒᵈ)
rw₂ rw₃ rw₄ :
  Eq (α := αᵒᵈ) (⨆ (i : ι), (OrderDual.toDual : (a : α) → αᵒᵈ) (⨅ (_ : i ∈ s), f i))
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)
rw₅ :
  Eq (α := αᵒᵈ) (⨆ i ∈ s, (OrderDual.toDual : (a : α) → αᵒᵈ) (f i))
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)
rw₆ :
  Eq (α := αᵒᵈ) (max' (image (fun (i : ι) ↦ (OrderDual.toDual : (a : α) → αᵒᵈ) (f i)) s) ⋯)
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)
rw₇ :
  Eq (α := αᵒᵈ) (max' (image (fun (i : ι) ↦ (OrderDual.toDual : (a : α) → αᵒᵈ) (f i)) s) ⋯)
    (max' (image ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) s) ⋯)
⊢ ⨅ i ∈ s, f i = (image f s).min' h'

Tactic:
classical
  rw [← OrderDual.toDual_inj, toDual_min', toDual_iInf]
  simp only [toDual_iInf]
  rw [ciSup_eq_max'_image _ h]
  simp only [image_image]
  congr

Premises used: Finset.ciSup_eq_max'_image, Finset.toDual_min', OrderDual.toDual_inj, toDual_iInf, Finset.image_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
rw : (image f s).max' ⋯ ∈ image f s
⊢ ⨆ i ∈ s, f i ∈ image f s

Tactic:
rw [ciSup_eq_max'_image _ h]

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

Tactic:
max'_mem (image f s) _

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

Tactic:
exact max'_mem (image f s) _

Premises used: Finset.max'_mem, Finset.image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
rw : (image f s).min' ⋯ ∈ image f s
⊢ ⨅ i ∈ s, f i ∈ image f s

Tactic:
rw [ciInf_eq_min'_image _ h]

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

Tactic:
min'_mem (image f s) _

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

Tactic:
exact min'_mem (image f s) _

Premises used: Finset.min'_mem, Finset.image
-- 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
⊢ s.Finite

Tactic:
hs