awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
pos : ∀ (B : BddAbove s ∨ BddAbove t), sSup s = sSup t
⊢ sSup s = sSup t
have neg : ∀ (B : ¬(BddAbove s ∨ BddAbove t)), sSup s = sSup t
Tactic: by_cases B : BddAbove s ∨ BddAbove t
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
⊢ BddAbove s
have inl : ∀ (hB : BddAbove s), BddAbove s
Tactic: rcases B with hB | ⟨b, hb⟩
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
inl : ∀ (hB : BddAbove s), BddAbove s
⊢ BddAbove s
have inr : ∀ (b : α) (hb : b ∈ upperBounds t), BddAbove s
Tactic: rcases B with hB | ⟨b, hb⟩
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
b : α
hb : b ∈ upperBounds t
⊢ BddAbove s
have inr : ∀ (x : α) (hx : x ∈ s), x ≤ b
Tactic: refine ⟨b, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
b : α
hb : b ∈ upperBounds t
x : α
hx : x ∈ s
⊢ x ≤ b
have inr : ∀ (y : α) (hy : y ∈ t) (hxy : x ≤ y), x ≤ b
Tactic: rcases hs x hx with ⟨y, hy, hxy⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (hypothesis)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
⊢ sSup s = sSup t
have Bs : BddAbove s
Tactic: have Bs : BddAbove s := by
      rcases B with hB | ⟨b, hb⟩
      · exact hB
      · refine ⟨b, fun x hx ↦ ?_⟩
        rcases hs x hx with ⟨y, hy, hxy⟩
        exact hxy.trans (hb hy)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
⊢ BddAbove t
have inl : ∀ (b : α) (hb : b ∈ upperBounds s), BddAbove t
Tactic: rcases B with ⟨b, hb⟩ | hB
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
inl : ∀ (b : α) (hb : b ∈ upperBounds s), BddAbove t
⊢ BddAbove t
have inr : ∀ (hB : BddAbove t), BddAbove t
Tactic: rcases B with ⟨b, hb⟩ | hB
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
b : α
hb : b ∈ upperBounds s
⊢ BddAbove t
have inl : ∀ (y : α) (hy : y ∈ t), y ≤ b
Tactic: refine ⟨b, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
b : α
hb : b ∈ upperBounds s
y : α
hy : y ∈ t
⊢ y ≤ b
have inl : ∀ (x : α) (hx : x ∈ s) (hyx : y ≤ x), y ≤ b
Tactic: rcases ht y hy with ⟨x, hx, hyx⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (hypothesis)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
⊢ sSup s = sSup t
have Bt : BddAbove t
Tactic: have Bt : BddAbove t := by
      rcases B with ⟨b, hb⟩ | hB
      · refine ⟨b, fun y hy ↦ ?_⟩
        rcases ht y hy with ⟨x, hx, hyx⟩
        exact hyx.trans (hb hx)
      · exact hB
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup s = sSup t
have pos : sSup s ≤ sSup t
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
pos : sSup s ≤ sSup t
⊢ sSup s = sSup t
have pos₁ : sSup t ≤ sSup s
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup s ≤ sSup t
have apply : ∀ (x : α) (hx : x ∈ s), x ≤ sSup t
Tactic: apply csSup_le s_ne (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
x : α
hx : x ∈ s
⊢ x ≤ sSup t
have rcases : ∀ (y : α) (yt : y ∈ t) (hxy : x ≤ y), x ≤ sSup t
Tactic: rcases hs x hx with ⟨y, yt, hxy⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup t ≤ sSup s
have apply : ∀ (y : α) (hy : y ∈ t), y ≤ sSup s
Tactic: apply csSup_le t_ne (fun y hy ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
y : α
hy : y ∈ t
⊢ y ≤ sSup s
have rcases : ∀ (x : α) (xs : x ∈ s) (hyx : y ≤ x), y ≤ sSup s
Tactic: rcases ht y hy with ⟨x, xs, hyx⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)
have inl : sSup (∅ ∪ t) ≤ max (sSup ∅) (sSup t)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
inl : sSup (∅ ∪ t) ≤ max (sSup ∅) (sSup t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)
have inr : ∀ (hs : s.Nonempty), sSup (s ∪ t) ≤ max (sSup s) (sSup t)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)
have inr : sSup (s ∪ ∅) ≤ max (sSup s) (sSup ∅)
Tactic: rcases t.eq_empty_or_nonempty with (rfl | ht)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
inr : sSup (s ∪ ∅) ≤ max (sSup s) (sSup ∅)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)
have inr₁ : ∀ (ht : t.Nonempty), sSup (s ∪ t) ≤ max (sSup s) (sSup t)
Tactic: rcases t.eq_empty_or_nonempty with (rfl | ht)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)
have pos : BddAbove (s ∪ t) → sSup (s ∪ t) ≤ max (sSup s) (sSup t)
Tactic: by_cases BddAbove (s ∪ t)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
pos : BddAbove (s ∪ t) → sSup (s ∪ t) ≤ max (sSup s) (sSup t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)
have neg : ¬BddAbove (s ∪ t) → sSup (s ∪ t) ≤ max (sSup s) (sSup t)
Tactic: by_cases BddAbove (s ∪ t)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (sSup (⋃ (i : ι), Iic (f i))) (⨆ (i : ι), f i)
have hs : ∀ (x : α),
  Membership.mem (γ := Set α) (⋃ (i : ι), Iic (f i)) x →
    ∃ (y : α), Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) y ∧ x ≤ y
