awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
this : ∀ (h : StrictAntiOn f (Icc s t)), False
⊢ f x < f y
have hf_mono_st₁ : StrictMonoOn f (Icc s t)
Tactic: replace hf_mono_st : StrictMonoOn f (Icc s t) := hf_mono_st.resolve_right this
Cleared hypotheses: hf_mono_st
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this : ∀ (h : StrictAntiOn f (Icc s t)), False
hf_mono_st : StrictMonoOn f (Icc s t)
⊢ f x < f y
have hsx : s ≤ x
Tactic: have hsx : s ≤ x := min_le_right a x
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this : ∀ (h : StrictAntiOn f (Icc s t)), False
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
⊢ f x < f y
have hyt : y ≤ t
Tactic: have hyt : y ≤ t := le_max_right b y
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this : ∀ (h : StrictAntiOn f (Icc s t)), False
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
hyt : y ≤ t
⊢ f x < f y
have this₁ : Icc x y ⊆ Icc s t
Tactic: replace : Icc x y ⊆ Icc s t := Icc_subset_Icc hsx hyt
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
hyt : y ≤ t
this : Icc x y ⊆ Icc s t
⊢ f x < f y
have this₁ : StrictMonoOn f (Icc x y)
Tactic: replace : StrictMonoOn f (Icc x y) := StrictMonoOn.mono hf_mono_st this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
⊢ StrictMonoOn f (Icc a b)
have this : Fact (a ≤ b)
Tactic: have : Fact (a ≤ b) := ⟨hab⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
⊢ StrictMonoOn f (Icc a b)
have refine : StrictMono ((Icc a b).restrict (π := fun (a : α) ↦ δ) f)
Tactic: refine StrictMono.of_restrict ?_
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
g : (↑(Icc a b) : Type u) → δ := (Icc a b).restrict (π := fun (a : α) ↦ δ) f
⊢ StrictMono g
have hgab : g ⊥ ≤ g ⊤
Tactic: have hgab : g ⊥ ≤ g ⊤ := by aesop
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
⊢ StrictMono f ∨ StrictAnti f
have H : ∀ {c d : α} (hcd : c < d), StrictMono f ∨ StrictAnti f
Tactic: have H {c d : α} (hcd : c < d) : StrictMono f ∨ StrictAnti f :=
    (hf_c.continuousOn.strictMonoOn_of_injOn_Icc' hcd.le hf_i.injOn).imp
      (hf_c.strictMonoOn_of_inj_rigidity hf_i hcd)
      (hf_c.strictMonoOn_of_inj_rigidity (δ := δᵒᵈ) hf_i hcd)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
H : ∀ {c d : α} (hcd : c < d), StrictMono f ∨ StrictAnti f
⊢ StrictMono f ∨ StrictAnti f
have x : Subsingleton α ∨ Nontrivial α
Tactic: cases subsingleton_or_nontrivial α with
  | inl h => exact Or.inl <| Subsingleton.strictMono f
  | inr h =>
    obtain ⟨a, b, hab⟩ := exists_pair_lt α
    exact H hab
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)
have haveI : ∀ (this : Inhabited (↑(Ioo a b) : Type u)), StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)
Tactic: haveI : Inhabited (Ioo a b) := Classical.inhabited_of_nonempty (nonempty_Ioo_subtype hab)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this : Inhabited (↑(Ioo a b) : Type u)
g : (↑(Ioo a b) : Type u) → δ := (Ioo a b).restrict (π := fun (a : α) ↦ δ) f
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)
have this₁ : StrictMono g ∨ StrictAnti g
Tactic: have : StrictMono g ∨ StrictAnti g :=
    Continuous.strictMono_of_inj hf_c.restrict hf_i.injective
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
hs : s.Nonempty
⊢ ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s
have rcases : ∀ (a' : α) (ha' : a' ∈ s), ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s
Tactic: rcases hs with ⟨a', ha'⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun (x : α) ↦ x ∈ s) x
⊢ False
have inl : ∀ (ha : IsLUB s a') (h : ∀ᶠ (x : α) in 𝓝[≤] a', ¬(fun (x : α) ↦ x ∈ s) x), False
Tactic: rcases (ha.1 ha').eq_or_lt with (rfl | ha'a)
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun (x : α) ↦ x ∈ s) x
inl : ∀ (ha : IsLUB s a') (h : ∀ᶠ (x : α) in 𝓝[≤] a', ¬(fun (x : α) ↦ x ∈ s) x), False
⊢ False
have inr : ∀ (ha'a : a' < a), False
Tactic: rcases (ha.1 ha').eq_or_lt with (rfl | ha'a)
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun (x : α) ↦ x ∈ s) x
ha'a : a' < a
⊢ False
have inr : ∀ (b : α) (hba : b ∈ Iio a) (hb : Ioc b a ⊆ {x : α | (fun (x : α) ↦ ¬(fun (x : α) ↦ x ∈ s) x) x}), False
Tactic: rcases (mem_nhdsLE_iff_exists_Ioc_subset' ha'a).1 h with ⟨b, hba, hb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun (x : α) ↦ x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x : α | (fun (x : α) ↦ ¬(fun (x : α) ↦ x ∈ s) x) x}
⊢ False
have inr : ∀ (b' : α) (hb's : b' ∈ s) (hb' : b < b' ∧ b' ≤ a), False
Tactic: rcases ha.exists_between hba with ⟨b', hb's, hb'⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : a ∈ closure[inst] s
⊢ IsLUB s a
have hsf₁ : (𝓟 s ⊓ 𝓝 a).NeBot
Tactic: rw [mem_closure_iff_clusterPt, ClusterPt, inf_comm] at hsf
Cleared hypotheses: hsf
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
ha : IsLUB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
⊢ f x ≤ b
have ha₁ : IsLUB (s ∩ Ici x) a
Tactic: replace ha := ha.inter_Ici_of_mem hx
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
⊢ f x ≤ b
have this : (𝓝[s ∩ Ici x] a).NeBot
Tactic: haveI := ha.nhdsWithin_neBot ⟨x, hx, le_rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Preorder γ
inst_4 : TopologicalSpace γ
inst_5 : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : (𝓝[s ∩ Ici x] a).NeBot
⊢ f x ≤ b
have refine : ∀ᶠ (c : α) in 𝓝[s ∩ Ici x] a, f x ≤ f c
Tactic: refine ge_of_tendsto (hb.mono_left (nhdsWithin_mono a (inter_subset_left (t := Ici x)))) ?_
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
⊢ upperBounds (f '' S) = upperBounds (range f)
have refine : upperBounds (f '' S) ⊆ upperBounds (range f)
Tactic: refine subset_antisymm ?_ fun _ => upperBounds_mono (Set.image_subset_range f S) le_rfl
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
⊢ upperBounds (f '' S) ⊆ upperBounds (range f)
have refine : upperBounds (f '' S) ⊆ upperBounds (closure[inst] (f '' S))
Tactic: refine subset_trans ?_ fun _ => upperBounds_mono (hf.range_subset_closure_image_dense hS) le_rfl
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
x : α
hx : x ∈ upperBounds (f '' S)
i : α
hi : i ∈ closure[inst] (f '' S)
⊢ i ≤ x
have hi₁ : ∃ᶠ (x : α) in 𝓝 i, x ∈ f '' S
Tactic: rw [mem_closure_iff_frequently] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)
have rw : Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))
Tactic: rw [← sSup_range, ← sSup_range]
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
⊢ Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))
have inl : IsEmpty γ → Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))
Tactic: obtain (_ | _) := isEmpty_or_nonempty γ
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
inl :
  IsEmpty γ →
    Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))
