awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : ∃ (x : α), ∀ y ∈ range f, y ≤ x
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
b : β
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (c : γ) ↦ f (b, c)) y → y ≤ x
have obtain : ∀ (B : α) (hB : ∀ y ∈ range f, y ≤ B),
  ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (c : γ) ↦ f (b, c)) y → y ≤ x
Tactic: obtain ⟨B, hB⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
have h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
Tactic: have h₂ b : BddAbove (Set.range fun c ↦ f (b, c)) := by
    rw [bddAbove_def] at hf ⊢
    obtain ⟨B, hB⟩ := hf
    exact ⟨B, by grind⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
have inr : ∀ (c : α), ⨆ (p : β × γ), f p ≤ c ↔ ⨆ (b : β), ⨆ (c : γ), f (b, c) ≤ c
Tactic: refine eq_of_forall_ge_iff fun c ↦ ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
⊢ ⨆ (p : β × γ), f p ≤ c ↔ ⨆ (b : β), ⨆ (c : γ), f (b, c) ≤ c
have inr : (∀ (i : β × γ), f i ≤ c) ↔ ∀ (i : β), ⨆ (c : γ), f (i, c) ≤ c
Tactic: rw [ciSup_le_iff (bddAbove_iff_subset_Iic.mpr hf), ciSup_le_iff h₁]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
| ∀ (i : β), ⨆ (c : γ), f (i, c) ≤ c
have enter : ∀ (b : β), ⨆ (c : γ), f (b, c) ≤ c
Tactic: enter [b]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
b : β
| ⨆ (c : γ), f (b, c) ≤ c
have rw : ∀ (i : γ), f (b, i) ≤ c
Tactic: rw [ciSup_le_iff (h₂ b)]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
| ∀ (i : β), ⨆ (c : γ), f (i, c) ≤ c
have enter : ∀ (b : β) (i : γ), f (b, i) ≤ c
Tactic: enter [b]; rw [ciSup_le_iff (h₂ b)]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
⊢ (∀ (i : β × γ), f i ≤ c) ↔ ∀ (i : β), ⨆ (c : γ), f (i, c) ≤ c
have inr : (∀ (i : β × γ), f i ≤ c) ↔ ∀ (b : β) (i : γ), f (b, i) ≤ c
Tactic: conv_rhs => enter [b]; rw [ciSup_le_iff (h₂ b)]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
hf : BddBelow (range f)
⊢ Eq.{u_1 + 1} (α := Set α) (Iic (⨅ (i : ι), f i)) (⋂ (i : ι), Iic (f i))
have h : ∀ (x : α), Membership.mem (γ := Set α) (Iic (⨅ (i : ι), f i)) x ↔ Membership.mem (γ := Set α) (⋂ (i : ι), Iic (f i)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have inl : IsEmpty.{max 1 u_4} (Subtype p) → iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
Tactic: cases isEmpty_or_nonempty (Subtype p)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
inl : IsEmpty.{max 1 u_4} (Subtype p) → iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have inr : Nonempty.{max 1 u_4} (Subtype p) → iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
Tactic: cases isEmpty_or_nonempty (Subtype p)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : IsEmpty.{max 1 u_4} (Subtype p)
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have inl : Eq.{u_1 + 1} (α := α) (sSup ∅) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h))
Tactic: rw [iSup_of_empty', cbiSup_eq_of_forall_not fun i h ↦ isEmptyElim (⟨i, h⟩ : Subtype p)]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : IsEmpty.{max 1 u_4} (Subtype p)
inl : Eq.{u_1 + 1} (α := α) (sSup ∅) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h))
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have inl₁ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
Tactic: rw [iSup_of_empty', cbiSup_eq_of_forall_not fun i h ↦ isEmptyElim (⟨i, h⟩ : Subtype p)]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have this : Nonempty ι
Tactic: have : Nonempty ι := (nonempty_subtype.mp ‹_›).nonempty
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have inr : ∀ (x : Subtype p), f x ≤ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
Tactic: refine le_antisymm (ciSup_le ?_) ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
inr : ∀ (x : Subtype p), f x ≤ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have inr₁ : ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
Tactic: refine le_antisymm (ciSup_le ?_) ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
h : p i
⊢ f (Subtype.mk (p := p) i h) ≤ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have this₁ : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
Tactic: have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
⊢ f (Subtype.mk (p := p) i h) ≤ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have inr : LE.le.{u_1} (α := α) ((fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i)
  (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
⊢ LE.le.{u_1} (α := α) ((fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i)
    (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h))
have inr : BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ ⨆ (h : p i), f (Subtype.mk (p := p) i h))
Tactic: refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
⊢ BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ ⨆ (h : p i), f (Subtype.mk (p := p) i h))
have inr : BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅)
Tactic: simp_rw [ciSup_eq_ite]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
⊢ BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅)
have inr : (range fun (i : ι) ↦ if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅) ⊆ range.{u_1, max 1 u_4} f ∪ {sSup ∅}
Tactic: refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
have inr : ∀ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
Tactic: refine ciSup_le fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
⊢ ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
have inr : (if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅) ≤ iSup.{u_1, max 1 u_4} f
Tactic: simp_rw [ciSup_eq_ite]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
⊢ (if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅) ≤ iSup.{u_1, max 1 u_4} f
have pos : ∀ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
pos : ∀ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
⊢ (if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅) ≤ iSup.{u_1, max 1 u_4} f
have neg : ¬p i → sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have inr : ∀ (x : Subtype p), f x ≤ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
Tactic: classical
  refine le_antisymm (ciSup_le ?_) ?_
  · intro ⟨i, h⟩
    have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]
    rw [this]
    refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i
    simp_rw [ciSup_eq_ite]
    refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_
    grind
  · refine ciSup_le fun i ↦ ?_
    simp_rw [ciSup_eq_ite]
    split_ifs
    · exact le_ciSup hf ?_
    · exact hf'
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
inr : ∀ (x : Subtype p), f x ≤ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
have inr₁ : ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
Tactic: classical
  refine le_antisymm (ciSup_le ?_) ?_
  · intro ⟨i, h⟩
    have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]
    rw [this]
    refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i
    simp_rw [ciSup_eq_ite]
    refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_
    grind
  · refine ciSup_le fun i ↦ ?_
    simp_rw [ciSup_eq_ite]
    split_ifs
    · exact le_ciSup hf ?_
    · exact hf'
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
s : Set β
f : β → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_2)) ↦ f (↑i : β))
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_2)), f (↑i : β))
⊢ sSup (f '' s) = ⨆ a ∈ s, f a
have rw : sSup (f '' s) = ⨆ (i : (↑s : Type u_2)), f (↑i : β)
Tactic: rw [← ciSup_subtype_fun hf hf', iSup, Set.image_eq_range]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
s : Set β
f : β → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_2)) ↦ f (↑i : β))
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_2)), f (↑i : β))
rw : sSup (f '' s) = ⨆ (i : (↑s : Type u_2)), f (↑i : β)
⊢ sSup (f '' s) = ⨆ a ∈ s, f a
have rw₁ : sSup (f '' s) = sSup (range fun (i : (↑s : Type u_2)) ↦ f (↑i : β))
Tactic: rw [← ciSup_subtype_fun hf hf', iSup, Set.image_eq_range]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
s : Set β
f : β → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_2)) ↦ f (↑i : β))
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_2)), f (↑i : β))
rw : sSup (f '' s) = ⨆ (i : (↑s : Type u_2)), f (↑i : β)
rw₁ : sSup (f '' s) = sSup (range fun (i : (↑s : Type u_2)) ↦ f (↑i : β))
⊢ sSup (f '' s) = ⨆ a ∈ s, f a
have rw₂ : Eq.{u_1 + 1} (α := α) (sSup (range fun (x : (↑s : Type u_2)) ↦ f (↑x : β)))
  (sSup (range fun (i : (↑s : Type u_2)) ↦ f (↑i : β)))