Tactic: apply csSup_eq_csSup_of_forall_exists_le
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
hs :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋃ (i : ι), Iic (f i)) x →
      ∃ (y : α), Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) y ∧ x ≤ y
⊢ Eq.{u_1 + 1} (α := α) (sSup (⋃ (i : ι), Iic (f i))) (⨆ (i : ι), f i)
have ht : ∀ (y : α),
  Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) y →
    ∃ (x : α), Membership.mem (γ := Set α) (⋃ (i : ι), Iic (f i)) x ∧ y ≤ x
Tactic: apply csSup_eq_csSup_of_forall_exists_le
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (sInf s)
have rw : IsLeast s (argminOn id s hs)
Tactic: rw [sInf_eq_argmin_on hs]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
n : α
⊢ sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a
have have : ∀ (this : OrderBot α), sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a
Tactic: have : OrderBot α := WellFoundedLT.toOrderBot α
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a
have mp : sInf s = n → n ∈ s ∧ ∀ a ∈ s, n ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
mp : sInf s = n → n ∈ s ∧ ∀ a ∈ s, n ≤ a
⊢ sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a
have mpr : (n ∈ s ∧ ∀ a ∈ s, n ≤ a) → sInf s = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
⊢ IsLUB s (sSup s)
have inl : ∀ (hs : BddAbove.{u_1} (α := α) ∅), IsLUB.{u_1} (α := α) ∅ (sSup ∅)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hne)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
inl : ∀ (hs : BddAbove.{u_1} (α := α) ∅), IsLUB.{u_1} (α := α) ∅ (sSup ∅)
⊢ IsLUB s (sSup s)
have inr : ∀ (hne : s.Nonempty), IsLUB s (sSup s)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hne)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : a < sSup s
⊢ ∃ b ∈ s, a < b
have contrapose! : ∀ (h : ∀ (b : α) (_ : b ∈ s), b ≤ a), sSup s ≤ a
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
⊢ sSup s ≤ sSup t
have inl : ∀ (h₂ : ∅ ⊆ t), sSup ∅ ≤ sSup t
Tactic: rcases eq_empty_or_nonempty s with rfl | h
Cleared hypotheses: s, h₂
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
inl : ∀ (h₂ : ∅ ⊆ t), sSup ∅ ≤ sSup t
⊢ sSup s ≤ sSup t
have inr : ∀ (h : s.Nonempty), sSup s ≤ sSup t
Tactic: rcases eq_empty_or_nonempty s with rfl | h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ sSup ∅ ≤ sSup t
have inl : ⊥ ≤ sSup t
Tactic: rw [csSup_empty]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s t : Set α
hs : BddAbove s
ht : BddAbove t
⊢ sSup (s ∪ t) = max (sSup s) (sSup t)
have inl : ∀ (hs : BddAbove.{u_1} (α := α) ∅), sSup (∅ ∪ t) = max (sSup ∅) (sSup t)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s t : Set α
hs : BddAbove s
ht : BddAbove t
inl : ∀ (hs : BddAbove.{u_1} (α := α) ∅), sSup (∅ ∪ t) = max (sSup ∅) (sSup t)
⊢ sSup (s ∪ t) = max (sSup s) (sSup t)
have inr : ∀ (hne : s.Nonempty), sSup (s ∪ t) = max (sSup s) (sSup t)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ IsLUB s (sSup s)
have left : sSup s ∈ upperBounds s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
left : sSup s ∈ upperBounds s
⊢ IsLUB s (sSup s)
have right : sSup s ∈ lowerBounds (upperBounds s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ (if ⊤ ∈ s then ⊤
    else
      if BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) then
        (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
      else ⊤) ∈
    upperBounds s
have pos : ∀ (h₁ : ⊤ ∈ s), ⊤ ∈ upperBounds s
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
pos : ∀ (h₁ : ⊤ ∈ s), ⊤ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤
    else
      if BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) then
        (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
      else ⊤) ∈
    upperBounds s
