awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Ici x) x
y : α
h₁ :
  eVariationOn f (s ∩ Icc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc x y)
⊢ eVariationOn f (s ∩ Icc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
have h₂ : eVariationOn f (s ∩ Icc x y) =
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Icc x y))
Tactic: rw [Icc_toDual, ← preimage_inter, comp_ofDual]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Ici x) x
y : α
h₁ :
  eVariationOn f (s ∩ Icc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc x y)
h₂ :
  eVariationOn f (s ∩ Icc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Icc x y))
⊢ eVariationOn f (s ∩ Icc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
have h₃ : eVariationOn f (s ∩ Icc x y) = eVariationOn f (s ∩ Icc x y)
Tactic: rw [Icc_toDual, ← preimage_inter, comp_ofDual]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Ici x) x
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc x y)) (𝓝[s] x) (𝓝 0)
have this : Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc x y)) fun (y : α) ↦
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
Tactic: have : (fun y ↦ eVariationOn f (s ∩ Icc x y)) =
      (fun y ↦ eVariationOn (f ∘ ofDual) (ofDual ⁻¹' s ∩ Icc (toDual y) (toDual x))) := by
    ext y
    rw [Icc_toDual, ← preimage_inter, comp_ofDual]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Ici x) x
this :
  Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc x y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc x y)) (𝓝[s] x) (𝓝 0)
have rw : Tendsto (β := ℝ≥0∞)
  (fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ))
  (𝓝[s] x) (𝓝 0)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
⊢ ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
have inl : ∀ (hs : s ∩ Iio x = ∅), ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
Tactic: rcases eq_empty_or_nonempty (s ∩ Iio x) with hs | hs
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
inl : ∀ (hs : s ∩ Iio x = ∅), ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
⊢ ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
have inr : ∀ (hs : (s ∩ Iio x).Nonempty), ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
Tactic: rcases eq_empty_or_nonempty (s ∩ Iio x) with hs | hs
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
hs : s ∩ Iio x = ∅
⊢ ∃ (l : E), Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
have inl : Nonempty E
Tactic: simp only [hs, nhdsWithin_empty, tendsto_bot, exists_const_iff, and_true]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
hf : BoundedVariationOn f univ
x : α
⊢ Tendsto f (𝓝[<] x) (𝓝 (Function.leftLim f x))
have h : ∃ (y : E), Tendsto f (𝓝[<] x) (𝓝 y)
Tactic: apply tendsto_leftLim_of_tendsto
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : CompleteSpace E
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : α → E
hf : BoundedVariationOn f univ
x : α
⊢ ∃ (y : E), Tendsto f (𝓝[<] x) (𝓝 y)
have h : ∀ (x_1 : E), Iio x = univ ∩ Iio x
Tactic: convert! hf.exists_tendsto_left x
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
⊢ eVariationOn g s ≤ eVariationOn f s
have rw : ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
    ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
      edist
        (g
          ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
            (i + 1)))
        (g ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α) i)) ≤
  eVariationOn f s
Tactic: rw [eVariationOn_eq_strictMonoOn]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
⊢ ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (g
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i + 1)))
          (g
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              i)) ≤
    eVariationOn f s
have h : ∀ (i : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
  ∑ i_1 ∈ Finset.range (i.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
      edist
        (g
          ((↑(i.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
            (i_1 + 1)))
        (g
          ((↑(i.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
            i_1)) ≤
    eVariationOn f s
Tactic: apply iSup_le
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
⊢ ∑
      i ∈
        Finset.range
          (Sigma.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
            (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) n
              (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯))),
      edist
        (g
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) n
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯))) :
              ℕ → α)
            (i + 1)))
        (g
          ((↑(Sigma.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })
                  (Sigma.mk (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }) n
                    (Subtype.mk (p := fun (u : ℕ → α) ↦ StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s) u ⋯))) :
              ℕ → α)
            i)) ≤
    eVariationOn f s
