awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Concept (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw : intent (r := r) (sInf (range fun (i : ι) ↦ f i)) = upperPolar r (⋂ (i : ι), (f i).extent (r := r))
simp_rw₁ :
  upperPolar r
      (⋂ (i : Concept α β r),
        ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.extent (r := r)) =
    upperPolar r (⋂ (i : ι), (f i).extent (r := r))
⊢ intent (r := r) (⨅ (i : ι), f i) = upperPolar r (⋂ (i : ι), (f i).extent (r := r))
have simp_rw₂ : upperPolar r
    (⨅ (i : Concept α β r),
      ⨅ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.extent (r := r)) =
  upperPolar r (⨅ (i : ι), (f i).extent (r := r))
Tactic: simp_rw [iInf, intent_sInf, ← Set.iInf_eq_iInter, iInf_range]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
have obtain : ∀ (x : α) (hx : x ∈ s), (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
Tactic: obtain ⟨x, hx⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
⊢ (↑(sInf s) : WithTop α) =
    if
        Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
          ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) then
      ⊤
    else
      (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
        WithTop α)
have pos : ∀
  (h :
    Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
      ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)),
  (↑(sInf s) : WithTop α) = ⊤
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
pos :
  ∀
    (h :
      Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
        ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)),
    (↑(sInf s) : WithTop α) = ⊤
⊢ (↑(sInf s) : WithTop α) =
    if
        Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
          ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) then
      ⊤
    else
      (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
        WithTop α)
have neg : ∀
  (h :
    ¬(Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
        ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))),
  (↑(sInf s) : WithTop α) =
    (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
      WithTop α)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h :
  Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
    ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
⊢ (↑(sInf s) : WithTop α) = ⊤
have pos : ∀ (h1 : Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤}), (↑(sInf s) : WithTop α) = ⊤
Tactic: rcases h with h1 | h2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h :
  Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
    ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
pos : ∀ (h1 : Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤}), (↑(sInf s) : WithTop α) = ⊤
⊢ (↑(sInf s) : WithTop α) = ⊤
have pos₁ : ∀ (h2 : ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)), (↑(sInf s) : WithTop α) = ⊤
Tactic: rcases h with h1 | h2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h :
  ¬(Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
      ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))
⊢ (↑(sInf s) : WithTop α) =
    (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
      WithTop α)
