awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)) ⋯ : αᵒᵈ)
rw₂ rw₃ 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'
have rw₅ : Eq (α := αᵒᵈ) (⨆ i ∈ s, (OrderDual.toDual : (a : α) → αᵒᵈ) (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)) ⋯ : αᵒᵈ)
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)) ⋯)
⊢ ⨅ i ∈ s, f i = (image f s).min' h'
have rw₆ : Eq (α := αᵒᵈ) (max' (image (fun (i : ι) ↦ (OrderDual.toDual : (a : α) → αᵒᵈ) (f i)) s) sorry)
  (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)) ⋯ : αᵒᵈ)
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)) ⋯)
⊢ ⨅ i ∈ s, f i = (image f s).min' h'
have rw₇ : Eq (α := αᵒᵈ) (max' (image (fun (i : ι) ↦ (OrderDual.toDual : (a : α) → αᵒᵈ) (f i)) s) sorry)
  (max' (image ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ 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, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i ∈ image f s
have rw : (image f s).max' sorry ∈ image f s
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 ∅
⊢ ⨅ i ∈ s, f i ∈ image f s
have rw : (image f s).min' sorry ∈ image f s
Tactic: rw [ciInf_eq_min'_image _ h]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i ∈ f '' s
have lift : ∀ (s : Finset ι) (h : ∃ x ∈ (↑s : Set ι), sSup ∅ ≤ f x), ⨆ i ∈ (↑s : Set ι), f i ∈ f '' (↑s : Set ι)
Tactic: lift s to Finset ι using hs
Cleared hypotheses: s, hs, h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ (↑s : Set ι), sSup ∅ ≤ f x
⊢ ⨆ i ∈ (↑s : Set ι), f i ∈ f '' (↑s : Set ι)
have h₁ : ∃ x ∈ s, sSup ∅ ≤ f x
Tactic: simp only [Finset.mem_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ s, f i ∈ f '' s
have lift : ∀ (s : Finset ι) (h : ∃ x ∈ (↑s : Set ι), f x ≤ sInf ∅), ⨅ i ∈ (↑s : Set ι), f i ∈ f '' (↑s : Set ι)
Tactic: lift s to Finset ι using hs
Cleared hypotheses: s, hs, h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ (↑s : Set ι), f x ≤ sInf ∅
⊢ ⨅ i ∈ (↑s : Set ι), f i ∈ f '' (↑s : Set ι)
have h₁ : ∃ x ∈ s, f x ≤ sInf ∅
Tactic: simp only [Finset.mem_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 < a ↔ ∀ x ∈ s, f x < a
have mp : ⨆ i ∈ s, f i < a → ∀ x ∈ s, f x < a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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
⊢ ⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a
have mpr : (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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
have mp : BddAbove.{u_2} (α := α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i)
Tactic: refine h.trans_le' (le_csSup ?_ ?_)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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)
⊢ f x < a
have mp₁ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) (f x)
Tactic: refine h.trans_le' (le_csSup ?_ ?_)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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)
have mp : (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sSup ∅}
Tactic: refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 : α
⊢ Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) a_1 → a_1 ∈ f '' s ∪ {sSup ∅}
have mp : ∀ (x : ι) (h : (if x ∈ s then f x else sSup ∅) = a_1), a_1 = sSup ∅ ∨ ∃ x ∈ s, f x = a_1
Tactic: simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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)
have mp : (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sSup ∅}
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
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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)
have mp₁ : ∀ ⦃a : α⦄, Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i) a → a ∈ f '' s ∪ {sSup ∅}
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
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 ∅}
⊢ BddAbove.{u_2} (α := α) (range fun (i : ι) ↦ ⨆ (_ : i ∈ s), f i)
have mp₂ : ∀ ⦃a : α⦄ (x : ι) (h : (if x ∈ s then f x else sSup ∅) = a), a = sSup ∅ ∨ ∃ x ∈ s, f x = a
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
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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
have mp : ⨆ (_ : x ∈ s), f x = f x
Tactic: refine ⟨x, ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a
have this : ⨆ i ∈ s, f i ∈ f '' s
Tactic: have := hs.ciSup_mem_image _ h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x
have mp : a < ⨅ i ∈ s, f i → ∀ x ∈ s, a < f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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
⊢ a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x
have mpr : (∀ x ∈ s, a < f x) → a < ⨅ i ∈ s, f i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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
have mp : BddBelow.{u_2} (α := α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i)
Tactic: refine h.trans_le (csInf_le ?_ ?_)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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)
⊢ a < f x
have mp₁ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i) (f x)
Tactic: refine h.trans_le (csInf_le ?_ ?_)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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)
have mp : (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sInf ∅}
Tactic: refine (((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 : α
⊢ Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i) a_1 → a_1 ∈ f '' s ∪ {sInf ∅}
have mp : ∀ (x : ι) (h : (if x ∈ s then f x else sInf ∅) = a_1), a_1 = sInf ∅ ∨ ∃ x ∈ s, f x = a_1
Tactic: simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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)
have mp : (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i) ⊆ f '' s ∪ {sInf ∅}
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
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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)
have mp₁ : ∀ ⦃a : α⦄, Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i) a → a ∈ f '' s ∪ {sInf ∅}
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
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 ∅}
⊢ BddBelow.{u_2} (α := α) (range fun (i : ι) ↦ ⨅ (_ : i ∈ s), f i)
have mp₂ : ∀ ⦃a : α⦄ (x : ι) (h : (if x ∈ s then f x else sInf ∅) = a), a = sInf ∅ ∨ ∃ x ∈ s, f x = a
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
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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
have mp : ⨅ (_ : x ∈ s), f x = f x
Tactic: refine ⟨x, ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (hypothesis)
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
⊢ a < ⨅ i ∈ s, f i
have this : ⨅ i ∈ s, f i ∈ f '' s
Tactic: have := hs.ciInf_mem_image _ h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (hypothesis)
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
⊢ a < ⨅ i ∈ s, f i
have this₁ : ∃ x ∈ s, f x = ⨅ i ∈ s, f i
Tactic: simp only [mem_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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
⊢ a < ⨅ i ∈ s, f i
have mpr : ∀ (w : ι) (hmem : w ∈ s) (hx : f w = ⨅ i ∈ s, f i), a < ⨅ i ∈ s, f i
Tactic: obtain ⟨_, hmem, hx⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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 < ⨅ i ∈ s, f i
have mpr : a < f w
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
⊢ s.sup' hs id = sSup (↑s : Set α)
have rw : sSup (id '' (↑s : Set α)) = sSup (↑s : Set α)
Tactic: rw [sup'_eq_csSup_image s hs, Set.image_id]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
rw : sSup (id '' (↑s : Set α)) = sSup (↑s : Set α)
⊢ s.sup' hs id = sSup (↑s : Set α)
have rw₁ : sSup (↑s : Set α) = sSup (↑s : Set α)
Tactic: rw [sup'_eq_csSup_image s hs, Set.image_id]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : DecidableEq ι
f : ι → α
s t : Finset ι
⊢ Eq.{u_2 + 1} (α := α) (⨆ x ∈ s ∪ t, f x) (max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x))
have suffices : ∀ (st : Finset ι), BddAbove.{u_2} (α := α) (Set.range fun (x : ι) ↦ ⨆ (_ : x ∈ st), f x)
Tactic: suffices ∀ st : Finset ι, BddAbove <| .range fun x ↦ ⨆ (_ : x ∈ st), f x by
    simp [ciSup_or', ciSup_sup_eq, this]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
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)
have 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
Tactic: refine fun st ↦ ⟨st.sup f, fun a ⟨i, ha⟩ ↦ ha ▸ ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
h : 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
have pos : ∀ (h : i ∈ st), (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i ≤ st.sup f
Tactic: by_cases h : i ∈ st
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
h : Membership.mem (γ := Set α) (Set.range fun (x : ι) ↦ ⨆ (_ : x ∈ st), f x) a
i : ι
ha : (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i = a
pos : ∀ (h : i ∈ st), (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i ≤ st.sup f
⊢ (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i ≤ st.sup f
have neg : ∀ (h : i ∉ st), (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i ≤ st.sup f
Tactic: by_cases h : i ∈ st
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : IsEmpty ι
inst_2 : InfSet α
f : ι → WithTop α
⊢ Eq.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), f i) ⊤
have rw : Eq.{u_1 + 1} (α := WithTop α) (sInf (range fun (i : ι) ↦ f i)) ⊤
Tactic: rw [iInf, range_eq_empty, WithTop.sInf_empty]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : IsEmpty ι
inst_2 : InfSet α
f : ι → WithTop α
rw : Eq.{u_1 + 1} (α := WithTop α) (sInf (range fun (i : ι) ↦ f i)) ⊤
⊢ Eq.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), f i) ⊤
have rw₁ : Eq.{u_1 + 1} (α := WithTop α) (sInf ∅) ⊤
Tactic: rw [iInf, range_eq_empty, WithTop.sInf_empty]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : IsEmpty ι
inst_2 : InfSet α
f : ι → WithTop α
rw : Eq.{u_1 + 1} (α := WithTop α) (sInf (range fun (i : ι) ↦ f i)) ⊤
rw₁ : Eq.{u_1 + 1} (α := WithTop α) (sInf ∅) ⊤
⊢ Eq.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), f i) ⊤
have rw₂ : Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤
Tactic: rw [iInf, range_eq_empty, WithTop.sInf_empty]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : Nonempty ι
inst_2 : InfSet α
f : ι → α
hf : BddBelow (range f)
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨅ (i : ι), f i) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))
have rw : Eq.{u_1 + 1} (α := WithTop α) (↑(sInf (range fun (i : ι) ↦ f i)) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))
Tactic: rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : Nonempty ι
inst_2 : InfSet α
f : ι → α
hf : BddBelow (range f)
rw : Eq.{u_1 + 1} (α := WithTop α) (↑(sInf (range fun (i : ι) ↦ f i)) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨅ (i : ι), f i) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))
have rw₁ : Eq.{u_1 + 1} (α := WithTop α) (↑(sInf (range fun (i : ι) ↦ f i)) : WithTop α)
  (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
Tactic: rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : Nonempty ι
inst_2 : InfSet α
f : ι → α
hf : BddBelow (range f)
rw : Eq.{u_1 + 1} (α := WithTop α) (↑(sInf (range fun (i : ι) ↦ f i)) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))
rw₁ :
  Eq.{u_1 + 1} (α := WithTop α) (↑(sInf (range fun (i : ι) ↦ f i)) : WithTop α)
    (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨅ (i : ι), f i) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))
have rw₂ : Eq (α := WithTop α) (sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' range f))
  (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
Tactic: rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]