have h : ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x)) ≤ eVariationOn f s
Tactic: simp only
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
⊢ ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x)) ≤ eVariationOn f s
have this : Nonempty α
Tactic: have : Nonempty α := ⟨u 0⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this : Nonempty α
⊢ ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x)) ≤ eVariationOn f s
have apply : ∀ (c : ℝ≥0∞) (hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))), c < eVariationOn f s
Tactic: apply le_of_forall_lt (fun c hc ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
⊢ ∀ᶠ (b : ℕ → E) in 𝓝 fun (i : ℕ) ↦ g (u i), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
have this₁ : Continuous[Pi.topologicalSpace, _] fun (v : ℕ → E) ↦ ∑ i ∈ Finset.range n, edist (v (i + 1)) (v i)
Tactic: have : Continuous (fun (v : ℕ → E) ↦ ∑ i ∈ Finset.range n, edist (v (i + 1)) (v i)) := by
      fun_prop
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
⊢ c < eVariationOn f s
have this₁ : ∀ᶠ (b : ℕ → E) in 𝓝 fun (i : ℕ) ↦ g (u i), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
Tactic: have : ∀ᶠ (b : ℕ → E) in 𝓝 (fun i ↦ g (u i)),
      c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i) := by
    have : Continuous (fun (v : ℕ → E) ↦ ∑ i ∈ Finset.range n, edist (v (i + 1)) (v i)) := by
      fun_prop
    exact (tendsto_order.1 (this.continuousAt (x := fun i ↦ g (u i))).tendsto).1 c hc
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this_1 : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this : ∀ᶠ (b : ℕ → E) in 𝓝 fun (i : ℕ) ↦ g (u i), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
⊢ c < eVariationOn f s
have this₁ : ∀ᶠ (b : ℕ → E) in Filter.pi (α := fun (i : ℕ) ↦ E) fun (i : ℕ) ↦ 𝓝 (g (u i)),
  c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
Tactic: rw [nhds_pi] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this_1 : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this :
  ∀ᶠ (b : ℕ → E) in Filter.pi (α := fun (i : ℕ) ↦ E) fun (i : ℕ) ↦ 𝓝 (g (u i)),
    c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
⊢ c < eVariationOn f s
have obtain : ∀ (I : Set ℕ) (I_fin : I.Finite) (t : (i : ℕ) → Set E) (t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i)))
  (ht : I.pi (α := fun (a : ℕ) ↦ E) t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}),
  c < eVariationOn f s
Tactic: obtain ⟨I, I_fin, t, t_mem, ht⟩ : ∃ (I : Set ℕ), I.Finite ∧ ∃ t, (∀ (i : ℕ), t i ∈ 𝓝 (g (u i))) ∧
      I.pi t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)} := mem_pi.1 this
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this_1 : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this :
  ∀ᶠ (b : ℕ → E) in Filter.pi (α := fun (i : ℕ) ↦ E) fun (i : ℕ) ↦ 𝓝 (g (u i)),
    c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : (i : ℕ) → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi (α := fun (a : ℕ) ↦ E) t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
⊢ ∀ᶠ (b : ℕ → α) in 𝓝 u, ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
have rw : ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, ∀ᶠ (x : ℕ → α) in 𝓝 u, x i.1 < x i.2
Tactic: rw [Filter.eventually_all_finset]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this_1 : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this :
  ∀ᶠ (b : ℕ → E) in Filter.pi (α := fun (i : ℕ) ↦ E) fun (i : ℕ) ↦ 𝓝 (g (u i)),
    c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : (i : ℕ) → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi (α := fun (a : ℕ) ↦ E) t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
i : ℕ × ℕ
hi : i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}
⊢ ∀ᶠ (x : ℕ → α) in 𝓝 u, x i.1 < x i.2
have apply : IsOpen[Pi.topologicalSpace] {x : ℕ → α | (fun (x : ℕ → α) ↦ x i.1 < x i.2) x}
Tactic: apply IsOpen.mem_nhds ?_ (by grind [StrictMonoOn])
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this_1 : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this :
  ∀ᶠ (b : ℕ → E) in Filter.pi (α := fun (i : ℕ) ↦ E) fun (i : ℕ) ↦ 𝓝 (g (u i)),
    c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : (i : ℕ) → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi (α := fun (a : ℕ) ↦ E) t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
⊢ c < eVariationOn f s
have this₁ : ∀ᶠ (b : ℕ → α) in 𝓝 u, ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
Tactic: have : ∀ᶠ b in 𝓝 u, ∀ i ∈ ((Finset.Iic n) ×ˢ (Finset.Iic n)).filter
      (fun i ↦ i.1 < i.2), b i.1 < b i.2 := by
    rw [Filter.eventually_all_finset]
    intro i hi
    apply IsOpen.mem_nhds ?_ (by grind [StrictMonoOn])
    exact isOpen_lt (by fun_prop) (by fun_prop)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this_1 : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this_2 :
  ∀ᶠ (b : ℕ → E) in Filter.pi (α := fun (i : ℕ) ↦ E) fun (i : ℕ) ↦ 𝓝 (g (u i)),
    c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : (i : ℕ) → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi (α := fun (a : ℕ) ↦ E) t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
