awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s
f : (b : (↑t : Type u_1)) → α
hf : ∀ (b : (↑t : Type u_1)), (↑b : α) ≤ f b ∧ f b ∈ t ∧ f b ∉ s
this : Nonempty.{u_1 + 1} (↑t : Type u_1)
hft : range f ⊆ t
apply : range f ∩ s = ∅
apply₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range f)
⊢ False
have apply₂ : IsLUB (range f) a
Tactic: apply (h (hDL hft hD) (range_nonempty f) _ _ has).ne_empty
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a_1 : α
ha_1 : IsLUB t a_1
has : a_1 ∈ s
H : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s
f : (b : (↑t : Type u_1)) → α
hf : ∀ (b : (↑t : Type u_1)), (↑b : α) ≤ f b ∧ f b ∈ t ∧ f b ∉ s
this : Nonempty.{u_1 + 1} (↑t : Type u_1)
hft : range f ⊆ t
a : α
ha : a ∈ range f
b : α
hb : b ∈ range f
⊢ ∃ z ∈ range f, (fun (x1 x2 : α) ↦ x1 ≤ x2) a z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) b z
have obtain : ∀ (c : α) (hc : c ∈ t), a ≤ c → b ≤ c → ∃ z ∈ range f, (fun (x1 x2 : α) ↦ x1 ≤ x2) a z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) b z
Tactic: obtain ⟨c, hc, _, _⟩ := ht₁ _ (hft ha) _ (hft hb)
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a_1 : α
ha_1 : IsLUB t a_1
has : a_1 ∈ s
H : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s
f : (b : (↑t : Type u_1)) → α
hf : ∀ (b : (↑t : Type u_1)), (↑b : α) ≤ f b ∧ f b ∈ t ∧ f b ∉ s
this : Nonempty.{u_1 + 1} (↑t : Type u_1)
hft : range f ⊆ t
a : α
ha : a ∈ range f
b : α
hb : b ∈ range f
c : α
hc : c ∈ t
left : a ≤ c
right : b ≤ c
⊢ ∃ z ∈ range f, (fun (x1 x2 : α) ↦ x1 ≤ x2) a z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) b z
have this₁ : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) : α) ≤ f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) ∧
  f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) ∈ t ∧ f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) ∉ s
Tactic: have := hf ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ b ∈ s
have a₁ : IsLUB {a} b
Tactic: apply hs (singleton_subset_iff.2 ha) ⟨a, rfl⟩ (directedOn_singleton a)
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ IsLUB {a} b
have a₁ : IsLUB {a} a
Tactic: rw [← isLUB_congr_of_antisymmRel h]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
⊢ Membership.mem (γ := Set α) {a} b
have rw : ∀ (hda : d = {a}) (hdn : d.Nonempty),
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃b : α⦄ (hb : IsLUB d b), Membership.mem (γ := Set α) {a} b
Tactic: rw [hdn.subset_singleton_iff] at hda
Cleared hypotheses: hda, hdn, h, b, hb
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
d : Set α
hda : d = {a}
hdn : d.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
⊢ Membership.mem (γ := Set α) {a} b
have hdn₁ : Set.Nonempty (α := α) {a}
Tactic: subst hda
Cleared hypotheses: d, hda, hdn, h, hb
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
d : Set α
hda : d = {a}
hdn : d.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
hdn₁ : Set.Nonempty (α := α) {a}
⊢ Membership.mem (γ := Set α) {a} b
have a₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) {a}
Tactic: subst hda
Cleared hypotheses: d, hda, hdn, h, hb
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
d : Set α
hda : d = {a}
hdn : d.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
hdn₁ : Set.Nonempty (α := α) {a}
a₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) {a}
⊢ Membership.mem (γ := Set α) {a} b
have hb₁ : IsLUB {a} b
Tactic: subst hda
Cleared hypotheses: d, hda, hdn, h, hb
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
⊢ DirectedOn r s ↔ Directed (ι := { x : α // x ∈ s }) r (Subtype.val (p := fun (x : α) ↦ x ∈ s))
have simp : (∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z) ↔
  ∀ (a : α) (b : a ∈ s) (a_1 : α) (b : a_1 ∈ s), ∃ (a_2 : α), r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2
Tactic: simp only [DirectedOn, Directed, Subtype.exists, exists_and_left, exists_prop, Subtype.forall]
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
⊢ DirectedOn r (Set.range f) ↔ Directed r f
have simp_rw : DirectedOn r (Set.range f) ↔ ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)
Tactic: simp_rw [Directed, DirectedOn, Set.forall_mem_range, Set.exists_range_iff]
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
simp_rw : DirectedOn r (Set.range f) ↔ ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)
⊢ DirectedOn r (Set.range f) ↔ Directed r f
have simp_rw₁ : (∀ x ∈ Set.range f, ∀ y ∈ Set.range f, ∃ z ∈ Set.range f, r x z ∧ r y z) ↔
  ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)
