awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
⊢ sSup (f '' Icc a b) = f b
have rw : ∀ (h' : MonotoneOn f (Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)))
  (this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)),
  sSup (f '' Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)) = f b
Tactic: rw [this] at h' ⊢
Cleared hypotheses: h', this
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
have rw : Icc a b = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc a b
Tactic: rw [Icc_toDual]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ sInf (f '' Icc a b) = f b
have this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
Tactic: have : Icc a b = Icc (α := αᵒᵈ) (toDual b) (toDual a) := by rw [Icc_toDual]; rfl
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
⊢ sInf (f '' Icc a b) = f b
have rw : ∀ (h' : AntitoneOn f (Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)))
  (this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)),
  sInf (f '' Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)) = f b
Tactic: rw [this] at h' ⊢
Cleared hypotheses: h', this
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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 α)
ha : a ∈ upperBounds S
⊢ sSup S ≤ a
have inl : ∀ (h : S = ∅), sSup S ≤ a
Tactic: rcases S.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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 α)
ha : a ∈ upperBounds S
inl : ∀ (h : S = ∅), sSup S ≤ a
⊢ sSup S ≤ a
have inr : ∀ (h : S.Nonempty), sSup S ≤ a
Tactic: rcases S.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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 α)
ha : a ∈ upperBounds S
h : S = ∅
⊢ sSup S ≤ a
have inl : (if ⊤ ∈ S then ⊤
  else
    if BddAbove (α := WithBot α) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) then
      (↑(sSup ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α))
    else ⊤) ≤
  a
Tactic: change ite _ _ _ ≤ a
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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
⊢ (if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤
    else (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α))) ≤
    a
have simp : (if S ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α))) ≤ a
Tactic: simp only [OrderBot.bddBelow, not_true_eq_false, or_false]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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
⊢ (if S ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α))) ≤
    a
have pos : ∀ (h₁ : S ⊆ {⊤}), ⊤ ≤ a
Tactic: split_ifs with h₁
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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
pos : ∀ (h₁ : S ⊆ {⊤}), ⊤ ≤ a
⊢ (if S ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α))) ≤
    a
have neg : ∀ (h₁ : ¬S ⊆ {⊤}), (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ≤ a
Tactic: split_ifs with h₁
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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 ⊆ {⊤}
⊢ ⊤ ≤ a
have pos : ∀ (haS : ⊤ ∈ S), LE.le.{u_5} (α := WithTop (WithBot α)) ⊤ ⊤
Tactic: cases a
Cleared hypotheses: a, haS
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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 ⊆ {⊤}
pos : ∀ (haS : ⊤ ∈ S), LE.le.{u_5} (α := WithTop (WithBot α)) ⊤ ⊤
⊢ ⊤ ≤ a
have pos₁ : ∀ (a : WithBot α) (haS : (↑a : WithTop (WithBot α)) ∈ S), ⊤ ≤ (↑a : WithTop (WithBot α))
Tactic: cases a
Cleared hypotheses: a, haS
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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 ⊆ {⊤}
⊢ (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ≤ a
have neg : ∀ (haS : ⊤ ∈ S),
  LE.le (α := WithTop (WithBot α))
    (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ⊤
Tactic: cases a
Cleared hypotheses: a, haS
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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 α)) ⊤
⊢ (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ≤ a
have neg₁ : ∀ (a : WithBot α) (haS : (↑a : WithTop (WithBot α)) ∈ S),
  (↑(sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) : WithTop (WithBot α)) ≤
    (↑a : WithTop (WithBot α))
Tactic: cases a
Cleared hypotheses: a, haS
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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)) : WithTop (WithBot α)) ≤
    (↑a : WithTop (WithBot α))
