awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
inr : c < a
⊢ c < a ∧ a < d
have inr₁ : a < d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ c < a
have inr : ¬c < a → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d
have inr : ¬a < d → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ btw a b c ∨ btw c b a
have inl : ∀ (hab : a ≤ b), btw a b c ∨ btw c b a
Tactic: rcases le_total a b with hab | hba
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inl : ∀ (hab : a ≤ b), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a
have inr : ∀ (hba : b ≤ a), btw a b c ∨ btw c b a
Tactic: rcases le_total a b with hab | hba
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
⊢ btw a b c ∨ btw c b a
have inl : ∀ (hbc : b ≤ c), btw a b c ∨ btw c b a
Tactic: rcases le_total b c with hbc | hcb
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
inl : ∀ (hbc : b ≤ c), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a
have inl₁ : ∀ (hcb : c ≤ b), btw a b c ∨ btw c b a
Tactic: rcases le_total b c with hbc | hcb
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
⊢ btw a b c ∨ btw c b a
have inr : ∀ (hbc : b ≤ c), btw a b c ∨ btw c b a
Tactic: rcases le_total b c with hbc | hcb
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
inr : ∀ (hbc : b ≤ c), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a
have inr₁ : ∀ (hcb : c ≤ b), btw a b c ∨ btw c b a
Tactic: rcases le_total b c with hbc | hcb
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ btw a b c ∨ btw c b a
have inl : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
Tactic: rcases le_total c a with hca | hac
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
inl : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a
have inl₁ : ∀ (hac : a ≤ c), btw a b c ∨ btw c b a
Tactic: rcases le_total c a with hca | hac
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
⊢ btw a b c ∨ btw c b a
have inl : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
Tactic: rcases le_total c a with hca | hac
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
inl : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a
have inl₁ : ∀ (hac : a ≤ c), btw a b c ∨ btw c b a
Tactic: rcases le_total c a with hca | hac
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
⊢ btw a b c ∨ btw c b a
have inr : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
Tactic: rcases le_total c a with hca | hac
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
inr : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a
have inr₁ : ∀ (hac : a ≤ c), btw a b c ∨ btw c b a
Tactic: rcases le_total c a with hca | hac
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
⊢ btw a b c ∨ btw c b a
have inr : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
Tactic: rcases le_total c a with hca | hac
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
inr : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a
have inr₁ : ∀ (hac : a ≤ c), btw a b c ∨ btw c b a
Tactic: rcases le_total c a with hca | hac
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : Preorder α
toOrderHom : α →o α
le_closure' : ∀ (x : α), x ≤ toOrderHom.toFun x
idempotent' : ∀ (x : α), toOrderHom.toFun (toOrderHom.toFun x) = toOrderHom.toFun x
IsClosed : (x : α) → Prop
isClosed_iff : ∀ {x : α}, IsClosed x ↔ toOrderHom.toFun x = x
IsClosed_1 : (x : α) → Prop
le_closure'_1 :
  ∀ (x : α),
    x ≤
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
        x