Tactic: simp_rw [Directed, DirectedOn, Set.forall_mem_range, Set.exists_range_iff]
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
simp_rw : DirectedOn r (Set.range f) ↔ ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)
simp_rw₁ :
  (∀ x ∈ Set.range f, ∀ y ∈ Set.range f, ∃ z ∈ Set.range f, r x z ∧ r y z) ↔
    ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)
⊢ DirectedOn r (Set.range f) ↔ Directed r f
have simp_rw₂ : (∀ (i i_1 : ι), ∃ z ∈ Set.range f, r (f i) z ∧ r (f i_1) z) ↔ ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)
Tactic: simp_rw [Directed, DirectedOn, Set.forall_mem_range, Set.exists_range_iff]
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
⊢ DirectedOn (r on f) s ↔ DirectedOn r (f '' s)
have refine : ∀ (h : DirectedOn r (f '' s)) (x : β) (hx : x ∈ s) (y : β) (hy : y ∈ s), ∃ z ∈ s, (r on f) x z ∧ (r on f) y z
Tactic: refine ⟨DirectedOn.mono_comp (by simp), fun h x hx y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
h : DirectedOn r (f '' s)
x : β
hx : x ∈ s
y : β
hy : y ∈ s
⊢ ∃ z ∈ s, (r on f) x z ∧ (r on f) y z
have obtain : ∀ (z : β) (hz : z ∈ s) (hz' : r (f x) (f z) ∧ r (f y) (f z)), ∃ z ∈ s, (r on f) x z ∧ (r on f) y z
Tactic: obtain ⟨_, ⟨z, hz, rfl⟩, hz'⟩ := h (f x) (Set.mem_image_of_mem f hx) (f y)
    (Set.mem_image_of_mem f hy)
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
a b : β
⊢ ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
have inl : ∀ (ha : ¬∃ (i : ι), e i = a),
  ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
Tactic: rcases (em (∃ i, e i = a)).symm with (ha | ⟨i, rfl⟩)
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
a b : β
inl :
  ∀ (ha : ¬∃ (i : ι), e i = a),
    ∃ (z : β),
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧
        (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
⊢ ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
have inr : ∀ (i : ι),
  ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
Tactic: rcases (em (∃ i, e i = a)).symm with (ha | ⟨i, rfl⟩)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
a b : β
ha : ¬∃ (i : ι), e i = a
⊢ ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
have h : (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ b) ∧
  (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ b)
Tactic: use b
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
⊢ ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
have inr : ∀ (hb : ¬∃ (i : ι), e i = b),
  ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
Tactic: rcases (em (∃ i, e i = b)).symm with (hb | ⟨j, rfl⟩)
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
inr :
  ∀ (hb : ¬∃ (i : ι), e i = b),
    ∃ (z : β),
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
        (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
⊢ ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
have inr₁ : ∀ (j : ι),
  ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)
Tactic: rcases (em (∃ i, e i = b)).symm with (hb | ⟨j, rfl⟩)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ (i : ι), e i = b
⊢ ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
have h : (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ (e i)) ∧
  (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ (e i))
Tactic: use e i
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
i j : ι
⊢ ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)
have inr : ∀ (k : ι) (hi : f i ≤ f k) (hj : f j ≤ f k),
  ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)