have neg : Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)
Tactic: rw [preimage_image_eq]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
have obtain : ∀ (x : α) (hx : x ∈ s), (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
Tactic: classical
  obtain ⟨x, hx⟩ := hs
  change _ = ite _ _ _
  split_ifs with h
  · rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
  · rw [preimage_image_eq]
    exact Option.some_injective _
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
obtain : ∀ (x : α) (hx : x ∈ s), (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
⊢ (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
have obtain₁ : ∀ (x : α) (hx : x ∈ s),
  (↑(sInf s) : WithTop α) =
    if
        Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
          ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) then
      ⊤
    else
      (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
        WithTop α)
Tactic: classical
  obtain ⟨x, hx⟩ := hs
  change _ = ite _ _ _
  split_ifs with h
  · rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
  · rw [preimage_image_eq]
    exact Option.some_injective _
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
obtain : ∀ (x : α) (hx : x ∈ s), (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
obtain₁ :
  ∀ (x : α) (hx : x ∈ s),
    (↑(sInf s) : WithTop α) =
      if
          Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
            ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) then
        ⊤
      else
        (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
          WithTop α)
⊢ (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
have pos : ∀ (x : α) (hx : x ∈ s)
  (h :
    Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
      ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)),
  (↑(sInf s) : WithTop α) = ⊤
Tactic: classical
  obtain ⟨x, hx⟩ := hs
  change _ = ite _ _ _
  split_ifs with h
  · rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
  · rw [preimage_image_eq]
    exact Option.some_injective _
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
obtain : ∀ (x : α) (hx : x ∈ s), (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
obtain₁ :
  ∀ (x : α) (hx : x ∈ s),
    (↑(sInf s) : WithTop α) =
      if
          Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
            ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) then
        ⊤
      else
        (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
          WithTop α)
pos :
  ∀ (x : α) (hx : x ∈ s)
    (h :
      Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
        ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)),
    (↑(sInf s) : WithTop α) = ⊤
⊢ (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
have neg : ∀ (x : α) (hx : x ∈ s)
  (h :
    ¬(Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
        ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))),
  (↑(sInf s) : WithTop α) =
    (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
      WithTop α)
Tactic: classical
  obtain ⟨x, hx⟩ := hs
  change _ = ite _ _ _
  split_ifs with h
  · rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
  · rw [preimage_image_eq]
    exact Option.some_injective _
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set α
hs : BddAbove s
⊢ (↑(sSup s) : WithTop α) =
    if Membership.mem (γ := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) ⊤ then ⊤
    else
      if
          BddAbove (α := α)
            (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) then
        (↑(sSup (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
          WithTop α)
      else ⊤
have h : Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)
Tactic: rw [if_neg, preimage_image_eq, if_pos hs]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set α
hs : BddAbove s
h : Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)
⊢ (↑(sSup s) : WithTop α) =
    if Membership.mem (γ := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) ⊤ then ⊤
    else
      if
          BddAbove (α := α)
            (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) then
        (↑(sSup (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
          WithTop α)
      else ⊤
have hnc : ⊤ ∉ (fun (a : α) ↦ (↑a : WithTop α)) '' s
Tactic: rw [if_neg, preimage_image_eq, if_pos hs]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set α
hs : BddAbove s
⊢ (↑(sSup s) : WithTop α) = sSup ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
have change : (↑(sSup s) : WithTop α) =
  if Membership.mem (γ := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) ⊤ then ⊤
  else
    if
        BddAbove (α := α)
          (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) then
      (↑(sSup (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
        WithTop α)
    else ⊤
Tactic: classical
  change _ = ite _ _ _
  rw [if_neg, preimage_image_eq, if_pos hs]
  · exact Option.some_injective _
  · rintro ⟨x, _, ⟨⟩⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set α
hs : BddAbove s
change :
  (↑(sSup s) : WithTop α) =
    if Membership.mem (γ := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) ⊤ then ⊤
    else
      if
          BddAbove (α := α)
            (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) then
        (↑(sSup (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
          WithTop α)
      else ⊤
⊢ (↑(sSup s) : WithTop α) = sSup ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
have h : Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)
Tactic: classical
  change _ = ite _ _ _
  rw [if_neg, preimage_image_eq, if_pos hs]
  · exact Option.some_injective _
  · rintro ⟨x, _, ⟨⟩⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set α
hs : BddAbove s
change :
  (↑(sSup s) : WithTop α) =
    if Membership.mem (γ := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) ⊤ then ⊤
    else
      if
          BddAbove (α := α)
            (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) then
        (↑(sSup (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
          WithTop α)
      else ⊤
h : Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)
⊢ (↑(sSup s) : WithTop α) = sSup ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
have hnc : ⊤ ∉ (fun (a : α) ↦ (↑a : WithTop α)) '' s
Tactic: classical
  change _ = ite _ _ _
  rw [if_neg, preimage_image_eq, if_pos hs]
  · exact Option.some_injective _
  · rintro ⟨x, _, ⟨⟩⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
⊢ Eq.{u_5 + 1} (α := WithBot α) (sInf ∅) ⊤
have rw : Eq.{u_5 + 1} (α := WithBot α) (↑(sInf (some ⁻¹' ∅)) : WithBot α) ⊤
Tactic: rw [WithBot.sInf_eq (by simp) (OrderBot.bddBelow _), Set.preimage_empty, _root_.sInf_empty,
    WithBot.coe_top]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
rw : Eq.{u_5 + 1} (α := WithBot α) (↑(sInf (some ⁻¹' ∅)) : WithBot α) ⊤
⊢ Eq.{u_5 + 1} (α := WithBot α) (sInf ∅) ⊤
have rw₁ : Eq.{u_5 + 1} (α := WithBot α) (↑(sInf ∅) : WithBot α) ⊤
Tactic: rw [WithBot.sInf_eq (by simp) (OrderBot.bddBelow _), Set.preimage_empty, _root_.sInf_empty,
    WithBot.coe_top]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
rw : Eq.{u_5 + 1} (α := WithBot α) (↑(sInf (some ⁻¹' ∅)) : WithBot α) ⊤
rw₁ : Eq.{u_5 + 1} (α := WithBot α) (↑(sInf ∅) : WithBot α) ⊤
⊢ Eq.{u_5 + 1} (α := WithBot α) (sInf ∅) ⊤
have rw₂ : Eq.{u_5 + 1} (α := WithBot α) (↑⊤ : WithBot α) ⊤
Tactic: rw [WithBot.sInf_eq (by simp) (OrderBot.bddBelow _), Set.preimage_empty, _root_.sInf_empty,
    WithBot.coe_top]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_5
inst : CompleteLattice α
rw : Eq.{u_5 + 1} (α := WithBot α) (↑(sInf (some ⁻¹' ∅)) : WithBot α) ⊤
rw₁ : Eq.{u_5 + 1} (α := WithBot α) (↑(sInf ∅) : WithBot α) ⊤
rw₂ : Eq.{u_5 + 1} (α := WithBot α) (↑⊤ : WithBot α) ⊤
⊢ Eq.{u_5 + 1} (α := WithBot α) (sInf ∅) ⊤
have rw₃ : Eq.{u_5 + 1} (α := WithBot α) ⊤ ⊤
Tactic: rw [WithBot.sInf_eq (by simp) (OrderBot.bddBelow _), Set.preimage_empty, _root_.sInf_empty,
    WithBot.coe_top]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
⊢ min a b = if a ≤ b then a else b
have pos : ∀ (hab : a = b), min a b = if a ≤ b then a else b
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
pos : ∀ (hab : a = b), min a b = if a ≤ b then a else b
⊢ min a b = if a ≤ b then a else b
have neg : ∀ (hab : ¬a = b), min a b = if a ≤ b then a else b
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ min a b = if a ≤ b then a else b
have neg : ∀ (h₁ : a ≤ b), min a b = if a ≤ b then a else b
Tactic: rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
neg : ∀ (h₁ : a ≤ b), min a b = if a ≤ b then a else b
⊢ min a b = if a ≤ b then a else b
have neg₁ : ∀ (h₂ : b ≤ a), min a b = if a ≤ b then a else b
Tactic: rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
⊢ max a b = if a ≤ b then b else a
have pos : ∀ (hab : a = b), max a b = if a ≤ b then b else a
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
pos : ∀ (hab : a = b), max a b = if a ≤ b then b else a
⊢ max a b = if a ≤ b then b else a
have neg : ∀ (hab : ¬a = b), max a b = if a ≤ b then b else a
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ max a b = if a ≤ b then b else a
have neg : ∀ (h₁ : a ≤ b), max a b = if a ≤ b then b else a
Tactic: rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
neg : ∀ (h₁ : a ≤ b), max a b = if a ≤ b then b else a
⊢ max a b = if a ≤ b then b else a
have neg₁ : ∀ (h₂ : b ≤ a), max a b = if a ≤ b then b else a
Tactic: rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → ConditionallyCompleteLattice (α i)
x : Set ((i : ι) → α i)
hn : x.Nonempty
hb : BddAbove x
x_1 : ι
⊢ IsLUB (eval (β := α) x_1 '' x) (sSup x x_1)
have rw : IsLUB (eval (β := α) x_1 '' x) (sSup (eval (β := α) x_1 '' x))
Tactic: rw [sSup_apply_eq_sSup_image]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → ConditionallyCompleteLattice (α i)
x : Set ((i : ι) → α i)
hn : x.Nonempty
hb : BddBelow x
x_1 : ι
⊢ IsGLB (eval (β := α) x_1 '' x) (sInf x x_1)
have rw : IsGLB (eval (β := α) x_1 '' x) (sInf (eval (β := α) x_1 '' x))
Tactic: rw [sInf_apply_eq_sInf_image]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
b : α
hs : s.Nonempty
hb : b < sSup s
⊢ ∃ a ∈ s, b < a
have contrapose! : ∀ (hb : ∀ (a : α) (_ : a ∈ s), a ≤ b), sSup s ≤ b
Tactic: contrapose! hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ sSup s = sSup univ
have rw : ¬BddAbove.{u_1} (α := α) univ
Tactic: rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ ¬BddAbove.{u_1} (α := α) univ
have contrapose : ∀ (hs : BddAbove.{u_1} (α := α) univ), BddAbove s
Tactic: contrapose hs
Cleared hypotheses: hs
-- 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
⊢ sSup s = sSup t
have inl : ∀ (hs : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∃ y ∈ t, x ≤ y)
  (ht : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ y ≤ x), sSup ∅ = sSup t
Tactic: rcases eq_empty_or_nonempty s with rfl | s_ne
Cleared hypotheses: s, hs, ht
-- 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
inl :
  ∀ (hs : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∃ y ∈ t, x ≤ y)
    (ht : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ y ≤ x), sSup ∅ = sSup t
⊢ sSup s = sSup t
have inr : ∀ (s_ne : s.Nonempty), sSup s = sSup t
Tactic: rcases eq_empty_or_nonempty s with rfl | s_ne
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (hypothesis)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ y ≤ x
⊢ sSup ∅ = sSup t
have this : t = ∅
Tactic: have : t = ∅ := eq_empty_of_forall_notMem (fun y yt ↦ by simpa using ht y yt)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ y ≤ x
this : t = ∅
⊢ sSup ∅ = sSup t
have inl : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
Tactic: rw [this]
-- 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
⊢ sSup s = sSup t
have inr : ∀ (hs : ∀ x ∈ s, ∃ (y : α), Membership.mem (γ := Set α) ∅ y ∧ x ≤ y)
  (ht : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ x ∈ s, y ≤ x), sSup s = sSup ∅
Tactic: rcases eq_empty_or_nonempty t with rfl | t_ne
Cleared hypotheses: t, hs, ht
-- 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
inr :
  ∀ (hs : ∀ x ∈ s, ∃ (y : α), Membership.mem (γ := Set α) ∅ y ∧ x ≤ y)
    (ht : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ x ∈ s, y ≤ x), sSup s = sSup ∅
⊢ sSup s = sSup t
have inr₁ : ∀ (t_ne : t.Nonempty), sSup s = sSup t
Tactic: rcases eq_empty_or_nonempty t with rfl | t_ne
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (hypothesis)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ (y : α), Membership.mem (γ := Set α) ∅ y ∧ x ≤ y
ht : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ x ∈ s, y ≤ x
⊢ sSup s = sSup ∅
have this : s = ∅
Tactic: have : s = ∅ := eq_empty_of_forall_notMem (fun x xs ↦ by simpa using hs x xs)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ (y : α), Membership.mem (γ := Set α) ∅ y ∧ x ≤ y
ht : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ x ∈ s, y ≤ x
this : s = ∅
⊢ sSup s = sSup ∅
have inr : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
Tactic: rw [this]
-- 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
⊢ sSup s = sSup t
have pos : ∀ (B : BddAbove s ∨ BddAbove t), sSup s = sSup t
Tactic: by_cases B : BddAbove s ∨ BddAbove t