idempotent'_1 :
  ∀ (x : α),
    { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
        ({ toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
          x) =
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
        x
isClosed_iff_1 :
  ∀ {x : α},
    IsClosed_1 x ↔
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
          x =
        x
h :
  Eq.{u_1 + 1} (α := (a : α) → α)
    ((fun (c : ClosureOperator α) ↦ ((⇑c.toOrderHom : (a : α) → α) : (a : α) → α))
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
        isClosed_iff := @isClosed_iff })
    ((fun (c : ClosureOperator α) ↦ ((⇑c.toOrderHom : (a : α) → α) : (a : α) → α))
      {
        toOrderHom :=
          { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff }.toOrderHom,
        le_closure' := le_closure'_1, idempotent' := idempotent'_1, IsClosed := IsClosed_1,
        isClosed_iff := @isClosed_iff_1 })
⊢ { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
      isClosed_iff := @isClosed_iff : ClosureOperator α } =
    {
      toOrderHom :=
        { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff }.toOrderHom,
      le_closure' := le_closure'_1, idempotent' := idempotent'_1, IsClosed := IsClosed_1,
      isClosed_iff := @isClosed_iff_1 }
have e_IsClosed : ∀ (x : α), IsClosed x ↔ IsClosed_1 x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
⊢ Eq (α := Set α) {x : α | c.IsClosed x} (range (ι := α) (⇑c : (a : α) → α))
have h : ∀ (x : α),
  Membership.mem (γ := Set α) {x : α | c.IsClosed x} x ↔
    Membership.mem (γ := Set α) (range (ι := α) (⇑c : (a : α) → α)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
x y : α
hy : c.IsClosed y
⊢ (c : (a : α) → α) x ≤ y ↔ x ≤ y
have rw : LE.le (α := α) ((c : (a : α) → α) x : α) ((c : (a : α) → α) y : α) ↔ x ≤ (c : (a : α) → α) y
Tactic: rw [← hy.closure_eq, ← le_closure_iff]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
x y : α
hy : c.IsClosed y
rw : LE.le (α := α) ((c : (a : α) → α) x : α) ((c : (a : α) → α) y : α) ↔ x ≤ (c : (a : α) → α) y
⊢ (c : (a : α) → α) x ≤ y ↔ x ≤ y
have rw₁ : x ≤ (c : (a : α) → α) y ↔ x ≤ (c : (a : α) → α) y
Tactic: rw [← hy.closure_eq, ← le_closure_iff]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : PartialOrder α
c : ClosureOperator α
⊢ c = ofPred (⇑c : (a : α) → α) c.IsClosed ⋯ ⋯ ⋯
have a : ∀ (x : α), Eq (α := α) ((c : (a : α) → α) x : α) ((ofPred (⇑c : (a : α) → α) c.IsClosed sorry sorry sorry : (a : α) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ LE.le (α := α) ((c : (a : α) → α) (x ⊔ y) : α) ((c : (a : α) → α) ((c : (a : α) → α) x ⊔ y : α) : α)
have grw : LE.le (α := α) ((c : (a : α) → α) (x ⊔ y) : α) ((c : (a : α) → α) (x ⊔ y) : α)
Tactic: grw [← c.le_closure x]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ Eq (α := α) ((c : (a : α) → α) (x ⊔ (c : (a : α) → α) y) : α) ((c : (a : α) → α) (x ⊔ y) : α)
have rw : Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) y ⊔ x : α) : α) ((c : (a : α) → α) (x ⊔ y) : α)
Tactic: rw [sup_comm, closure_sup_closure_left, sup_comm (a := x)]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
c : ClosureOperator α
x y : α
rw : Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) y ⊔ x : α) : α) ((c : (a : α) → α) (x ⊔ y) : α)
⊢ Eq (α := α) ((c : (a : α) → α) (x ⊔ (c : (a : α) → α) y) : α) ((c : (a : α) → α) (x ⊔ y) : α)
have rw₁ : Eq (α := α) ((c : (a : α) → α) (y ⊔ x) : α) ((c : (a : α) → α) (x ⊔ y) : α)
Tactic: rw [sup_comm, closure_sup_closure_left, sup_comm (a := x)]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
c : ClosureOperator α
x y : α
rw : Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) y ⊔ x : α) : α) ((c : (a : α) → α) (x ⊔ y) : α)
rw₁ : Eq (α := α) ((c : (a : α) → α) (y ⊔ x) : α) ((c : (a : α) → α) (x ⊔ y) : α)
⊢ Eq (α := α) ((c : (a : α) → α) (x ⊔ (c : (a : α) → α) y) : α) ((c : (a : α) → α) (x ⊔ y) : α)
have rw₂ : Eq (α := α) ((c : (a : α) → α) (y ⊔ x) : α) ((c : (a : α) → α) (y ⊔ x) : α)
Tactic: rw [sup_comm, closure_sup_closure_left, sup_comm (a := x)]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) x ⊔ (c : (a : α) → α) y : α) : α) ((c : (a : α) → α) (x ⊔ y) : α)
have rw : Eq (α := α) ((c : (a : α) → α) (x ⊔ (c : (a : α) → α) y) : α) ((c : (a : α) → α) (x ⊔ y) : α)
Tactic: rw [closure_sup_closure_left, closure_sup_closure_right]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
c : ClosureOperator α
x y : α
rw : Eq (α := α) ((c : (a : α) → α) (x ⊔ (c : (a : α) → α) y) : α) ((c : (a : α) → α) (x ⊔ y) : α)
⊢ Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) x ⊔ (c : (a : α) → α) y : α) : α) ((c : (a : α) → α) (x ⊔ y) : α)
have rw₁ : Eq (α := α) ((c : (a : α) → α) (x ⊔ y) : α) ((c : (a : α) → α) (x ⊔ y) : α)
Tactic: rw [closure_sup_closure_left, closure_sup_closure_right]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
s : Set β
x : β
⊢ x ∈ l.toFun (u := SetLike.coe) s ↔ ∀ (S : α), s ⊆ (↑S : Set β) → x ∈ S
have simp_rw : l.toFun (u := SetLike.coe) {x} ≤ l.toFun (u := SetLike.coe) s ↔
  ∀ (S : α), l.toFun (u := SetLike.coe) s ≤ S → l.toFun (u := SetLike.coe) {x} ≤ S