Tactic: rcases hf i j with ⟨k, hi, hj⟩
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ ∃ (z : β),
    (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)
have h : (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ (e k)) ∧
  (fun (x1 x2 : α) ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ (e k))
Tactic: use e k
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
inst : LE α
s : Set α
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ↔ IsDirectedOrder.{u_1} (↑s : Type u_1)
have rw : Directed (ι := { x : α // x ∈ s }) (fun (x1 x2 : α) ↦ x1 ≤ x2) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ↔
  IsDirected.{u_1 + 1} (↑s : Type u_1) fun (x1 x2 : (↑s : Type u_1)) ↦ x1 ≤ x2
Tactic: rw [directedOn_iff_directed, IsDirectedOrder]
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert x s, r x z ∧ r y z
have inl : ∀ (w : α) (hws : w ∈ s) (hwr : r x w ∧ r y w), ∃ z ∈ insert x s, r x z ∧ r y z
Tactic: obtain ⟨w, hws, hwr⟩ := ha y hy
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r x z ∧ r y z
have inr : ∀ (w : α) (hws : w ∈ s) (hwr : r y w ∧ r x w), ∃ z ∈ insert y s, r x z ∧ r y z
Tactic: obtain ⟨w, hws, hwr⟩ := ha x hx
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert a s, r x z ∧ r y z
have inr : ∀ (w : α) (hws : w ∈ s) (hwr : r x w ∧ r y w), ∃ z ∈ insert a s, r x z ∧ r y z
Tactic: obtain ⟨w, hws, hwr⟩ := hd x hx y hy
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a b : α
hab : r a b
⊢ DirectedOn r {b, a}
have rw : DirectedOn r {a, b}
Tactic: rw [Set.pair_comm]
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n : α
⊢ f m ≤ g n
have obtain : ∀ (k : α) (hkm : m ≤ k) (hkn : n ≤ k), f m ≤ g n
Tactic: obtain ⟨k, hkm, hkn⟩ := exists_ge_ge m n
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsCodirectedOrder β
⊢ ∃ (a : β) (b : β), a < b
have rcases : ∀ (a b : β) (hne : a ≠ b), ∃ (a : β) (b : β), a < b
Tactic: rcases exists_pair_ne β with ⟨a, b, hne⟩
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsCodirectedOrder β
a b : β
hne : a ≠ b
⊢ ∃ (a : β) (b : β), a < b
have inl : ∀ (ha : IsBot a), ∃ (a : β) (b : β), a < b
Tactic: rcases isBot_or_exists_lt a with (ha | ⟨c, hc⟩)
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsCodirectedOrder β
a b : β
hne : a ≠ b
inl : ∀ (ha : IsBot a), ∃ (a : β) (b : β), a < b
⊢ ∃ (a : β) (b : β), a < b
have inr : ∀ (c : β) (hc : c < a), ∃ (a : β) (b : β), a < b
Tactic: rcases isBot_or_exists_lt a with (ha | ⟨c, hc⟩)
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
⊢ False
have obtain : ∀ (a c : β) (hac : c < a), False
Tactic: obtain ⟨a, c, hac⟩ := exists_lt_of_directed_le β
-- Lean 4 proof step from Mathlib.Order.Directed (hypothesis)
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
a c : β
hac : c < a
⊢ False
have this : a ≤ b
Tactic: have := hb.isTop a
-- Lean 4 proof step from Mathlib.Order.Directed (hypothesis)
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
a c : β
hac : c < a
this : a ≤ b
⊢ False
have hac₁ : c < b
Tactic: obtain rfl := (hb' <| this).antisymm this
Cleared hypotheses: a, hac, this
-- Lean 4 proof step from Mathlib.Order.Directed (hypothesis)
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
a c : β
hac : c < a
this : a ≤ b
hac₁ : c < b
⊢ False
have this₁ : b ≤ b
Tactic: obtain rfl := (hb' <| this).antisymm this
Cleared hypotheses: a, hac, this
-- Lean 4 proof step from Mathlib.Order.Directed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : Preorder α
f : α → β
inst_2 : IsDirectedOrder α
hf : Monotone f
hf' : Antitone f
a b : α
⊢ f a = f b
have this : ∀ (m n : α), f m ≤ f n
Tactic: have := hf.forall_le_of_antitone hf' le_rfl
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a = f b
have obtain : ∀ (c : α) (hc : c ∈ s) (hac : a ≤ c) (hbc : b ≤ c), f a = f b
Tactic: obtain ⟨c, hc, hac, hbc⟩ := hs _ ha _ hb
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
ha : a ∈ Set.pi (α := α) Set.univ d
b : (i : ι) → α i
hb : b ∈ Set.pi (α := α) Set.univ d
⊢ ∃ z ∈ Set.pi (α := α) Set.univ d,
    (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧
      (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) b z
have choose : ∀ (f : (i : ι) → α i) (hfd : ∀ (i : ι), f i ∈ d i) (haf : ∀ (i : ι), r i (a i) (f i))
  (hbf : ∀ (i : ι), r i (b i) (f i)),
  ∃ z ∈ Set.pi (α := α) Set.univ d,
    (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧
      (fun (x y : (i : ι) → α i) ↦ ∀ (i : ι), r i (x i) (y i)) b z
Tactic: choose f hfd haf hbf using fun i => hd i (a i) (ha i trivial) (b i) (hb i trivial)
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r₂ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun (x1 x2 : α) ↦ r x1 x2) d₁
h₂ : DirectedOn (fun (x1 x2 : β) ↦ r₂ x1 x2) d₂
x : α × β
hpd : x ∈ d₁ ×ˢ d₂
x_1 : α × β
hqd : x_1 ∈ d₁ ×ˢ d₂
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x z ∧ (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x_1 z
have obtain : ∀ (r₁ : α) (hdr₁ : r₁ ∈ d₁) (hpr₁ : r x.1 r₁) (hqr₁ : r x_1.1 r₁),
  ∃ z ∈ d₁ ×ˢ d₂, (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x z ∧ (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x_1 z
Tactic: obtain ⟨r₁, hdr₁, hpr₁, hqr₁⟩ := h₁ _ hpd.1 _ hqd.1
-- Lean 4 proof step from Mathlib.Order.Directed (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r₂ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun (x1 x2 : α) ↦ r x1 x2) d₁
h₂ : DirectedOn (fun (x1 x2 : β) ↦ r₂ x1 x2) d₂
x : α × β
hpd : x ∈ d₁ ×ˢ d₂
x_1 : α × β
hqd : x_1 ∈ d₁ ×ˢ d₂
r₁ : α
hdr₁ : r₁ ∈ d₁
hpr₁ : r x.1 r₁
hqr₁ : r x_1.1 r₁
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x z ∧ (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x_1 z
have obtain : ∀ (r₂_1 : β) (hdr₂ : r₂_1 ∈ d₂) (hpr₂ : r₂ x.2 r₂_1) (hqr₂ : r₂ x_1.2 r₂_1),
  ∃ z ∈ d₁ ×ˢ d₂, (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x z ∧ (fun (p q : α × β) ↦ r p.1 q.1 ∧ r₂ p.2 q.2) x_1 z
Tactic: obtain ⟨r₂, hdr₂, hpr₂, hqr₂⟩ := h₂ _ hpd.2 _ hqd.2
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_1
inst : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_6, u_2 + 1, u_2 + 1} (T₁ h) (F₁ i) (F₁ j)
inst_2 : DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₁ x1 x2 x3) : (a : F₁ x1) → F₁ x2)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_7, u_3 + 1, u_3 + 1} (T₂ h) (F₂ i) (F₂ j)
inst_4 : DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f₂ x1 x2 x3) : (a : F₂ x1) → F₂ x2)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_6 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_7 : IsDirectedOrder ι
x y z : (i : ι) × F i
h :
  ∃ (i : ι) (hx : x.fst (β := fun (i : ι) ↦ F i) ≤ i) (hy : y.fst (β := fun (i : ι) ↦ F i) ≤ i),
    Eq (α := F i)
      ((f (x.fst (β := fun (i : ι) ↦ F i)) i hx : (a : F x.fst) → F i) (x.snd (β := fun (i : ι) ↦ F i)) : F i)
      ((f (y.fst (β := fun (i : ι) ↦ F i)) i hy : (a : F y.fst) → F i) (y.snd (β := fun (i : ι) ↦ F i)) : F i)
h_1 :
  ∃ (i : ι) (hx : y.fst (β := fun (i : ι) ↦ F i) ≤ i) (hy : z.fst (β := fun (i : ι) ↦ F i) ≤ i),
    Eq (α := F i)
      ((f (y.fst (β := fun (i : ι) ↦ F i)) i hx : (a : F y.fst) → F i) (y.snd (β := fun (i : ι) ↦ F i)) : F i)
      ((f (z.fst (β := fun (i : ι) ↦ F i)) i hy : (a : F z.fst) → F i) (z.snd (β := fun (i : ι) ↦ F i)) : F i)
j : ι
hx : x.fst (β := fun (i : ι) ↦ F i) ≤ j
w : y.fst (β := fun (i : ι) ↦ F i) ≤ j
jeq :
  Eq (α := F j) ((f (x.fst (β := fun (i : ι) ↦ F i)) j hx : (a : F x.fst) → F j) (x.snd (β := fun (i : ι) ↦ F i)) : F j)
    ((f (y.fst (β := fun (i : ι) ↦ F i)) j w : (a : F y.fst) → F j) (y.snd (β := fun (i : ι) ↦ F i)) : F j)
k : ι
w_1 : y.fst (β := fun (i : ι) ↦ F i) ≤ k
hz : z.fst (β := fun (i : ι) ↦ F i) ≤ k
keq :
  Eq (α := F k)
    ((f (y.fst (β := fun (i : ι) ↦ F i)) k w_1 : (a : F y.fst) → F k) (y.snd (β := fun (i : ι) ↦ F i)) : F k)
    ((f (z.fst (β := fun (i : ι) ↦ F i)) k hz : (a : F z.fst) → F k) (z.snd (β := fun (i : ι) ↦ F i)) : F k)
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ Eq (α := F i) ((f (x.fst (β := fun (i : ι) ↦ F i)) i ⋯ : (a : F x.fst) → F i) (x.snd (β := fun (i : ι) ↦ F i)) : F i)
    ((f (z.fst (β := fun (i : ι) ↦ F i)) i ⋯ : (a : F z.fst) → F i) (z.snd (β := fun (i : ι) ↦ F i)) : F i)
have rw : Eq (α := F i)
  ((f j i hji : (a : F j) → F i)
      ((f (x.fst (β := fun (i : ι) ↦ F i)) j hx : (a : F x.fst) → F j) (x.snd (β := fun (i : ι) ↦ F i)) : F j) :
    F i)
  ((f (z.fst (β := fun (i : ι) ↦ F i)) i sorry : (a : F z.fst) → F i) (z.snd (β := fun (i : ι) ↦ F i)) : F i)
Tactic: rw [← map_map' _ hx hji, ← map_map' _ hz hki, jeq, ← keq, map_map', map_map']
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_1
inst : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike.{u_8, u_4 + 1, u_4 + 1} (T h) (F i) (F j)
inst_2 : DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : F x1) → F x2)
inst_3 : IsDirectedOrder ι
z : DirectLimit F (T := T) f
⊢ ∃ (i : ι) (x : F i), z = ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧
have mk : ∀ (a : (i : ι) × F i),
  ∃ (i : ι) (x : F i),
    Eq (α := DirectLimit F (T := T) f) (Quot.mk (⇑(setoid f) : (i : ι) × F i → (i : ι) × F i → Prop) a)
      ⟦Sigma.mk (β := fun (i : ι) ↦ F i) i x⟧
Tactic: rcases z