awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
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
f' : (i : ℕ) → E := fun (i : ℕ) ↦ if i ∈ Iic n then f (v i) else g (u i)
⊢ c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
have this₁ : Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))) (∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i))
Tactic: have : ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) =
        ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i) :=
      Finset.sum_congr rfl (fun i hi ↦ by grind)
-- 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_3 :
  ∀ᶠ (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}
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
f' : (i : ℕ) → E := fun (i : ℕ) ↦ if i ∈ Iic n then f (v i) else g (u i)
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)))
    (∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i))
⊢ c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
have rw : c < ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i)
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 : 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_3 :
  ∀ᶠ (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}
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
f' : (i : ℕ) → E := fun (i : ℕ) ↦ if i ∈ Iic n then f (v i) else g (u i)
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)))
    (∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i))
⊢ c < ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i)
have suffices : f' ∈ I.pi (α := fun (i : ℕ) ↦ E) t
Tactic: suffices H : f' ∈ I.pi t from ht H
-- 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_3 :
  ∀ᶠ (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}
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
f' : (i : ℕ) → E := fun (i : ℕ) ↦ if i ∈ Iic n then f (v i) else g (u i)
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)))
    (∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i))
⊢ f' ∈ I.pi (α := fun (i : ℕ) ↦ E) t
have A : ∀ (i : ℕ), g (u i) ∈ t i
Tactic: have A i : g (u i) ∈ t i := mem_of_mem_nhds (t_mem i)
-- 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}
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
have this₁ : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
Tactic: have : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by
    let f' i := if i ∈ Iic n then f (v i) else g (u i)
    have : ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) =
        ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i) :=
      Finset.sum_congr rfl (fun i hi ↦ by grind)
    rw [this]
    suffices H : f' ∈ I.pi t from ht H
    have A i : g (u i) ∈ t i := mem_of_mem_nhds (t_mem i)
    grind
-- 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_3 :
  ∀ᶠ (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}
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
this : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
⊢ c < eVariationOn f s
have apply : ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f s
Tactic: apply this.trans_le
-- 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_3 :
  ∀ᶠ (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}
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
this_4 : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ∈ Iic n then v i else u i
this : w ∈ J.pi (α := fun (i : ℕ) ↦ α) k
⊢ StrictMonoOn v (Iic n)
have hk₁ : J.pi (α := fun (i : ℕ) ↦ α) k ⊆ {x : ℕ → α | ∀ (a b : ℕ), a ≤ n → b ≤ n → a < b → x a < x b}
Tactic: simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_Iic, and_imp, Prod.forall] at hk
Cleared hypotheses: hk
-- 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_3 :
  ∀ᶠ (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}
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
this : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ∈ Iic n then v i else u i
⊢ StrictMonoOn v (Iic n)
have suffices : w ∈ J.pi (α := fun (i : ℕ) ↦ α) k
Tactic: suffices w ∈ J.pi k by
      simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_Iic, and_imp, Prod.forall] at hk
      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_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_3 :
  ∀ᶠ (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}
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
this : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
w : (i : ℕ) → α := fun (i : ℕ) ↦ if i ∈ Iic n then v i else u i
⊢ w ∈ J.pi (α := fun (i : ℕ) ↦ α) k
have A : ∀ (i : ℕ), u i ∈ k i
Tactic: have A i : u i ∈ k i := mem_of_mem_nhds (k_mem i)
-- 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_3 :
  ∀ᶠ (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}
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
this : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
⊢ ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f s
have v_mono : StrictMonoOn v (Iic n)
Tactic: have v_mono : StrictMonoOn v (Iic n) := by
    let w i := if i ∈ Iic n then v i else u i
    suffices w ∈ J.pi k by
      simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_Iic, and_imp, Prod.forall] at hk
      grind [StrictMonoOn]
    have A i : u i ∈ k i := mem_of_mem_nhds (k_mem i)
    grind
