awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
rw : f (sInf (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
rw₃ : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
⊢ f (⨅ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₄ : Eq.{u_2 + 1} (α := β) (sSup (range fun (x : ι) ↦ f (g x))) (sSup (range fun (i : ι) ↦ f (g i)))
Tactic: rw [iInf, Antitone.map_csInf_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iSup,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
bdd : BddAbove (range g)
⊢ f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)
have rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
Tactic: rw [iSup, Antitone.map_csSup_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
bdd : BddAbove (range g)
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
⊢ f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)
have rw₁ : sInf (f '' range g) = ⨅ (i : ι), f (g i)
Tactic: rw [iSup, Antitone.map_csSup_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
bdd : BddAbove (range g)
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
rw₁ : sInf (f '' range g) = ⨅ (i : ι), f (g i)
⊢ f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)
have rw₂ : sInf (range (f ∘ g)) = ⨅ (i : ι), f (g i)
Tactic: rw [iSup, Antitone.map_csSup_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
bdd : BddAbove (range g)
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
rw₁ : sInf (f '' range g) = ⨅ (i : ι), f (g i)
rw₂ : sInf (range (f ∘ g)) = ⨅ (i : ι), f (g i)
⊢ f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)
have rw₃ : sInf (range (f ∘ g)) = sInf (range fun (i : ι) ↦ f (g i))
Tactic: rw [iSup, Antitone.map_csSup_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
inst_6 : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
bdd : BddAbove (range g)
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨅ (i : ι), f (g i)
rw₁ : sInf (f '' range g) = ⨅ (i : ι), f (g i)
rw₂ : sInf (range (f ∘ g)) = ⨅ (i : ι), f (g i)
rw₃ : sInf (range (f ∘ g)) = sInf (range fun (i : ι) ↦ f (g i))
⊢ f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)
have rw₄ : Eq.{u_2 + 1} (α := β) (sInf (range fun (x : ι) ↦ f (g x))) (sInf (range fun (i : ι) ↦ f (g i)))
Tactic: rw [iSup, Antitone.map_csSup_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
⊢ f (sSup s) = sSup (f '' s)
have inl : ∀ (h : s = ∅), f (sSup s) = sSup (f '' s)
Tactic: rcases s.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
inl : ∀ (h : s = ∅), f (sSup s) = sSup (f '' s)
⊢ f (sSup s) = sSup (f '' s)
have inr : ∀ (h : s.Nonempty), f (sSup s) = sSup (f '' s)
Tactic: rcases s.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
Tactic: rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup, comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
Tactic: rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup, comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
Tactic: rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup, comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₃ : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
Tactic: rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup, comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
rw₃ : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have rw₄ : Eq.{u_2 + 1} (α := β) (sSup (range fun (x : ι) ↦ f (g x))) (sSup (range fun (i : ι) ↦ f (g i)))
Tactic: rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup, comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Ioo y x)))
have refine_1 : ∀ (l : β) (hl : l < sSup (f '' Ioo y x)), ∀ᶠ (b : α) in 𝓝[<] x, l < f b
Tactic: refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
refine_1 : ∀ (l : β) (hl : l < sSup (f '' Ioo y x)), ∀ᶠ (b : α) in 𝓝[<] x, l < f b
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Ioo y x)))
have refine_2 : ∀ (m : β) (hm : m > sSup (f '' Ioo y x)), ∀ᶠ (b : α) in 𝓝[<] x, f b < m
Tactic: refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b
have refine_1 : ∀ (z : α) (lz : l < f z) (yz : y < z) (zx : z < x), ∀ᶠ (b : α) in 𝓝[<] x, l < f b
Tactic: obtain ⟨z, ⟨yz, zx⟩, lz⟩ : ∃ a : α, a ∈ Ioo y x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h_nonempty.image _) hl
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
z : α
lz : l < f z
yz : y < z
zx : z < x
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b
have h : ∀ (w : α) (hw : w ∈ Ioo z x), l < f w
Tactic: filter_upwards [Ioo_mem_nhdsLT zx] with w hw
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
m : β
hm : m > sSup (f '' Ioo y x)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m
have refine_2 : ∀ (w : α) (hy : y < w) (hx : w < x), ∀ᶠ (b : α) in 𝓝[<] x, f b < m
Tactic: rcases h_nonempty with ⟨_, hy, hx⟩
Cleared hypotheses: h_nonempty
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
m : β
hm : m > sSup (f '' Ioo y x)
w : α
hy : y < w
hx : w < x
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m
have h : ∀ (w : α) (hw : w ∈ Ioo y x), f w < m
Tactic: filter_upwards [Ioo_mem_nhdsLT (hy.trans hx)] with w hw
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
⊢ Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioo x y)))
have refine_1 : ∀ (l : β) (hl : l < sInf (f '' Ioo x y)), ∀ᶠ (b : α) in 𝓝[>] x, l < f b
Tactic: refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
refine_1 : ∀ (l : β) (hl : l < sInf (f '' Ioo x y)), ∀ᶠ (b : α) in 𝓝[>] x, l < f b
⊢ Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioo x y)))
have refine_2 : ∀ (m : β) (hm : m > sInf (f '' Ioo x y)), ∀ᶠ (b : α) in 𝓝[>] x, f b < m
Tactic: refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
l : β
hl : l < sInf (f '' Ioo x y)
⊢ ∀ᶠ (b : α) in 𝓝[>] x, l < f b
have refine_1 : ∀ (p : α) (hy : x < p) (hx : p < y), ∀ᶠ (b : α) in 𝓝[>] x, l < f b
Tactic: rcases h_nonempty with ⟨p, hy, hx⟩
Cleared hypotheses: h_nonempty
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
l : β
hl : l < sInf (f '' Ioo x y)
p : α
hy : x < p
hx : p < y
⊢ ∀ᶠ (b : α) in 𝓝[>] x, l < f b
have h : ∀ (w : α) (hw : w ∈ Ioo x y), l < f w
Tactic: filter_upwards [Ioo_mem_nhdsGT (hy.trans hx)] with w hw
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < m
have refine_2 : ∀ (z : α) (zm : f z < m) (xz : x < z) (zy : z < y), ∀ᶠ (b : α) in 𝓝[>] x, f b < m
Tactic: obtain ⟨z, ⟨xz, zy⟩, zm⟩ : ∃ a : α, a ∈ Ioo x y ∧ f a < m := by
      simpa [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_csInf_lt (h_nonempty.image _) hm
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
z : α
zm : f z < m
xz : x < z
zy : z < y
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < m
have h : ∀ (w : α) (hw : w ∈ Ioo x z), f w < m
Tactic: filter_upwards [Ioo_mem_nhdsGT xz] with w hw
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
have inl : ∀ (h : Iio x = ∅), Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
Tactic: rcases eq_empty_or_nonempty (Iio x) with (h | h)
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
inl : ∀ (h : Iio x = ∅), Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
have inr : ∀ (h : (Iio x).Nonempty), Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
Tactic: rcases eq_empty_or_nonempty (Iio x) with (h | h)
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
have inr : ∀ (l : β) (hl : l < sSup (f '' Iio x)), ∀ᶠ (b : α) in 𝓝[<] x, l < f b
Tactic: refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
inr : ∀ (l : β) (hl : l < sSup (f '' Iio x)), ∀ᶠ (b : α) in 𝓝[<] x, l < f b
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
have inr₁ : ∀ (m : β) (hm : m > sSup (f '' Iio x)), ∀ᶠ (b : α) in 𝓝[<] x, f b < m
Tactic: refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
l : β
hl : l < sSup (f '' Iio x)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b
have inr : ∀ (z : α) (zx : z < x) (lz : l < f z), ∀ᶠ (b : α) in 𝓝[<] x, l < f b
Tactic: obtain ⟨z, zx, lz⟩ : ∃ a : α, a < x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h.image _) hl
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
l : β
hl : l < sSup (f '' Iio x)
z : α
zx : z < x
lz : l < f z
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x_1 : α | x_1 ∈ Ioo z x → Membership.mem (γ := Set α) {x : α | (fun (b : α) ↦ l < f b) x} x_1} a
Tactic: filter_upwards [Ioo_mem_nhdsLT zx] with y hy using lz.trans_le (Mf zx hy.2 hy.1.le)
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
l : β
hl : l < sSup (f '' Iio x)
z : α
zx : z < x
lz : l < f z
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α | x_1 ∈ Ioo z x → Membership.mem (γ := Set α) {x : α | (fun (b : α) ↦ l < f b) x} x_1} a
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b
have h₂ : ∀ a ∈ Ioo z x, l < f a
Tactic: filter_upwards [Ioo_mem_nhdsLT zx] with y hy using lz.trans_le (Mf zx hy.2 hy.1.le)
-- Lean 4 proof step from Mathlib.Topology.Order.Monotone (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
m : β
hm : m > sSup (f '' Iio x)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m
have inr : ∀ (y : α) (hy : y ∈ Iio x), f y ≤ sSup (f '' Iio x)
Tactic: refine mem_of_superset self_mem_nhdsWithin fun y hy => lt_of_le_of_lt ?_ hm
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
⊢ SupConvergenceClass α
have refine_1 : ∀ (a : α) (s : Set α) (ha : IsLUB s a) (b : α) (hb : b < a), ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)
Tactic: refine ⟨fun a s ha => tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
refine_1 :
  ∀ (a : α) (s : Set α) (ha : IsLUB s a) (b : α) (hb : b < a), ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)
⊢ SupConvergenceClass α
have refine_2 : ∀ (a : α) (s : Set α) (ha : IsLUB s a) (b : α) (hb : b > a), ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, (↑b_1 : α) < b
Tactic: refine ⟨fun a s ha => tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
⊢ ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)
have refine_1 : ∀ (c : α) (hcs : c ∈ s) (bc : b < c) (bca : c ≤ a), ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)
Tactic: rcases ha.exists_between hb with ⟨c, hcs, bc, bca⟩
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : α
hcs : c ∈ s
bc : b < c
bca : c ≤ a
⊢ ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)
have refine_1 : ∀ (c : { x : α // x ∈ s }) (bc : b < (↑c : α)) (bca : (↑c : α) ≤ a),
  ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)
Tactic: lift c to s using hcs
Cleared hypotheses: c, hcs, bc, bca
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto f atTop (𝓝 a)
have suffices : Tendsto (rangeFactorization f) atTop atTop
Tactic: suffices Tendsto (rangeFactorization f) atTop atTop from
    (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
have inl : ∀ (h : Eq.{u_3 + 1} (α := Filter ι) atTop ⊥), Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
Tactic: obtain (h | h) := eq_or_ne atTop (⊥ : Filter ι)