Tactic: simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← l.le_iff_subset]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
x y : α
⊢ l.toFun (u := SetLike.coe)
      ((↑(l.toFun (u := SetLike.coe) (↑x : Set β)) : Set β) ∪ (↑(l.toFun (u := SetLike.coe) (↑y : Set β)) : Set β)) =
    l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))
have rw : l.toFun (u := SetLike.coe) ((↑(l.toFun (u := SetLike.coe) (↑x : Set β)) : Set β) ∪ (↑y : Set β)) =
  l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))
Tactic: rw [closure_union_closure_right, closure_union_closure_left]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
x y : α
rw :
  l.toFun (u := SetLike.coe) ((↑(l.toFun (u := SetLike.coe) (↑x : Set β)) : Set β) ∪ (↑y : Set β)) =
    l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))
⊢ l.toFun (u := SetLike.coe)
      ((↑(l.toFun (u := SetLike.coe) (↑x : Set β)) : Set β) ∪ (↑(l.toFun (u := SetLike.coe) (↑y : Set β)) : Set β)) =
    l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))
have rw₁ : l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β)) = l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))
Tactic: rw [closure_union_closure_right, closure_union_closure_left]
-- Lean 4 proof step from Mathlib.Order.Closure (goal)
Goal:
α : Type u_1
inst : PartialOrder α
c : ClosureOperator α
⊢ ⋯.closureOperator = c
have a : ∀ (x : α), Eq (α := α) ((sorry.closureOperator : (a : α) → α) x : α) ((c : (a : α) → α) x : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : LE α
⊢ IsCofinal.{u_1} (α := α) ∅ ↔ IsEmpty α
have refine : ∀ (h : IsCofinal.{u_1} (α := α) ∅) (a : α), False
Tactic: refine ⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty⟩
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a : α
⊢ ∃ y ∈ t, a ≤ y
have obtain : ∀ (b : α) (hb : b ∈ s) (hb' : a ≤ b), ∃ y ∈ t, a ≤ y
Tactic: obtain ⟨b, hb, hb'⟩ := hs a
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
a : β
⊢ ∃ y ∈ f '' s, a ≤ y
have obtain : ∀ (b : α) (hb : a ≤ f b), ∃ y ∈ f '' s, a ≤ y
Tactic: obtain ⟨_, ⟨b, rfl⟩, hb⟩ := hf' a
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
a : β
b : α
hb : a ≤ f b
⊢ ∃ y ∈ f '' s, a ≤ y
have obtain : ∀ (c : α) (hc : c ∈ s) (hc' : b ≤ c), ∃ y ∈ f '' s, a ≤ y
Tactic: obtain ⟨c, hc, hc'⟩ := hs b
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : IsCofinal s
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iio i) univ
have simp_rw : ∀ (x : α), ∃ i ∈ s, x ∈ Iio i
Tactic: simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : IsCofinal s
x : α
⊢ ∃ i ∈ s, x ∈ Iio i
have obtain : ∀ (y : α) (hy : x < y), ∃ i ∈ s, x ∈ Iio i
Tactic: obtain ⟨y, hy⟩ := exists_gt x
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : IsCofinal s
x y : α
hy : x < y
⊢ ∃ i ∈ s, x ∈ Iio i
have obtain : ∀ (z : α) (hz : z ∈ s) (hz' : y ≤ z), ∃ i ∈ s, x ∈ Iio i
Tactic: obtain ⟨z, hz, hz'⟩ := hs y
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iio i) univ
⊢ IsCofinal s
have rw : Subset.{u_1} (α := Set α) (⋃ i ∈ s, Iio i) (⋃ i ∈ s, Iic i)
Tactic: rw [isCofinal_iff_iUnion_Iic_eq_univ, ← univ_subset_iff, ← hs]
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iio i) univ
⊢ Subset.{u_1} (α := Set α) (⋃ i ∈ s, Iio i) (⋃ i ∈ s, Iic i)
have h : ∀ i ∈ s, Iio i ⊆ Iic i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
⊢ a ∈ s
have obtain : ∀ (b : α) (hb : b ∈ s) (hb' : a ≤ b), a ∈ s
Tactic: obtain ⟨b, hb, hb'⟩ := hs a
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
b : α
hb : b ∈ s
hb' : a ≤ b
⊢ a ∈ s
have rwa : ∀ (hb : a ∈ s) (hb' : a ≤ b), a ∈ s
Tactic: rwa [ha.eq_of_ge hb'] at hb
Cleared hypotheses: hb, hb'
-- Lean 4 proof step from Mathlib.Order.Cofinal (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s
have h₁ : ∃ (x : α), ∀ y ∈ s, y < x
Tactic: rw [not_isCofinal_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
h : ∃ (x : α), ∀ y ∈ s, y < x
⊢ BddAbove s
have obtain : ∀ (x : α) (h : ∀ y ∈ s, y < x), BddAbove s
Tactic: obtain ⟨x, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
h : ¬BddAbove s
⊢ IsCofinal s
have contrapose : ∀ (h : ¬IsCofinal s), BddAbove s
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : NoMaxOrder α
s : Set α
⊢ ¬IsCofinal s ↔ BddAbove s
have mpr : BddAbove s → ¬IsCofinal s
Tactic: use .of_not_isCofinal
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : NoMaxOrder α
s : Set α
⊢ BddAbove s → ¬IsCofinal s
have mpr : BddAbove s → ∃ (x : α), ∀ y ∈ s, y < x
Tactic: rw [not_isCofinal_iff]
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : NoMaxOrder α
s : Set α
x : α
h : x ∈ upperBounds s
⊢ ∃ (x : α), ∀ y ∈ s, y < x
have mpr : ∀ (z : α) (hz : x < z), ∃ (x : α), ∀ y ∈ s, y < x
Tactic: obtain ⟨z, hz⟩ := exists_gt x
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a : α
⊢ ∃ (y : α), Membership.mem (γ := Set α) {a : α | ∀ (b : α), r b a → b < a} y ∧ a ≤ y
have obtain : ∀ (b : α) (hb : b ∈ Ici a) (hb' : ∀ x ∈ Ici a, ¬r x b),
  ∃ (y : α), Membership.mem (γ := Set α) {a : α | ∀ (b : α), r b a → b < a} y ∧ a ≤ y
Tactic: obtain ⟨b, hb, hb'⟩ := h.wf.has_min (Set.Ici a) Set.nonempty_Ici
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
⊢ ∃ (y : α), Membership.mem (γ := Set α) {a : α | ∀ (b : α), r b a → b < a} y ∧ a ≤ y
have refine : ∀ (c : α) (hc : r c b), c < b
Tactic: refine ⟨b, fun c hc ↦ ?_, hb⟩
-- Lean 4 proof step from Mathlib.Order.Cofinal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
c : α
hc : r c b
⊢ c < b
have by_contra! : ∀ (hc' : b ≤ c), False
Tactic: by_contra! hc'
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
⊢ IsCompactElement k ↔
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
have mp : IsCompactElement k → ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
mp :
  IsCompactElement k →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
⊢ IsCompactElement k ↔
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
have mpr : (∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) →
  IsCompactElement k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hu : IsLUB s u
h_le : k ≤ u
⊢ ∃ x ∈ s, k ≤ x
have hu₁ : sSup s = u
Tactic: rw [isLUB_iff_sSup_eq] at hu
Cleared hypotheses: hu, h_le
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hu : sSup s = u
h_le : k ≤ u
⊢ ∃ x ∈ s, k ≤ x
have h_le₁ : k ≤ sSup s
Tactic: rw [← hu] at h_le
Cleared hypotheses: h_le
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have rw : (∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) ↔
  ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
Tactic: rw [isCompactElement_iff_le_of_directed_sSup_le]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
⊢ (∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) ↔
    ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have mp : (∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) →
  ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
mp :
  (∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) →
    ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ (∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) ↔
    ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have mpr : (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) →
  ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : (↑c : Set α) ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : (↑d : Set α) ⊆ s ∧ y = d.sup id
⊢ ∃ z ∈ S, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
have h : x ⊔ y ∈ S ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y (x ⊔ y)
Tactic: use x ⊔ y
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : (↑c : Set α) ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : (↑d : Set α) ⊆ s ∧ y = d.sup id
⊢ x ⊔ y ∈ S ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y (x ⊔ y)
have h : x ⊔ y ∈ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : (↑c : Set α) ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : (↑d : Set α) ⊆ s ∧ y = d.sup id
h : x ⊔ y ∈ S
⊢ x ⊔ y ∈ S ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y (x ⊔ y)
have h₁ : (fun (x1 x2 : α) ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y (x ⊔ y)
Tactic: constructor