have neg : sInf ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S) ≤ a
Tactic: apply WithTop.coe_le_coe.2
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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
have neg : BddBelow (α := WithBot α) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)
Tactic: refine csInf_le ?_ haS
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
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
⊢ BddBelow (α := WithBot α) ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)
have h : Membership.mem (γ := Set (WithBot α)) (lowerBounds ((fun (a : WithBot α) ↦ (↑a : WithTop (WithBot α))) ⁻¹' S)) ⊥
Tactic: use ⊥
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Defs (goal)
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 (sInf s)
have simp : IsGLB s (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) sorry s hn)
Tactic: simp only [dif_pos hn]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Defs (hypothesis)
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
⊢ sSup s = sSup ∅
have H₁ : ¬(upperBounds s).Nonempty
Tactic: rw [BddAbove] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Finset α
h : s.Nonempty
⊢ sSup (↑s : Set α) ∈ s
have rw : s.max' h ∈ s
Tactic: rw [h.csSup_eq_max']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
h : s.Nonempty
hs : s.Finite
⊢ sSup s ∈ s
have lift : ∀ (s : Finset α) (h : (↑s : Set α).Nonempty), sSup (↑s : Set α) ∈ (↑s : Set α)
Tactic: lift s to Finset α using hs
Cleared hypotheses: s, h, hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ⨆ i ∈ s, f i = (image f s).max' h'
have rw : sSup (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) = sSup (f '' (↑s : Set ι))
Tactic: rw [iSup, ← h'.csSup_eq_max', coe_image]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 ι))
have refine_1 : ∀ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x → ∃ y ∈ f '' (↑s : Set ι), x ≤ y
Tactic: refine csSup_eq_csSup_of_forall_exists_le ?_ ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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
⊢ sSup (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) = sSup (f '' (↑s : Set ι))
have refine_2 : ∀ y ∈ f '' (↑s : Set ι), ∃ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x ∧ y ≤ x
Tactic: refine csSup_eq_csSup_of_forall_exists_le ?_ ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x → ∃ y ∈ f '' (↑s : Set ι), x ≤ y
have refine_1 : ∀ (a : ι), ∃ a_1 ∈ s, (if a ∈ s then f a else sSup ∅) ≤ f a_1
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]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
⊢ ∃ a ∈ s, (if i ∈ s then f i else sSup ∅) ≤ f a
have pos : i ∈ s → ∃ a ∈ s, f i ≤ f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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
⊢ ∃ a ∈ s, (if i ∈ s then f i else sSup ∅) ≤ f a
have neg : i ∉ s → ∃ a ∈ s, sSup ∅ ≤ f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ y ∈ f '' (↑s : Set ι), ∃ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x ∧ y ≤ x
have refine_2 : ∀ a ∈ s, ∃ (a_2 : ι), f a ≤ if a_2 ∈ s then f a_2 else sSup ∅
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₂]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 ∅
have refine_2 : f i ≤ if i ∈ s then f i else sSup ∅
Tactic: refine ⟨i, ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ⨆ i ∈ s, f i = (image f s).max' h'
have rw : sSup (Set.range fun (i : ι) ↦ ⨆ (_ : 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]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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'
⊢ ⨆ i ∈ s, f i = (image f s).max' h'
have rw₁ : sSup (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) = sSup (↑(image f s) : Set α)
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]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 α)
⊢ ⨆ i ∈ s, f i = (image f s).max' h'
have rw₂ : sSup (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) = sSup (f '' (↑s : Set ι))
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]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 ι))
⊢ ⨆ i ∈ s, f i = (image f s).max' h'
have refine_1 : ∀ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x → ∃ y ∈ f '' (↑s : Set ι), x ≤ y
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]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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
⊢ ⨆ i ∈ s, f i = (image f s).max' h'
have refine_2 : ∀ y ∈ f '' (↑s : Set ι), ∃ (x : α), Membership.mem (γ := Set α) (Set.range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) x ∧ y ≤ x
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]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ ⨅ i ∈ s, f i = (image f s).min' h'
have rw : Eq (α := αᵒᵈ) (⨆ (i : ι), (OrderDual.toDual : (a : α) → αᵒᵈ) (⨅ (_ : i ∈ s), f i))
  (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) sorry)
Tactic: rw [← OrderDual.toDual_inj, toDual_min', toDual_iInf]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ Eq (α := αᵒᵈ) (⨆ (i : ι), (OrderDual.toDual : (a : α) → αᵒᵈ) (⨅ (_ : i ∈ s), f i))
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)
have simp : Eq (α := αᵒᵈ) (⨆ i ∈ s, (OrderDual.toDual : (a : α) → αᵒᵈ) (f i))
  (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) sorry)
Tactic: simp only [toDual_iInf]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ Eq (α := αᵒᵈ) (⨆ i ∈ s, (OrderDual.toDual : (a : α) → αᵒᵈ) (f i))
    (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) ⋯)
have rw : Eq (α := αᵒᵈ) (max' (image (fun (i : ι) ↦ (OrderDual.toDual : (a : α) → αᵒᵈ) (f i)) s) sorry)
  (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) sorry)
Tactic: rw [ciSup_eq_max'_image _ h]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 : α) → αᵒᵈ) (image f s)) ⋯)
have simp : Eq (α := αᵒᵈ) (max' (image (fun (i : ι) ↦ (OrderDual.toDual : (a : α) → αᵒᵈ) (f i)) s) sorry)
  (max' (image ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f) s) sorry)
Tactic: simp only [image_image]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ ⨅ i ∈ s, f i = (image f s).min' h'
have rw : Eq (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) (⨅ i ∈ s, f i) : αᵒᵈ)
  ((OrderDual.toDual : (a : α) → αᵒᵈ) ((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
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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') : αᵒᵈ)
⊢ ⨅ i ∈ s, f i = (image f s).min' h'
have rw₁ : Eq (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) (⨅ i ∈ s, f i) : αᵒᵈ)
  (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) sorry : αᵒᵈ)
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
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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)) ⋯ : αᵒᵈ)
⊢ ⨅ i ∈ s, f i = (image f s).min' h'
have rw₂ : Eq (α := αᵒᵈ) (⨆ (i : ι), (OrderDual.toDual : (a : α) → αᵒᵈ) (⨅ (_ : i ∈ s), f i))
  (max' (image (⇑OrderDual.toDual : (a : α) → αᵒᵈ) (image f s)) sorry)
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