awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂) ⋯
have h : ∀ (n : ℕ),
  Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) n : α × β)
    ((pair (a₁, b₁) (a₂, b₂) sorry : (a : ℕ) → α × β) n : α × β)
Tactic: ext n : 2
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n : ℕ
⊢ Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) n : α × β)
    ((pair (a₁, b₁) (a₂, b₂) ⋯ : (a : ℕ) → α × β) n : α × β)
have h : Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) 0 : α × β)
  ((pair (a₁, b₁) (a₂, b₂) sorry : (a : ℕ) → α × β) 0 : α × β)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n : ℕ
h :
  Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) 0 : α × β)
    ((pair (a₁, b₁) (a₂, b₂) ⋯ : (a : ℕ) → α × β) 0 : α × β)
⊢ Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) n : α × β)
    ((pair (a₁, b₁) (a₂, b₂) ⋯ : (a : ℕ) → α × β) n : α × β)
have h₁ : ∀ (n : ℕ),
  Eq (α := α × β) (((pair a₁ a₂ ha).zip (pair b₁ b₂ hb) : (a : ℕ) → α × β) (n + 1) : α × β)
    ((pair (a₁, b₁) (a₂, b₂) sorry : (a : ℕ) → α × β) (n + 1) : α × β)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), LE.le.{u_2} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) → x ≤ y
h' : ∀ (c : Chain β), (f : (a : β) → α) (ωSup₀ c) = ωSup (c.map f)
c : Chain β
i : ℕ
⊢ LE.le.{u_2} (α := α) ((f : (a : β) → α) ((c : (a : ℕ) → β) i : β) : α) ((f : (a : β) → α) (ωSup₀ c) : α)
have rw : (f : (a : β) → α) ((c : (a : ℕ) → β) i : β) ≤ ωSup (c.map f)
Tactic: rw [h']
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), LE.le.{u_2} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) → x ≤ y
h' : ∀ (c : Chain β), (f : (a : β) → α) (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), (c : (a : ℕ) → β) i ≤ x
⊢ LE.le.{u_2} (α := α) ((f : (a : β) → α) (ωSup₀ c) : α) ((f : (a : β) → α) x : α)
have rw : ωSup (c.map f) ≤ (f : (a : β) → α) x
Tactic: rw [h']
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), LE.le.{u_2} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α) → x ≤ y
h' : ∀ (c : Chain β), (f : (a : β) → α) (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), (c : (a : ℕ) → β) i ≤ x
⊢ ωSup (c.map f) ≤ (f : (a : β) → α) x
have a : ∀ (i : ℕ), LE.le (α := α) ((c.map f : (a : ℕ) → α) i : α) ((f : (a : β) → α) x : α)
Tactic: apply ωSup_le
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h : c₀ ≤ c₁
i : ℕ
⊢ (c₀ : (a : ℕ) → α) i ≤ ωSup c₁
have obtain : ∀ (w : ℕ) (h : LE.le (α := α) ((c₀ : (a : ℕ) → α) i : α) ((c₁ : (a : ℕ) → α) w : α)), (c₀ : (a : ℕ) → α) i ≤ ωSup c₁
Tactic: obtain ⟨_, h⟩ := h i
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x ↔ ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x
have mp : ωSup c ≤ x → ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
mp : ωSup c ≤ x → ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x
⊢ ωSup c ≤ x ↔ ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x
have mpr : (∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ x) → ωSup c ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ωSup c ≤ x
i : ℕ
⊢ (c : (a : ℕ) → α) i ≤ x
have trans : (c : (a : ℕ) → α) i ≤ ωSup c
Tactic: trans ωSup c
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
⊢ IsLUB (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) (ωSup c)
have left : Membership.mem (γ := Set α) (upperBounds (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α))) (ωSup c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
left : Membership.mem (γ := Set α) (upperBounds (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α))) (ωSup c)
⊢ IsLUB (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) (ωSup c)
have right : Membership.mem (γ := Set α) (lowerBounds (upperBounds (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)))) (ωSup c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
⊢ Membership.mem (γ := Set α) (upperBounds (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α))) (ωSup c)
have left : ∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ ωSup c
Tactic: simp only [upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
      Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
⊢ Membership.mem (γ := Set α) (lowerBounds (upperBounds (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)))) (ωSup c)
have right : ∀ ⦃a : α⦄, (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) → ωSup c ≤ a
Tactic: simp only [lowerBounds, upperBounds, Set.mem_range, forall_exists_index,
      forall_apply_eq_imp_iff, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) a
