awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
u : ℕ → α
hu : StrictMono u
huyxf : ∀ (n : ℕ), u n ∈ Ioo y x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have huyxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f
Tactic: obtain rfl : f ∘ v = u := funext hv
Cleared hypotheses: u, hu, huyxf, hlim, huyx, hv
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
u : ℕ → α
hu : StrictMono u
huyxf : ∀ (n : ℕ), u n ∈ Ioo y x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huyxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have hlim₁ : Tendsto (f ∘ v) atTop (𝓝 x)
Tactic: obtain rfl : f ∘ v = u := funext hv
Cleared hypotheses: u, hu, huyxf, hlim, huyx, hv
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
u : ℕ → α
hu : StrictMono u
huyxf : ∀ (n : ℕ), u n ∈ Ioo y x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huyxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f
hlim₁ : Tendsto (f ∘ v) atTop (𝓝 x)
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have huyx₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x
Tactic: obtain rfl : f ∘ v = u := funext hv
Cleared hypotheses: u, hu, huyxf, hlim, huyx, hv
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
u : ℕ → α
hu : StrictMono u
huyxf : ∀ (n : ℕ), u n ∈ Ioo y x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huyxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f
hlim₁ : Tendsto (f ∘ v) atTop (𝓝 x)
huyx₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have hv₁ : ∀ (n : ℕ), f (v n) = (f ∘ v) n
Tactic: obtain rfl : f ∘ v = u := funext hv
Cleared hypotheses: u, hu, huyxf, hlim, huyx, hv
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have rcases : ∀ (u : ℕ → α) (hu : StrictMono u) (huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f) (hlim : Tendsto u atTop (𝓝 x)),
  ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
Tactic: rcases Dense.exists_seq_strictMono_tendsto hf x with ⟨u, hu, huxf, hlim⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have hux : ∀ (n : ℕ), u n ∈ Iio x
Tactic: have hux (n : ℕ) : u n ∈ Iio x := (huxf n).1
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have huf : ∀ (n : ℕ), u n ∈ range f
Tactic: have huf (n : ℕ) : u n ∈ range f := (huxf n).2
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
huf : ∀ (n : ℕ), u n ∈ range f
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have choose : ∀ (v : (n : ℕ) → β) (hv : ∀ (n : ℕ), f (v n) = u n),
  ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