this : ∀ᶠ (b : ℕ → α) in 𝓝 u, ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
⊢ c < eVariationOn f s
have this₁ : ∀ᶠ (b : ℕ → α) in Filter.pi (α := fun (i : ℕ) ↦ α) fun (i : ℕ) ↦ 𝓝 (u i),
  ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
Tactic: rw [nhds_pi] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this_1 : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this_2 :
  ∀ᶠ (b : ℕ → E) in Filter.pi (α := fun (i : ℕ) ↦ E) fun (i : ℕ) ↦ 𝓝 (g (u i)),
    c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : (i : ℕ) → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi (α := fun (a : ℕ) ↦ E) t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
this :
  ∀ᶠ (b : ℕ → α) in Filter.pi (α := fun (i : ℕ) ↦ α) fun (i : ℕ) ↦ 𝓝 (u i),
    ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
⊢ c < eVariationOn f s
have obtain : ∀ (J : Set ℕ) (J_fin : J.Finite) (k : (i : ℕ) → Set α) (k_mem : ∀ (i : ℕ), k i ∈ 𝓝 (u i))
  (hk :
    J.pi (α := fun (i : ℕ) ↦ α) k ⊆
      {x : ℕ → α | (fun (b : ℕ → α) ↦ ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2) x}),
  c < eVariationOn f s
Tactic: obtain ⟨J, J_fin, k, k_mem, hk⟩ : ∃ (J : Set ℕ), J.Finite ∧ ∃ k, (∀ (i : ℕ), k i ∈ 𝓝 (u i)) ∧
    J.pi k ⊆ _ := mem_pi.1 this
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this_1 : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this_2 :
  ∀ᶠ (b : ℕ → E) in Filter.pi (α := fun (i : ℕ) ↦ E) fun (i : ℕ) ↦ 𝓝 (g (u i)),
    c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : (i : ℕ) → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi (α := fun (a : ℕ) ↦ E) t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
this :
  ∀ᶠ (b : ℕ → α) in Filter.pi (α := fun (i : ℕ) ↦ α) fun (i : ℕ) ↦ 𝓝 (u i),
    ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
J : Set ℕ
J_fin : J.Finite
k : (i : ℕ) → Set α
k_mem : ∀ (i : ℕ), k i ∈ 𝓝 (u i)
hk :
  J.pi (α := fun (i : ℕ) ↦ α) k ⊆
    {x : ℕ → α | (fun (b : ℕ → α) ↦ ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2) x}
⊢ c < eVariationOn f s
have A : ∀ (i : ℕ) (hi : i ∈ Iic n), ∃ (x : α), (f x ∈ t i ∧ x ∈ k i) ∧ x ∈ s
Tactic: have A i (hi : i ∈ Iic n) : ∃ x, (f x ∈ t i ∧ x ∈ k i) ∧ x ∈ s :=
    ((((mapClusterPt_iff_frequently.1 (hg (u i) (u_mem i hi)) (t i) (t_mem i))).and_eventually
      (mem_nhdsWithin_of_mem_nhds (k_mem i))).and_eventually self_mem_nhdsWithin).exists
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this_1 : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this_2 :
  ∀ᶠ (b : ℕ → E) in Filter.pi (α := fun (i : ℕ) ↦ E) fun (i : ℕ) ↦ 𝓝 (g (u i)),
    c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : (i : ℕ) → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi (α := fun (a : ℕ) ↦ E) t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
this :
  ∀ᶠ (b : ℕ → α) in Filter.pi (α := fun (i : ℕ) ↦ α) fun (i : ℕ) ↦ 𝓝 (u i),
    ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2
J : Set ℕ
J_fin : J.Finite
k : (i : ℕ) → Set α
k_mem : ∀ (i : ℕ), k i ∈ 𝓝 (u i)
hk :
  J.pi (α := fun (i : ℕ) ↦ α) k ⊆
    {x : ℕ → α | (fun (b : ℕ → α) ↦ ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2) x}
A : ∀ (i : ℕ) (hi : i ∈ Iic n), ∃ (x : α), (f x ∈ t i ∧ x ∈ k i) ∧ x ∈ s
⊢ c < eVariationOn f s
have choose! : ∀ (v : (i : ℕ) → α) (hv : ∀ (i : ℕ) (hi : i ∈ Iic n), f (v i) ∈ t i ∧ v i ∈ k i)
  (h'v : ∀ (i : ℕ) (hi : i ∈ Iic n), v i ∈ s), c < eVariationOn f s
Tactic: choose! v hv h'v using A
Cleared hypotheses: A