⊢ Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))
have inr : Nonempty γ →
  Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))
Tactic: obtain (_ | _) := isEmpty_or_nonempty γ
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
h_1 : Nonempty γ
⊢ Eq.{u_3 + 1} (α := α) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ))) (sSup (range fun (i : γ) ↦ f i))
have inr : IsLUB (range f) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ)))
Tactic: refine ((isLUB_csSup (range_nonempty f) h).unique ?_).symm
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLattice α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove (range f)
h_1 : Nonempty γ
⊢ IsLUB (range f) (sSup (range fun (s : (↑S : Type u_2)) ↦ f (↑s : γ)))
have inr : BddAbove (f '' S)
Tactic: refine (isLUB_congr (hS.upperBounds_image hf)).mp (isLUB_ciSup_set ?_ hS.nonempty)
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
⊢ Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)
have pos : ∀ (h : BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))),
  Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)
Tactic: by_cases h : BddAbove (range (fun x : S ↦ f x))
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
pos :
  ∀ (h : BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))),
    Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)
⊢ Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)
have neg : ∀ (h : ¬BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))),
  Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)
Tactic: by_cases h : BddAbove (range (fun x : S ↦ f x))
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
⊢ Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)
have pos : range f ⊆ closure[inst] (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
Tactic: refine hS.ciSup hf <| h.closure.mono ?_
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : ¬BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
⊢ Eq.{u_3 + 1} (α := α) (⨆ (s : (↑S : Type u_2)), f (↑s : γ)) (⨆ (i : γ), f i)
have neg : ¬BddAbove (range f)
Tactic: suffices ¬ BddAbove (range f) by simp [ciSup_of_not_bddAbove, this, h]
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
γ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : ClosedIicTopology α
f : γ → α
inst_3 : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst_3, inst] f
h : ¬BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
⊢ ¬BddAbove (range f)
have neg : ∀ (h : BddAbove (range f)), BddAbove.{u_3} (α := α) (range fun (x : (↑S : Type u_2)) ↦ f (↑x : γ))
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
⊢ IsCompact (Icc a b)
have simp : ∀ (f : Ultrafilter α), Icc a b ∈ (↑f : Filter α) → ∃ x ∈ Icc a b, (↑f : Filter α) ≤ 𝓝 x
Tactic: simp only [isCompact_iff_ultrafilter_le_nhds, le_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
⊢ ∀ (f : Ultrafilter α), Icc a b ∈ (↑f : Filter α) → ∃ x ∈ Icc a b, (↑f : Filter α) ≤ 𝓝 x
have refine : a ≤ b → ∀ (f : Ultrafilter α) (hfab : Icc a b ∈ (↑f : Filter α)), ∃ x ∈ Icc a b, (↑f : Filter α) ≤ 𝓝 x
Tactic: refine (le_or_gt a b).elim (fun _ f hfab ↦ ?_) (by simp [·])
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
⊢ ∃ x ∈ Icc a b, (↑f : Filter α) ≤ 𝓝 x
have by_contra! : ∀ (hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
⊢ False
have hpt : ∀ x ∈ Icc a b, {x} ∉ f
Tactic: have hpt : ∀ x ∈ Icc a b, {x} ∉ f := fun x hx _ ↦ hf x hx (le_trans (by simpa) (pure_le_nhds x))
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
⊢ False
have hsb : b ∈ upperBounds s
Tactic: have hsb : b ∈ upperBounds s := fun x hx ↦ hx.1.2
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
⊢ False
have ha : a ∈ s
Tactic: have ha : a ∈ s := by simp [s, *]
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
⊢ False
have hsc : IsLUB s c
Tactic: have hsc : IsLUB s c := isLUB_csSup ⟨a, ha⟩ ⟨b, hsb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
⊢ False
have hc : c ∈ Icc a b
Tactic: have hc : c ∈ Icc a b := ⟨hsc.1 ha, hsc.2 hsb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
i : α
hic : i < c
⊢ Ioi i ∈ f
have have : ∀ (j : α) (hj : j ∈ s) (hij : i < j) (hjc : j ≤ c), Ioi i ∈ f
Tactic: have ⟨j, hj, hij, hjc⟩ := hsc.exists_between hic