-- 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
⊢ eVariationOn (Function.leftLim f) univ ≤ eVariationOn f univ
have apply : ∀ (x : α) (hx : Membership.mem (γ := Set α) univ x), MapClusterPt (Function.leftLim f x) (𝓝[univ] x) f
Tactic: apply eVariationOn_le_of_mapClusterPt (fun x hx ↦ ?_)
-- 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
⊢ eVariationOn (Function.rightLim f) univ ≤ eVariationOn f univ
have apply : ∀ (x : α) (hx : Membership.mem (γ := Set α) univ x), MapClusterPt (Function.rightLim f x) (𝓝[univ] x) f
Tactic: apply eVariationOn_le_of_mapClusterPt (fun x hx ↦ ?_)
-- 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 α
inst_4 : CompleteSpace E
inst_5 : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x
have this : Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim (Function.leftLim f) x))
Tactic: have : Tendsto f.leftLim (𝓝[<] x) (𝓝 (f.leftLim.leftLim x)) := hf.leftLim.tendsto_leftLim x
-- 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 α
inst_4 : CompleteSpace E
inst_5 : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
this : Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim (Function.leftLim f) x))
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x
have this₁ : Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim f x))
Tactic: rw [leftLim_leftLim (hf.tendsto_leftLim x)] 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
f : α → E
s : Set α
hf : BoundedVariationOn f s
⊢ Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Iic y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ici ((toDual : (a : α) → αᵒᵈ) y) : Set αᵒᵈ)
have h : ∀ (y : α),
  eVariationOn f (s ∩ Iic y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ici ((toDual : (a : α) → αᵒᵈ) y) : Set αᵒᵈ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
y : α
⊢ eVariationOn f (s ∩ Iic y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ici ((toDual : (a : α) → αᵒᵈ) y) : Set αᵒᵈ)
have h : eVariationOn f (s ∩ Iic y) =
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Iic y)
Tactic: rw [Ici_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
f : α → E
s : Set α
hf : BoundedVariationOn f s
y : α
h :
  eVariationOn f (s ∩ Iic y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Iic y)
⊢ eVariationOn f (s ∩ Iic y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ici ((toDual : (a : α) → αᵒᵈ) y) : Set αᵒᵈ)
have h₁ : eVariationOn f (s ∩ Iic y) =
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Iic y))
Tactic: rw [Ici_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
f : α → E
s : Set α
hf : BoundedVariationOn f s
y : α
h :
  eVariationOn f (s ∩ Iic y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Iic y)
h₁ :
  eVariationOn f (s ∩ Iic y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Iic y))
⊢ eVariationOn f (s ∩ Iic y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ici ((toDual : (a : α) → αᵒᵈ) y) : Set αᵒᵈ)
have h₂ : eVariationOn f (s ∩ Iic y) = eVariationOn f (s ∩ Iic y)
Tactic: rw [Ici_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
f : α → E
s : Set α
hf : BoundedVariationOn f s
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Iic y)) (𝓟 s ⊓ atBot) (𝓝 0)
have this : Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Iic y)) fun (y : α) ↦
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ici ((toDual : (a : α) → αᵒᵈ) y) : Set αᵒᵈ)
Tactic: have : (fun y ↦ eVariationOn f (s ∩ Iic y)) =
      (fun y ↦ eVariationOn (f ∘ ofDual) (ofDual ⁻¹' s ∩ Ici (toDual y))) := by
    ext y
    rw [Ici_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
f : α → E
s : Set α
hf : BoundedVariationOn f s
this :
  Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Iic y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ici ((toDual : (a : α) → αᵒᵈ) y) : Set αᵒᵈ)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Iic y)) (𝓟 s ⊓ atBot) (𝓝 0)
have rw : Tendsto (β := ℝ≥0∞)
  (fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ici ((toDual : (a : α) → αᵒᵈ) y) : Set αᵒᵈ))
  (𝓟 s ⊓ atBot) (𝓝 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
hE : Nonempty E
f : α → E
s : Set α
hf : BoundedVariationOn f s
⊢ ∃ (l : E), Tendsto f (𝓟 s ⊓ atTop) (𝓝 l)
have inl : ∀ (hf : BoundedVariationOn f ∅), ∃ (l : E), Tendsto f (𝓟 ∅ ⊓ atTop) (𝓝 l)
Tactic: rcases eq_empty_or_nonempty s with rfl | hs
Cleared hypotheses: s, hf
-- 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
hE : Nonempty E
f : α → E
s : Set α
hf : BoundedVariationOn f s
inl : ∀ (hf : BoundedVariationOn f ∅), ∃ (l : E), Tendsto f (𝓟 ∅ ⊓ atTop) (𝓝 l)
⊢ ∃ (l : E), Tendsto f (𝓟 s ⊓ atTop) (𝓝 l)
have inr : ∀ (hs : s.Nonempty), ∃ (l : E), Tendsto f (𝓟 s ⊓ atTop) (𝓝 l)
Tactic: rcases eq_empty_or_nonempty s with rfl | hs