have pos₁ : ∀ (h₁ : ⊤ ∉ s) (h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)),
  (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ∈ upperBounds s
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
pos : ∀ (h₁ : ⊤ ∈ s), ⊤ ∈ upperBounds s
pos₁ :
  ∀ (h₁ : ⊤ ∉ s) (h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)),
    (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤
    else
      if BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) then
        (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
      else ⊤) ∈
    upperBounds s
have neg : ∀ (h₁ : ⊤ ∉ s) (h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)), ⊤ ∈ upperBounds s
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ Option.some a ≤ (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
have pos : a ≤ sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
Tactic: apply coe_le_coe.2
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ (if ⊤ ∈ s then ⊤
    else
      if BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) then
        (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
      else ⊤) ∈
    lowerBounds (upperBounds s)
have pos : ∀ (h₁ : ⊤ ∈ s), ⊤ ∈ lowerBounds (upperBounds s)
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
pos : ∀ (h₁ : ⊤ ∈ s), ⊤ ∈ lowerBounds (upperBounds s)
⊢ (if ⊤ ∈ s then ⊤
    else
      if BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) then
        (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
      else ⊤) ∈
    lowerBounds (upperBounds s)
have pos₁ : ∀ (h₁ : ⊤ ∉ s) (h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)),
  (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ∈ lowerBounds (upperBounds s)
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
pos : ∀ (h₁ : ⊤ ∈ s), ⊤ ∈ lowerBounds (upperBounds s)
pos₁ :
  ∀ (h₁ : ⊤ ∉ s) (h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)),
    (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ∈ lowerBounds (upperBounds s)
⊢ (if ⊤ ∈ s then ⊤
    else
      if BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) then
        (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
      else ⊤) ∈
    lowerBounds (upperBounds s)
have neg : ∀ (h₁ : ⊤ ∉ s) (h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)), ⊤ ∈ lowerBounds (upperBounds s)
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ≤ Option.some b
have pos : Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
Tactic: refine coe_le_coe.2 (csSup_le ?_ ?_)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
pos : Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
⊢ (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ≤ Option.some b
have pos₁ : ∀ (b_1 : β), Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) b_1 → b_1 ≤ b
Tactic: refine coe_le_coe.2 (csSup_le ?_ ?_)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have pos : ∀ (hb : none ∈ s), Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
Tactic: rcases hs with ⟨⟨⟩ | b, hb⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
pos : ∀ (hb : none ∈ s), Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have pos₁ : ∀ (b : β) (hb : Option.some b ∈ s), Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
Tactic: rcases hs with ⟨⟨⟩ | b, hb⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ⊤ ≤ Option.some b
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ False
have neg : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
Tactic: apply h₂
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have h : Membership.mem (γ := Set β) (upperBounds ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) b
Tactic: use b
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ IsLUB s (sSup s)
have left : sSup s ∈ upperBounds s
Tactic: classical
  constructor
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · contradiction
      apply coe_le_coe.2
      exact le_csSup h₂ ha
    · intro _ _
      exact le_top
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · rintro (⟨⟩ | a) ha
      · exact le_rfl
      · exact False.elim (not_top_le_coe a (ha h₁))
    · rintro (⟨⟩ | b) hb
      · exact le_top
      refine coe_le_coe.2 (csSup_le ?_ ?_)
      · rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩
      · intro a ha
        exact coe_le_coe.1 (hb ha)
    · rintro (⟨⟩ | b) hb
      · exact le_rfl
      · exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)