⊢ a = ωSup c
have rw : a ≤ ωSup c ∧ ωSup c ≤ a
Tactic: rw [le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) a
⊢ a ≤ ωSup c ∧ ωSup c ≤ a
have h₁ : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
Tactic: simp only [IsLUB, IsLeast, upperBounds, lowerBounds, Set.mem_range, forall_exists_index,
    forall_apply_eq_imp_iff, Set.mem_setOf_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c ∧ ωSup c ≤ a
have left : a ≤ ωSup c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
left : a ≤ ωSup c
⊢ a ≤ ωSup c ∧ ωSup c ≤ a
have right : ωSup c ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c
have left : ∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ ωSup c
Tactic: apply h.2
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), (c : (a : ℕ) → α) a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), (c : (a : ℕ) → α) a ≤ a_1) → a ≤ a_1
⊢ ωSup c ≤ a
have right : ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ a
Tactic: rw [ωSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ Membership.mem (γ := Set (Set α)) (Set.range fun (c : Chain α) ↦ Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) {a, b}
have h₁ : Eq (α := Set α) ((fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) (pair a b hab)) {a, b}
Tactic: use pair a b hab
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
⊢ ωScottContinuous f ↔
    ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
have refine : (∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })) →
  ωScottContinuous f
Tactic: refine ⟨fun hf ↦ ⟨hf.monotone, hf.map_ωSup⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
⊢ ωScottContinuous f
have _ : ∀ ⦃d : Set α⦄,
  Membership.mem (γ := Set (Set α)) (Set.range fun (c : Chain α) ↦ Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) d →
    d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)
Tactic: _
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
⊢ Membership.mem (γ := Set (Set α)) (Set.range fun (c : Chain α) ↦ Set.range (ι := ℕ) (⇑c : (a : ℕ) → α)) d →
    d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)
have this : ∀ (c : Chain α) (hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d),
  d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → IsLUB (f '' d) (f a)