Tactic: choose v hv using huf
Cleared hypotheses: huf
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have hu₁ : StrictMono (f ∘ v)
Tactic: obtain rfl : f ∘ v = u := funext hv
Cleared hypotheses: u, hu, huxf, hlim, hux, hv
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have huxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f
Tactic: obtain rfl : f ∘ v = u := funext hv
Cleared hypotheses: u, hu, huxf, hlim, hux, hv
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have hlim₁ : Tendsto (f ∘ v) atTop (𝓝 x)
Tactic: obtain rfl : f ∘ v = u := funext hv
Cleared hypotheses: u, hu, huxf, hlim, hux, hv
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f
hlim₁ : Tendsto (f ∘ v) atTop (𝓝 x)
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have hux₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x
Tactic: obtain rfl : f ∘ v = u := funext hv
Cleared hypotheses: u, hu, huxf, hlim, hux, hv
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f
hlim₁ : Tendsto (f ∘ v) atTop (𝓝 x)
hux₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have hv₁ : ∀ (n : ℕ), f (v n) = (f ∘ v) n
Tactic: obtain rfl : f ∘ v = u := funext hv
Cleared hypotheses: u, hu, huxf, hlim, hux, hv
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
x y : α
h : x < y
⊢ ∃ (u : ℕ → α) (v : ℕ → α),
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)
have rcases : ∀ (u : ℕ → α) (hu_anti : StrictAnti u) (hu_mem : ∀ (n : ℕ), u n ∈ Ioo x y) (hux : Tendsto u atTop (𝓝 x)),
  ∃ (u : ℕ → α) (v : ℕ → α),
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)
Tactic: rcases exists_seq_strictAnti_tendsto' h with ⟨u, hu_anti, hu_mem, hux⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
x y : α
h : x < y
u : ℕ → α
hu_anti : StrictAnti u
hu_mem : ∀ (n : ℕ), u n ∈ Ioo x y
hux : Tendsto u atTop (𝓝 x)
⊢ ∃ (u : ℕ → α) (v : ℕ → α),
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)
have rcases : ∀ (v : ℕ → α) (hv_mono : StrictMono v) (hv_mem : ∀ (n : ℕ), v n ∈ Ioo (u 0) y) (hvy : Tendsto v atTop (𝓝 y)),
  ∃ (u : ℕ → α) (v : ℕ → α),
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)
Tactic: rcases exists_seq_strictMono_tendsto' (hu_mem 0).2 with ⟨v, hv_mono, hv_mem, hvy⟩
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a : α
h : ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
⊢ ∀ᶠ (x : γ) in l, f x ≤ a
have rcases : ∀ (d : α) (hd : IsGLB (Ioi a) d), ∀ᶠ (x : γ) in l, f x ≤ a
Tactic: rcases exists_glb_Ioi a with ⟨d, hd⟩
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a : α
h : ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
d : α
hd : IsGLB (Ioi a) d
⊢ ∀ᶠ (x : γ) in l, f x ≤ a
have inl : ∀ (h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b) (hd : IsGLB (Ioi d) d), ∀ᶠ (x : γ) in l, f x ≤ d
Tactic: obtain rfl | H0 := glb_Ioi_eq_self_or_Ioi_eq_Ici _ hd
Cleared hypotheses: a, h, hd
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a : α
h : ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
d : α
hd : IsGLB (Ioi a) d
inl : ∀ (h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b) (hd : IsGLB (Ioi d) d), ∀ᶠ (x : γ) in l, f x ≤ d
⊢ ∀ᶠ (x : γ) in l, f x ≤ a
have inr : ∀ (H0 : Ioi a = Ici d), ∀ᶠ (x : γ) in l, f x ≤ a
Tactic: obtain rfl | H0 := glb_Ioi_eq_self_or_Ioi_eq_Ici _ hd
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
have inl : ∀ (h : IsTop d), ∀ᶠ (x : γ) in l, f x ≤ d
Tactic: obtain h | _ := isTop_or_exists_gt d
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
inl : ∀ (h : IsTop d), ∀ᶠ (x : γ) in l, f x ≤ d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
have inl₁ : (∃ (b : α), d < b) → ∀ᶠ (x : γ) in l, f x ≤ d
Tactic: obtain h | _ := isTop_or_exists_gt d
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
have inl : ∀ (u : ℕ → α) (hu_tt : Tendsto u atTop (𝓝 d)) (hu_gt : ∀ (n : ℕ), u n ∈ Ioi d), ∀ᶠ (x : γ) in l, f x ≤ d
Tactic: obtain ⟨u, -, -, hu_tt, hu_gt⟩ := hd.exists_seq_antitone_tendsto (by simpa)
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
have h₁ : ∀ (n : ℕ), ∀ᶠ (x : γ) in l, f x < u n
Tactic: replace h := fun n ↦ h (u n) (by grind)
Cleared hypotheses: h
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ (n : ℕ), ∀ᶠ (x : γ) in l, f x < u n
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
have h₁ : ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i
Tactic: rw [← eventually_countable_forall] at h
Cleared hypotheses: h
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h_1 : ∃ (b : α), d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
have h₁ : ∀ (x : γ) (hx : ∀ (i : ℕ), f x < u i), f x ≤ d
Tactic: filter_upwards [h] with x hx
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a : α
h : ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
d : α
hd : IsGLB (Ioi a) d
H0 : Ioi a = Ici d
⊢ ∀ᶠ (x : γ) in l, f x ≤ a
have h₁ : ∀ᶠ (x : γ) in l, f x < d
Tactic: specialize h d <| by simp [← Set.mem_Ioi, H0]
Cleared hypotheses: h
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a d : α
hd : IsGLB (Ioi a) d
H0 : Ioi a = Ici d
h : ∀ᶠ (x : γ) in l, f x < d
⊢ ∀ᶠ (x : γ) in l, f x ≤ a
have h₁ : ∀ (x : γ) (hx : f x < d), f x ≤ a
Tactic: filter_upwards [h] with x hx
-- 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 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a d : α
hd : IsGLB (Ioi a) d
H0 : Ioi a = Ici d
h : ∀ᶠ (x : γ) in l, f x < d
x : γ
hx : f x < d
⊢ f x ≤ a
have h₁ : ∀ (H0 : Iic a = Iio d) (h : ∀ᶠ (x : γ) in l, f x < d) (x : γ) (hx : f x < d), f x ≤ a
Tactic: rw [← Set.compl_Iic, ← Set.compl_Iio, compl_inj_iff] at H0
Cleared hypotheses: H0, h, x, hx
-- Lean 4 proof step from Mathlib.Topology.Order.IsLocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
inst_1 : LinearOrder X
inst_2 : ClosedIicTopology X
⊢ IsLocallyClosed (Set.Ioc a b)
have rw : IsLocallyClosed (Set.Iic b ∩ Set.Ioi a)
Tactic: rw [← Set.Iic_inter_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Order.IsLocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
inst_1 : LinearOrder X
inst_2 : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Ico a b)
have rw : IsLocallyClosed (Set.Iio b ∩ Set.Ici a)
Tactic: rw [← Set.Iio_inter_Ici]
-- Lean 4 proof step from Mathlib.Topology.Order.Lattice (hypothesis)
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s_1 : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : ∀ (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))), Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : ∀ i ∈ cons a s ha, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))
have hs₁ : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
Tactic: rw [forall_mem_cons] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Order.Lattice (goal)
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s_1 : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : ∀ (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))), Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))
have cons : Tendsto (f a ⊔ s.sup' hne f) l (𝓝 (g a ⊔ s.sup' hne g))
Tactic: simp only [sup'_cons, hne]
-- Lean 4 proof step from Mathlib.Topology.Order.Lattice (goal)
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
have singleton : ∀ (a : ι) (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) {a} i → Tendsto (f i) l (𝓝 (g i))),
  Tendsto (sup' {a} sorry f) l (𝓝 (sup' {a} sorry g))
