awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))
⊢ 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
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : Continuous[Pi.topologicalSpace, _] fun (v : ℕ → E) ↦ ∑ i ∈ Finset.range n, edist (v (i + 1)) (v i)
⊢ ∀ᶠ (b : ℕ → E) in 𝓝 fun (i : ℕ) ↦ g (u i), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)

Tactic:
(tendsto_order.1 (this.continuousAt (x := fun i ↦ g (u i))).tendsto).1 c hc

Premises used: tendsto_order, Continuous.continuousAt, ContinuousAt.tendsto, And.left, Iff.mp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : Continuous[Pi.topologicalSpace, _] fun (v : ℕ → E) ↦ ∑ i ∈ Finset.range n, edist (v (i + 1)) (v i)
⊢ ∀ᶠ (b : ℕ → E) in 𝓝 fun (i : ℕ) ↦ g (u i), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)

Tactic:
exact (tendsto_order.1 (this.continuousAt (x := fun i ↦ g (u i))).tendsto).1 c hc

Premises used: tendsto_order, Continuous.continuousAt, ContinuousAt.tendsto, And.left, Iff.mp
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)

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
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
⊢ ∀ᶠ (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

Premises used: nhds_pi
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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.Finite ∧
      ∃ (t : (i : ℕ) → Set E),
        (∀ (i : ℕ), t i ∈ 𝓝 (g (u i))) ∧
          I.pi (α := fun (a : ℕ) ↦ E) t ⊆ {b : ℕ → E | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}

Tactic:
mem_pi.1 this
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
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
⊢ 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

Premises used: Finset.range, Nat, Iff.mp, Filter.mem_pi, Set
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)}
rw : ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, ∀ᶠ (x : ℕ → α) in 𝓝 u, x i.1 < x i.2
⊢ ∀ᶠ (b : ℕ → α) in 𝓝 u, ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, b i.1 < b i.2

Tactic:
rw [Filter.eventually_all_finset]

Premises used: Filter.eventually_all_finset
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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}
⊢ Membership.mem (γ := Set (ℕ → α)) {x : ℕ → α | (fun (x : ℕ → α) ↦ x i.1 < x i.2) x} u

Tactic:
grind [StrictMonoOn]

Premises used: StrictMonoOn
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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}
apply : IsOpen[Pi.topologicalSpace] {x : ℕ → α | (fun (x : ℕ → α) ↦ x i.1 < x i.2) x}
⊢ ∀ᶠ (x : ℕ → α) in 𝓝 u, x i.1 < x i.2

Tactic:
apply IsOpen.mem_nhds ?_ (by grind [StrictMonoOn])

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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}
⊢ Continuous[Pi.topologicalSpace, inst_2] fun (x : ℕ → α) ↦ x i.1

Tactic:
fun_prop
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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}
⊢ Continuous[Pi.topologicalSpace, inst_2] fun (x : ℕ → α) ↦ x i.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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}
⊢ IsOpen[Pi.topologicalSpace] {x : ℕ → α | (fun (x : ℕ → α) ↦ x i.1 < x i.2) x}

Tactic:
exact isOpen_lt (by fun_prop) (by fun_prop)

Premises used: isOpen_lt
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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

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)
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ ∀ᶠ (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

Premises used: nhds_pi
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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.Finite ∧
      ∃ (k : (i : ℕ) → Set α),
        (∀ (i : ℕ), k i ∈ 𝓝 (u i)) ∧
          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}

Tactic:
mem_pi.1 this
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
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
⊢ 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

Premises used: Nat, Iff.mp, Filter.mem_pi, Set
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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}
⊢ ∀ (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
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
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
⊢ c < eVariationOn f s

Tactic:
choose! v hv h'v using A
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
i : ℕ
hi : i ∈ Finset.range n
⊢ edist (f (v (i + 1))) (f (v i)) = edist (f' (i + 1)) (f' i)

Tactic:
grind
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
⊢ 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)
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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))
rw : c < ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i)
⊢ c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))

Tactic:
rw [this]