awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ Tendsto f (𝓝[≤] x) (𝓝 (f x))
have simp_rw : ∀ (s : Set Y),
  Membership.mem (γ := Set (Set Y)) {s : Set Y | ∃ (a : Y), s = Ioi a ∨ s = Iio a} s →
    f x ∈ s → ∃ (u : Set X), IsOpen[inst_1] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' s
Tactic: simp_rw [TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Ioi z
have inl : ∀ (a : X) (hax : a ∈ Iio x) (hza : z < f a), ∃ (u : Set X), IsOpen[inst_1] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Ioi z
Tactic: obtain ⟨_, ⟨a, hax, rfl⟩, hza⟩ := (lt_isLUB_iff <| hf isLUB_Iio).mp hxz
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Lattice α
inst_2 : Nonempty α
h : inst = orderBornology
s : Set α
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw : IsBounded s ↔ BddBelow s ∧ BddAbove s
Tactic: rw [h, orderBornology_isBounded]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Lattice α
inst_2 : Nonempty α
h : inst = orderBornology
s : Set α
rw : IsBounded s ↔ BddBelow s ∧ BddAbove s
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw₁ : BddBelow s ∧ BddAbove s ↔ BddBelow s ∧ BddAbove s
Tactic: rw [h, orderBornology_isBounded]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Lattice α
inst_2 : Nonempty α
⊢ IsOrderBornology α ↔ inst = orderBornology
have refine : ∀ (h : IsOrderBornology α), inst = orderBornology
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun s ↦ by rw [h, orderBornology_isBounded]⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Lattice α
inst_2 : Nonempty α
h : IsOrderBornology α
⊢ inst = orderBornology
have h_cobounded : ∀ (s : Set α), s ∈ cobounded α ↔ s ∈ cobounded α
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
s : Set αᵒᵈ
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw : IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ BddBelow s ∧ BddAbove s
Tactic: rw [← isBounded_preimage_toDual, ← bddBelow_preimage_toDual, ← bddAbove_preimage_toDual,
      isBounded_iff_bddBelow_bddAbove, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
s : Set αᵒᵈ
rw : IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ BddBelow s ∧ BddAbove s
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw₁ : IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ BddBelow s ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
Tactic: rw [← isBounded_preimage_toDual, ← bddBelow_preimage_toDual, ← bddAbove_preimage_toDual,
      isBounded_iff_bddBelow_bddAbove, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
s : Set αᵒᵈ
rw : IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ BddBelow s ∧ BddAbove s
rw₁ :
  IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
    BddBelow s ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw₂ : IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
  BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
Tactic: rw [← isBounded_preimage_toDual, ← bddBelow_preimage_toDual, ← bddAbove_preimage_toDual,
      isBounded_iff_bddBelow_bddAbove, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
s : Set αᵒᵈ
rw : IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ BddBelow s ∧ BddAbove s
rw₁ :
  IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
    BddBelow s ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
rw₂ :
  IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
    BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw₃ : BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
  BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
Tactic: rw [← isBounded_preimage_toDual, ← bddBelow_preimage_toDual, ← bddAbove_preimage_toDual,
      isBounded_iff_bddBelow_bddAbove, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
s : Set αᵒᵈ
rw : IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ BddBelow s ∧ BddAbove s
rw₁ :
  IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
    BddBelow s ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
rw₂ :
  IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
    BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
rw₃ :
  BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
    BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw₄ : BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔
  BddAbove (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ∧ BddBelow (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s)
Tactic: rw [← isBounded_preimage_toDual, ← bddBelow_preimage_toDual, ← bddAbove_preimage_toDual,
      isBounded_iff_bddBelow_bddAbove, and_comm]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
β : Type u_2
inst_3 : Preorder β
inst_4 : Bornology β
inst_5 : IsOrderBornology β
s : Set (α × β)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ BddBelow s ∧ BddAbove s
Tactic: rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm,
      isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
β : Type u_2
inst_3 : Preorder β
inst_4 : Bornology β
inst_5 : IsOrderBornology β
s : Set (α × β)
rw : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ BddBelow s ∧ BddAbove s
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw₁ : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove s
Tactic: rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm,
      isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
β : Type u_2
inst_3 : Preorder β
inst_4 : Bornology β
inst_5 : IsOrderBornology β
s : Set (α × β)
rw : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ BddBelow s ∧ BddAbove s
rw₁ : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove s
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw₂ : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
  (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove (fst '' s) ∧ BddAbove (snd '' s)
Tactic: rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm,
      isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
β : Type u_2
inst_3 : Preorder β
inst_4 : Bornology β
inst_5 : IsOrderBornology β
s : Set (α × β)
rw : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ BddBelow s ∧ BddAbove s
rw₁ : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove s
rw₂ :
  IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove (fst '' s) ∧ BddAbove (snd '' s)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw₃ : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
  (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
Tactic: rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm,
      isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
β : Type u_2
inst_3 : Preorder β
inst_4 : Bornology β
inst_5 : IsOrderBornology β
s : Set (α × β)
rw : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ BddBelow s ∧ BddAbove s
rw₁ : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove s
rw₂ :
  IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove (fst '' s) ∧ BddAbove (snd '' s)
rw₃ :
  IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw₄ : (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ IsBounded (snd '' s) ↔
  (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
Tactic: rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm,
      isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
s_1 t : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
β : Type u_2
inst_3 : Preorder β
inst_4 : Bornology β
inst_5 : IsOrderBornology β
s : Set (α × β)
rw : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ BddBelow s ∧ BddAbove s
rw₁ : IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔ (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove s
rw₂ :
  IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddBelow (snd '' s)) ∧ BddAbove (fst '' s) ∧ BddAbove (snd '' s)
rw₃ :
  IsBounded (fst '' s) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
rw₄ :
  (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have rw₅ : (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s) ↔
  (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
Tactic: rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm,
      isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α_1 : Type u_1
s_1 t : Set α_1
inst : Bornology α_1
inst_1 : Preorder α_1
inst_2 : IsOrderBornology α_1
ι : Type u_2
α : ι → Type u_3
inst_3 : (i : ι) → Preorder (α i)
inst_4 : (i : ι) → Bornology (α i)
inst_5 : ∀ (i : ι), IsOrderBornology.{u_3} (α i)
s : Set ((i : ι) → α i)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have simp_rw : (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔ BddBelow s ∧ BddAbove s
Tactic: simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and,
      isBounded_iff_bddBelow_bddAbove]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α_1 : Type u_1
s_1 t : Set α_1
inst : Bornology α_1
inst_1 : Preorder α_1
inst_2 : IsOrderBornology α_1
ι : Type u_2
α : ι → Type u_3
inst_3 : (i : ι) → Preorder (α i)
inst_4 : (i : ι) → Bornology (α i)
inst_5 : ∀ (i : ι), IsOrderBornology.{u_3} (α i)
s : Set ((i : ι) → α i)
simp_rw : (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔ BddBelow s ∧ BddAbove s
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have simp_rw₁ : (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔
  (∀ (a : ι), BddBelow (Function.eval (β := α) a '' s)) ∧ BddAbove s
Tactic: simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and,
      isBounded_iff_bddBelow_bddAbove]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α_1 : Type u_1
s_1 t : Set α_1
inst : Bornology α_1
inst_1 : Preorder α_1
inst_2 : IsOrderBornology α_1
ι : Type u_2
α : ι → Type u_3
inst_3 : (i : ι) → Preorder (α i)
inst_4 : (i : ι) → Bornology (α i)
inst_5 : ∀ (i : ι), IsOrderBornology.{u_3} (α i)
s : Set ((i : ι) → α i)
simp_rw : (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔ BddBelow s ∧ BddAbove s
simp_rw₁ :
  (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔
    (∀ (a : ι), BddBelow (Function.eval (β := α) a '' s)) ∧ BddAbove s
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have simp_rw₂ : (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔
  (∀ (a : ι), BddBelow (Function.eval (β := α) a '' s)) ∧ ∀ (a : ι), BddAbove (Function.eval (β := α) a '' s)
Tactic: simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and,
      isBounded_iff_bddBelow_bddAbove]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α_1 : Type u_1
s_1 t : Set α_1
inst : Bornology α_1
inst_1 : Preorder α_1
inst_2 : IsOrderBornology α_1
ι : Type u_2
α : ι → Type u_3
inst_3 : (i : ι) → Preorder (α i)
inst_4 : (i : ι) → Bornology (α i)
inst_5 : ∀ (i : ι), IsOrderBornology.{u_3} (α i)
s : Set ((i : ι) → α i)
simp_rw : (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔ BddBelow s ∧ BddAbove s
simp_rw₁ :
  (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔
    (∀ (a : ι), BddBelow (Function.eval (β := α) a '' s)) ∧ BddAbove s
simp_rw₂ :
  (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔
    (∀ (a : ι), BddBelow (Function.eval (β := α) a '' s)) ∧ ∀ (a : ι), BddAbove (Function.eval (β := α) a '' s)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
have simp_rw₃ : (∀ (i : ι), IsBounded (Function.eval (β := α) i '' s)) ↔
  ∀ (x : ι), BddBelow (Function.eval (β := α) x '' s) ∧ BddAbove (Function.eval (β := α) x '' s)
Tactic: simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and,
      isBounded_iff_bddBelow_bddAbove]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
s : Set α
⊢ s ∈ cobounded α → Membership.mem (γ := Filter α) Filter.atTop s
have rw : BddBelow sᶜ ∧ BddAbove sᶜ → ∃ (i : α), True ∧ Ioi i ⊆ s
Tactic: rw [← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove, compl_compl s,
    Filter.atTop_basis_Ioi.mem_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (hypothesis)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
s : Set α
left : BddBelow sᶜ
b : α
hb : b ∈ upperBounds sᶜ
⊢ ∃ (i : α), True ∧ Ioi i ⊆ s
have hb₁ : Ioi b ⊆ s
Tactic: rw [mem_upperBounds_iff_subset_Iic, ← compl_compl (Iic b), compl_subset_compl, compl_Iic] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
s : Set α
left : BddBelow sᶜ
b : α
hb : Ioi b ⊆ s
w : α
⊢ ∃ (i : α), True ∧ Ioi i ⊆ s
have h : True ∧ Ioi b ⊆ s
Tactic: use b
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
⊢ Membership.mem (γ := Filter α) (Filter.atBot ⊔ Filter.atTop) s → s ∈ cobounded α
have rw : ((∃ (i : α), True ∧ Iic i ⊆ s) ∧ ∃ (i : α), True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ
Tactic: rw [Filter.mem_sup, Filter.atTop_basis.mem_iff, Filter.atBot_basis.mem_iff,
    ← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove, compl_compl s]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
⊢ BddBelow sᶜ ∧ BddAbove sᶜ
have refine_1 : ∀ (x : α) (hx : x ∈ sᶜ), b ≤ x
Tactic: refine ⟨⟨b, fun x hx ↦ ?_⟩, ⟨a, fun x hx ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
refine_1 : ∀ (x : α) (hx : x ∈ sᶜ), b ≤ x
⊢ BddBelow sᶜ ∧ BddAbove sᶜ
have refine_2 : ∀ (x : α) (hx : x ∈ sᶜ), x ≤ a
Tactic: refine ⟨⟨b, fun x hx ↦ ?_⟩, ⟨a, fun x hx ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
⊢ b ≤ x
have refine_1 : ∀ (hx' : x < b), False
Tactic: by_contra! hx'
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
s : Set α
b : α
left : True
hb : Iic b ⊆ s
a : α
left_1 : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
⊢ x ≤ a
have refine_2 : ∀ (hx' : a < x), False
Tactic: by_contra! hx'
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
⊢ cobounded α = Filter.atTop
have refine : ∀ (s : Set α), Membership.mem (γ := Filter α) Filter.atTop s → s ∈ cobounded α
Tactic: refine atTop_le_cobounded.antisymm' fun s ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
s : Set α
⊢ Membership.mem (γ := Filter α) Filter.atTop s → s ∈ cobounded α
have rw : (∃ (i : α), True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ
Tactic: rw [Filter.atTop_basis.mem_iff,
    ← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove, compl_compl s]
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
s : Set α
⊢ (∃ (i : α), True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ
have refine : (∃ (i : α), True ∧ Ici i ⊆ s) → ∀ (b : α), True → ∀ (hb : Ici b ⊆ s) (x : α) (hx : x ∈ sᶜ), x ≤ b
Tactic: refine fun ⟨b, _, hb⟩ ↦ ⟨⟨⊥, fun x hx ↦ by simp⟩, ⟨b, fun x hx ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Bornology (goal)
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Nonempty α
inst_2 : LinearOrder α
inst_3 : IsOrderBornology α
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
s : Set α
h : ∃ (i : α), True ∧ Ici i ⊆ s
b : α
left : True
hb : Ici b ⊆ s
x : α
hx : x ∈ sᶜ
⊢ x ≤ b
have by_contra! : ∀ (hx' : b < x), False
Tactic: by_contra! hx'
-- Lean 4 proof step from Mathlib.Topology.Order.Category.AlexDisc (goal)
Goal:
X Y : AlexDisc
f g : X ⟶ Y
h :
  Eq (α :=
    Functor.obj
        (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
          (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
          C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
        X ⟶
      Functor.obj
        (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
          (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
          C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
        Y)
    (CategoryTheory.Functor.map
      (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
        C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
      f)
    (CategoryTheory.Functor.map
      (forget₂ AlexDisc (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦ C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1)))
        (CC := fun (X : AlexDisc.{u_1}) ↦ (↑X.toTopCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
        C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
      g)
⊢ f = g
have h₁ : ∀ (x : (↑X.toTopCat : Type u_1)),
  Eq (α := (↑Y.toTopCat : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1)) f :
          (a : (↑X.toTopCat : Type u_1)) → (↑Y.toTopCat : Type u_1))
        x :
      (↑Y.toTopCat : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AlexDisc.{u_1}) ↦
            C((↑x1.toTopCat : Type u_1), (↑x2.toTopCat : Type u_1))) (CC := fun (X : AlexDisc.{u_1}) ↦
            (↑X.toTopCat : Type u_1)) g :
          (a : (↑X.toTopCat : Type u_1)) → (↑Y.toTopCat : Type u_1))
        x :
      (↑Y.toTopCat : Type u_1))
Tactic: ext x