Tactic: induction hne using Finset.Nonempty.cons_induction with
  | singleton => simpa using hs
  | cons a s ha hne ihs =>
    rw [forall_mem_cons] at hs
    simp only [sup'_cons, hne]
    exact hs.1.sup_nhds (ihs hs.2)
Cleared hypotheses: hne, hs
-- Lean 4 proof step from Mathlib.Topology.Order.Lattice (goal)
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : ContinuousSup L
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
singleton :
  ∀ (a : ι) (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) {a} i → Tendsto (f i) l (𝓝 (g i))),
    Tendsto (sup' {a} ⋯ f) l (𝓝 (sup' {a} ⋯ g))
⊢ Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
have cons : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (hne : s.Nonempty)
  (ihs : ∀ (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))), Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g)))
  (hs : ∀ i ∈ cons a s ha, Tendsto (f i) l (𝓝 (g i))), Tendsto ((cons a s ha).sup' sorry f) l (𝓝 ((cons a s ha).sup' sorry g))
Tactic: induction hne using Finset.Nonempty.cons_induction with
  | singleton => simpa using hs
  | cons a s ha hne ihs =>
    rw [forall_mem_cons] at hs
    simp only [sup'_cons, hne]
    exact hs.1.sup_nhds (ihs hs.2)
Cleared hypotheses: hne, hs
-- Lean 4 proof step from Mathlib.Topology.Order.Lattice (goal)
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : OrderBot L
inst_3 : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))
have inl : ∀ (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) l (𝓝 (g i))),
  Tendsto (Finset.sup ∅ f) l (𝓝 (Finset.sup ∅ g))
Tactic: rcases s.eq_empty_or_nonempty with rfl | hne
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.Order.Lattice (goal)
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : OrderBot L
inst_3 : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
inl :
  ∀ (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) l (𝓝 (g i))),
    Tendsto (Finset.sup ∅ f) l (𝓝 (Finset.sup ∅ g))
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))
have inr : ∀ (hne : s.Nonempty), Tendsto (s.sup f) l (𝓝 (s.sup g))
Tactic: rcases s.eq_empty_or_nonempty with rfl | hne
-- Lean 4 proof step from Mathlib.Topology.Order.Lattice (goal)
Goal:
L : Type u_1
inst : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst_1 : SemilatticeSup L
inst_2 : OrderBot L
inst_3 : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
hne : s.Nonempty
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))
have inr : Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
Tactic: simp only [← sup'_eq_sup hne]