awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
have this : Nonempty ι
Tactic: have : Nonempty ι := ⟨i⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
have bdd : BddAbove (range.{u_1, max 1 u_4} f)
Tactic: have bdd : BddAbove (range f) := not_not.mp fun h ↦ gt.ne (ciSup_of_not_bddAbove h)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
have inr : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)) (sSup ∅)
Tactic: rw [max_eq_right gt.le]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)) (sSup ∅)
have inr : ∀ (j : ι), LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)
Tactic: refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
inr : ∀ (j : ι), LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)) (sSup ∅)
have inr₁ : ∀ w < sSup ∅, ∃ (i : ι), w < ⨆ (h : p i), f (Subtype.mk (p := p) i h)
Tactic: refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
j : ι
⊢ LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)
have pos : ∀ (hj : p j), LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)
Tactic: by_cases hj : p j
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range.{u_1, max 1 u_4} f)
j : ι
pos : ∀ (hj : p j), LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)
⊢ LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)
have neg : ∀ (hj : ¬p j), LE.le.{u_1} (α := α) (⨆ (h : p j), f (Subtype.mk (p := p) j h)) (sSup ∅)
Tactic: by_cases hj : p j
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Nonempty ι
f : ι → α
n : α
⊢ ⨅ (i : ι), f i = n ↔ (∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i
have have : ∀ (this : OrderBot α), ⨅ (i : ι), f i = n ↔ (∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i
Tactic: have : OrderBot α := WellFoundedLT.toOrderBot α
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ⨅ (i : ι), f i = n ↔ (∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i
have mp : ⨅ (i : ι), f i = n → (∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Nonempty ι
f : ι → α
n : α
this : OrderBot α
mp : ⨅ (i : ι), f i = n → (∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i
⊢ ⨅ (i : ι), f i = n ↔ (∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i
have mpr : ((∃ (i : ι), f i = n) ∧ ∀ (i : ι), n ≤ f i) → ⨅ (i : ι), f i = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : IsEmpty ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) ⊥
have rw : Eq.{u_1 + 1} (α := α) (sSup ∅) ⊥
Tactic: rw [iSup_of_empty', csSup_empty]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : IsEmpty ι
f : ι → α
rw : Eq.{u_1 + 1} (α := α) (sSup ∅) ⊥
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) ⊥
have rw₁ : Eq.{u_1 + 1} (α := α) ⊥ ⊥
Tactic: rw [iSup_of_empty', csSup_empty]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : a < ⨆ (i : ι), f i
⊢ ∃ (i : ι), a < f i
have contrapose! : ∀ (h : ∀ (i : ι), f i ≤ a), ⨆ (i : ι), f i ≤ a
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
p : ι → Prop
f : Exists p → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
have refine : ∀ (i : ι) (hi : p i), f sorry ≤ ⨆ (ih : Exists p), f ih
Tactic: refine le_antisymm ciSup_exists_le <| ciSup_le' fun i ↦ ciSup_le' fun hi ↦ ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
have pos : ∀ (hp : p), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f sorry) (⨆ (h : q), f sorry))
Tactic: by_cases hp : p
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
pos : ∀ (hp : p), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
have neg : ∀ (hp : ¬p), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f sorry) (⨆ (h : q), f sorry))
Tactic: by_cases hp : p
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
have pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f sorry) (⨆ (h : q), f sorry))
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : p
pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
have neg : ∀ (hq : ¬q), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f sorry) (⨆ (h : q), f sorry))
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
have pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f sorry) (⨆ (h : q), f sorry))
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
hp : ¬p
pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯))
have neg : ∀ (hq : ¬q), Eq.{u_1 + 1} (α := α) (⨆ (h : p ∨ q), f h) (max (⨆ (h : p), f sorry) (⨆ (h : q), f sorry))
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = sSup (l '' s)
have rw : ⨆ (x : (↑s : Type u_1)), l (↑x : α) = sSup (l '' s)
Tactic: rw [gc.l_csSup hne hbdd, sSup_image']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
rw : ⨆ (x : (↑s : Type u_1)), l (↑x : α) = sSup (l '' s)
⊢ l (sSup s) = sSup (l '' s)
have rw₁ : Eq.{u_2 + 1} (α := β) (⨆ (x : (↑s : Type u_1)), l (↑x : α)) (⨆ (a : (↑s : Type u_1)), l (↑a : α))
Tactic: rw [gc.l_csSup hne hbdd, sSup_image']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
⊢ l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
have rw : l (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), l (f i)
Tactic: rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
rw : l (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), l (f i)
⊢ l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
have rw₁ : Eq.{u_2 + 1} (α := β) (⨆ (x : (↑(range f) : Type u_1)), l (↑x : α)) (⨆ (i : ι), l (f i))
Tactic: rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
rw : l (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), l (f i)
rw₁ : Eq.{u_2 + 1} (α := β) (⨆ (x : (↑(range f) : Type u_1)), l (↑x : α)) (⨆ (i : ι), l (f i))
⊢ l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
have rw₂ : Eq.{u_2 + 1} (α := β) (⨆ (i : ι), l (f i)) (⨆ (i : ι), l (f i))
Tactic: rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
⊢ l (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨆ (i : (↑s : Type u_3)), l (f (↑i : γ))
have this : Nonempty.{u_3 + 1} (↑s : Type u_3)
Tactic: haveI := hne.to_subtype
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ l (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨆ (i : (↑s : Type u_3)), l (f (↑i : γ))
have hf₁ : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
Tactic: rw [image_eq_range] at hf
Cleared hypotheses: hf, hne, this
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
have inl : IsEmpty ι → Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
inl :
  IsEmpty ι → Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
have inr : Nonempty ι → Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h : Nonempty ι
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
have pos : ∀ (hf : BddAbove (range f)),
  Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
Tactic: by_cases hf : BddAbove (range f)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h : Nonempty ι
pos :
  ∀ (hf : BddAbove (range f)),
    Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
have neg : ∀ (hf : ¬BddAbove (range f)),
  Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
Tactic: by_cases hf : BddAbove (range f)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrderBot β
e : α ≃o β
f : ι → α
h : Nonempty ι
hf : ¬BddAbove (range f)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)
have hfe : ¬BddAbove.{u_2} (α := β) (range fun (i : ι) ↦ (e : (a : α) → β) (f i))
Tactic: have hfe : ¬ BddAbove (range fun i ↦ e (f i)) := by
      simpa [Set.Nonempty, BddAbove, upperBounds, e.surjective.forall] using hf
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ Eq.{u_1 + 1} (α := WithTop α) (⨆ (x : ι), (↑(f x) : WithTop α)) ⊤ ↔ ¬BddAbove (range f)
have rw : (∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)) ↔ ∀ (x : α), ∃ y ∈ range f, x < y
Tactic: rw [iSup_eq_top, not_bddAbove_iff]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ (∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)) ↔ ∀ (x : α), ∃ y ∈ range f, x < y
have refine_1 : ∀ (hf : ∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)) (r : α), ∃ y ∈ range f, r < y
Tactic: refine ⟨fun hf r => ?_, fun hf a ha => ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
refine_1 : ∀ (hf : ∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)) (r : α), ∃ y ∈ range f, r < y
⊢ (∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)) ↔ ∀ (x : α), ∃ y ∈ range f, x < y
have refine_2 : ∀ (hf : ∀ (x : α), ∃ y ∈ range f, x < y) (a : WithTop α) (ha : a < ⊤), ∃ (i : ι), a < (↑(f i) : WithTop α)
Tactic: refine ⟨fun hf r => ?_, fun hf a ha => ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ (i : ι), b < (↑(f i) : WithTop α)
r : α
⊢ ∃ y ∈ range f, r < y
have refine_1 : ∀ (i : ι) (hi : (↑r : WithTop α) < (↑(f i) : WithTop α)), ∃ y ∈ range f, r < y
Tactic: rcases hf r (WithTop.coe_lt_top r) with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
⊢ ∃ (i : ι), a < (↑(f i) : WithTop α)
have refine_2 : ∀ (i : ι) (hi : a.untop sorry < f i), ∃ (i : ι), a < (↑(f i) : WithTop α)
Tactic: rcases hf (a.untop ha.ne) with ⟨-, ⟨i, rfl⟩, hi⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ LT.lt.{u_1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
have rw : Ne.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
Tactic: rw [lt_top_iff_ne_top, Ne, iInf_coe_eq_top, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
rw : Ne.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
⊢ LT.lt.{u_1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
have rw₁ : ¬Eq.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
Tactic: rw [lt_top_iff_ne_top, Ne, iInf_coe_eq_top, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
rw : Ne.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
rw₁ : ¬Eq.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
⊢ LT.lt.{u_1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
have rw₂ : ¬IsEmpty ι ↔ Nonempty ι
Tactic: rw [lt_top_iff_ne_top, Ne, iInf_coe_eq_top, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
rw : Ne.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
rw₁ : ¬Eq.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
rw₂ : ¬IsEmpty ι ↔ Nonempty ι
⊢ LT.lt.{u_1} (α := WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α)) ⊤ ↔ Nonempty ι
have rw₃ : Nonempty ι ↔ Nonempty ι
Tactic: rw [lt_top_iff_ne_top, Ne, iInf_coe_eq_top, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
f : β → α
s : Set β
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (⨆ (i : (↑s : Type u_2)), f (↑i : β))
have rw : IsLUB (f '' s) (sSup (f '' s))
Tactic: rw [← sSup_image']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hdg : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
⊢ iSup f ≤ iSup g
have inl : IsEmpty ι → iSup f ≤ iSup g
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hdg : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
inl : IsEmpty ι → iSup f ≤ iSup g
⊢ iSup f ≤ iSup g
have inr : Nonempty ι → iSup f ≤ iSup g
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hdg : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h : IsEmpty ι
⊢ iSup f ≤ iSup g
have inl : sSup ∅ ≤ iSup g
Tactic: rw [iSup_of_empty', iSup_of_empty']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hdg : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h : IsEmpty ι
inl : sSup ∅ ≤ iSup g
⊢ iSup f ≤ iSup g
have inl₁ : LE.le.{u_1} (α := α) (sSup ∅) (sSup ∅)
Tactic: rw [iSup_of_empty', iSup_of_empty']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
⊢ ⨆ (x : ι), a = a
have rw : sSup (range fun (x : ι) ↦ a) = a
Tactic: rw [iSup, range_const, csSup_singleton]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
rw : sSup (range fun (x : ι) ↦ a) = a
⊢ ⨆ (x : ι), a = a
have rw₁ : sSup {a} = a
Tactic: rw [iSup, range_const, csSup_singleton]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
rw : sSup (range fun (x : ι) ↦ a) = a
rw₁ : sSup {a} = a
⊢ ⨆ (x : ι), a = a
have rw₂ : a = a
Tactic: rw [iSup, range_const, csSup_singleton]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (hypothesis)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Unique ι
s : ι → α
⊢ ⨆ (i : ι), s i = s default
have this : ∀ (i : ι), s i = s default
Tactic: have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (sSup ∅)
have rw : Eq.{u_1 + 1} (α := α) (sSup (range fun (h : p) ↦ f h)) (sSup ∅)
Tactic: rw [iSup]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ Eq.{u_1 + 1} (α := α) (sSup (range fun (h : p) ↦ f h)) (sSup ∅)
have e_a : Eq.{u_1 + 1} (α := Set α) (range fun (h : p) ↦ f h) ∅
Tactic: congr