Tactic: ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB (f '' d) (f a)
have h : f '' d = Set.range (ι := ℕ) (⇑(c.map { toFun := f, monotone' := sorry }) : (a : ℕ) → β)
Tactic: convert! isLUB_range_ωSup (c.map { toFun := f, monotone' := hf.1 })
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h_1 : d.Nonempty
h_2 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
h : f '' d = Set.range (ι := ℕ) (⇑(c.map { toFun := f, monotone' := ⋯ }) : (a : ℕ) → β)
⊢ IsLUB (f '' d) (f a)
have h₁ : f a = ωSup (c.map { toFun := f, monotone' := sorry })
Tactic: convert! isLUB_range_ωSup (c.map { toFun := f, monotone' := hf.1 })
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ f a = ωSup (c.map { toFun := f, monotone' := ⋯ })
have hda₁ : IsLUB ((fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c) a
Tactic: rw [← hc] at hda
Cleared hypotheses: hda
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB ((fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c) a
⊢ f a = ωSup (c.map { toFun := f, monotone' := ⋯ })
have h : f a = f (ωSup c)
Tactic: rw [← hf.2 c, ωSup_eq_of_isLUB hda]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf : α →o β })
d : Set α
c : Chain α
hc : (fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c = d
h_1 : d.Nonempty
h_2 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB ((fun (c : Chain α) ↦ (Set.range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) c) a
h : f a = f (ωSup c)
⊢ f a = ωSup (c.map { toFun := f, monotone' := ⋯ })
have h₁ : f (ωSup c) = f (ωSup c)
Tactic: rw [← hf.2 c, ωSup_eq_of_isLUB hda]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
f : α →o β
⊢ ωScottContinuous.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β) ↔
    ∀ (c : Chain α), (f : (a : α) → β) (ωSup c) = ωSup (c.map f)
have rw : (∃ (hf : Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)),
    ∀ (c : Chain α),
      (f : (a : α) → β) (ωSup c) = ωSup (c.map { toFun := (⇑f : (a : α) → β), monotone' := hf : α →o β })) ↔
  ∀ (c : Chain α), (f : (a : α) → β) (ωSup c) = ωSup (c.map f)
Tactic: rw [ωScottContinuous_iff_monotone_map_ωSup]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
ha : some a ∈ c
hb : some b ∈ c
⊢ a = b
have obtain : ∀ (i : ℕ) (ha : some a = (c : (a : ℕ) → Part α) i), a = b
Tactic: obtain ⟨i, ha⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : some a = (c : (a : ℕ) → Part α) i
⊢ a = b
have ha₁ : (c : (a : ℕ) → Part α) i = some a
Tactic: replace ha := ha.symm
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : (c : (a : ℕ) → Part α) i = some a
⊢ a = b
have obtain : ∀ (j : ℕ) (hb : some b = (c : (a : ℕ) → Part α) j), a = b
Tactic: obtain ⟨j, hb⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : (c : (a : ℕ) → Part α) i = some a
j : ℕ
hb : some b = (c : (a : ℕ) → Part α) j
⊢ a = b
have hb₁ : (c : (a : ℕ) → Part α) j = some b
Tactic: replace hb := hb.symm
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : (c : (a : ℕ) → Part α) i = some a
j : ℕ
hb : (c : (a : ℕ) → Part α) j = some b
⊢ a = b
have rw : ∀ (ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a) (j : ℕ)
  (hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b), a = b
Tactic: rw [eq_some_iff] at ha hb
Cleared hypotheses: ha, j, hb
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
⊢ a = b
have inl : ∀ (hij : i ≤ j), a = b
Tactic: rcases le_total i j with hij | hji
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
inl : ∀ (hij : i ≤ j), a = b
⊢ a = b
have inr : ∀ (hji : j ≤ i), a = b
Tactic: rcases le_total i j with hij | hji
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
hij : i ≤ j
⊢ a = b
have this : Membership.mem (γ := Part α) ((c.toOrderHom : (a : ℕ) → Part α) j : Part α) a
Tactic: have := c.monotone hij _ ha
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
hji : j ≤ i
⊢ a = b
have this : Membership.mem (γ := Part α) ((c.toOrderHom : (a : ℕ) → Part α) i : Part α) b
Tactic: have := c.monotone hji _ hb
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
j : ℕ
hb : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) j : Part α) b
hji : j ≤ i
this : Membership.mem (γ := Part α) ((c.toOrderHom : (a : ℕ) → Part α) i : Part α) b
⊢ a = b
have inr : b = a
Tactic: apply Eq.symm
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h :
  Membership.mem (γ := Part α)
    (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) a
⊢ some a ∈ c
have pos : ∀ (h_1 : ∃ (a : α), some a ∈ c) (h : a ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1)), some a ∈ c
Tactic: split_ifs at h with h_1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h :
  Membership.mem (γ := Part α)
    (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) a
pos : ∀ (h_1 : ∃ (a : α), some a ∈ c) (h : a ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1)), some a ∈ c
⊢ some a ∈ c
have neg : ∀ (h_1 : ¬∃ (a : α), some a ∈ c) (h : Membership.mem (γ := Part α) none a), some a ∈ c
Tactic: split_ifs at h with h_1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ (a : α), some a ∈ c
h : a ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1)
⊢ some a ∈ c
have h' : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c
Tactic: have h' := Classical.choose_spec h_1
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ (a : α), some a ∈ c
h : a ∈ some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1)
h' : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) ∈ c
⊢ some a ∈ c
have h₁ : some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h_1) = some a
Tactic: rw [← eq_some_iff] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) x
⊢ x ∈ Part.ωSup c
have rw : ∀ (hx : (c : (a : ℕ) → Part α) i = some x), Part.ωSup c = some x
Tactic: rw [← eq_some_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : (c : (a : ℕ) → Part α) i = some x
⊢ Part.ωSup c = some x
have rw : some x ∈ c
Tactic: rw [ωSup_eq_some]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : (c : (a : ℕ) → Part α) i = some x
⊢ some x ∈ c
have rw : Membership.mem (α := Part α) c ((c : (a : ℕ) → Part α) i : Part α)
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), (c : (a : ℕ) → Part α) i ≤ x
a : α
ha : a ∈ Part.ωSup c
⊢ a ∈ x
have ha₁ : some a ∈ c
Tactic: replace ha := mem_chain_of_mem_ωSup ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), (c : (a : ℕ) → Part α) i ≤ x
a : α
ha : some a ∈ c
⊢ a ∈ x
have obtain : ∀ (i : ℕ) (ha : some a = (c : (a : ℕ) → Part α) i), a ∈ x
Tactic: obtain ⟨i, ha⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), (c : (a : ℕ) → Part α) i ≤ x
a : α
i : ℕ
ha : some a = (c : (a : ℕ) → Part α) i
⊢ a ∈ x
have a₁ : Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
Tactic: apply hx i
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), (c : (a : ℕ) → Part α) i ≤ x
a : α
i : ℕ
ha : some a = (c : (a : ℕ) → Part α) i
⊢ Membership.mem (γ := Part α) ((c : (a : ℕ) → Part α) i : Part α) a
have a₁ : a ∈ some a
Tactic: rw [← ha]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
x : α
c : Chain (Part α)
⊢ Membership.mem (γ := Part α)
      (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x ↔
    some x ∈ c
have mp : Membership.mem (γ := Part α)
    (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x →
  some x ∈ c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
x : α
c : Chain (Part α)
mp :
  Membership.mem (γ := Part α)
      (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x →
    some x ∈ c
⊢ Membership.mem (γ := Part α)
      (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x ↔
    some x ∈ c
have mpr : some x ∈ c →
  Membership.mem (γ := Part α)
    (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
⊢ Membership.mem (γ := Part α)
    (if h : ∃ (a : α), some a ∈ c then some (Classical.choose (p := fun (x : α) ↦ some x ∈ c) h) else none) x
have h' : ∃ (a : α), some a ∈ c
Tactic: have h' : ∃ a : α, some a ∈ c := ⟨_, h⟩