Tactic: rw [← ciSup_subtype_fun hf hf', iSup, Set.image_eq_range]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ ⨆ i ∈ s, i = sSup s
have rw : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_1)), (↑i : α))
Tactic: rw [← csSup_image (Subtype.range_coe ▸ hs), Set.image_id']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_1)), (↑i : α))
have h₁ : ⨆ (i : (↑s : Type u_1)), (↑i : α) = sSup s
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ ⨆ (i : (↑s : Type u_1)), (↑i : α) = sSup s
have h₁ : sSup (range fun (i : (↑s : Type u_1)) ↦ (↑i : α)) = sSup s
Tactic: rw [← sSup_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
h₁ : sSup (range fun (i : (↑s : Type u_1)) ↦ (↑i : α)) = sSup s
⊢ ⨆ (i : (↑s : Type u_1)), (↑i : α) = sSup s
have h₂ : sSup s = sSup s
Tactic: rw [← sSup_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ i ∈ s, i = sInf s
have rw : LE.le.{u_1} (α := α) (⨅ (i : (↑s : Type u_1)), (↑i : α)) (sInf ∅)
Tactic: rw [← csInf_image (Subtype.range_coe ▸ hs), Set.image_id']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ LE.le.{u_1} (α := α) (⨅ (i : (↑s : Type u_1)), (↑i : α)) (sInf ∅)
have h₁ : ⨅ (i : (↑s : Type u_1)), (↑i : α) = sInf s
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ (i : (↑s : Type u_1)), (↑i : α) = sInf s
have h₁ : sInf (range fun (i : (↑s : Type u_1)) ↦ (↑i : α)) = sInf s
Tactic: rw [← sInf_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
h₁ : sInf (range fun (i : (↑s : Type u_1)) ↦ (↑i : α)) = sInf s
⊢ ⨅ (i : (↑s : Type u_1)), (↑i : α) = sInf s
have h₂ : sInf s = sInf s
Tactic: rw [← sInf_range, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))
have inl : ∀ (hf : BddAbove.{u_1} (α := α) (range fun (i : (↑∅ : Type u_5)) ↦ g (f (↑i : ι))))
  (hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑∅ : Type u_5)), g (f (↑i : ι)))),
  Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' ∅, g i) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
Cleared hypotheses: s, hf, hg'
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
inl :
  ∀ (hf : BddAbove.{u_1} (α := α) (range fun (i : (↑∅ : Type u_5)) ↦ g (f (↑i : ι))))
    (hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑∅ : Type u_5)), g (f (↑i : ι)))),
    Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' ∅, g i) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))
have inr : ∀ (hs : s.Nonempty), Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑∅ : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑∅ : Type u_5)), g (f (↑i : ι)))
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' ∅, g i) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
have inl : Eq.{u_1 + 1} (α := α) (⨆ (i : ι'), ⨆ (_ : Membership.mem (γ := Set ι') ∅ i), g i)
  (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
Tactic: rw [Set.image_empty, cbiSup_empty, cbiSup_empty]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑∅ : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑∅ : Type u_5)), g (f (↑i : ι)))
inl :
  Eq.{u_1 + 1} (α := α) (⨆ (i : ι'), ⨆ (_ : Membership.mem (γ := Set ι') ∅ i), g i)
    (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' ∅, g i) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
have inl₁ : Eq.{u_1 + 1} (α := α) (sSup ∅) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
Tactic: rw [Set.image_empty, cbiSup_empty, cbiSup_empty]