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_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))
suffices : f' ∈ I.pi (α := fun (i : ℕ) ↦ E) t
⊢ c < ∑ i ∈ Finset.range n, edist (f' (i + 1)) (f' i)

Tactic:
suffices H : f' ∈ I.pi t from ht H
-- 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))
⊢ ∀ (i : ℕ), g (u i) ∈ t i

Tactic:
have A i : g (u i) ∈ t i := mem_of_mem_nhds (t_mem i)
-- 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))
A : ∀ (i : ℕ), g (u i) ∈ t i
⊢ f' ∈ I.pi (α := fun (i : ℕ) ↦ E) t

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
⊢ 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
-- 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
this : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
apply : ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f s
⊢ c < eVariationOn f s

Tactic:
apply this.trans_le

Premises used: LT.lt.trans_le
-- 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
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
⊢ 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

Premises used: and_imp, Finset.mem_Iic, Prod.forall, Finset.mem_filter, Finset.mem_product
-- 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)
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
hk : J.pi (α := fun (i : ℕ) ↦ α) k ⊆ {x : ℕ → α | ∀ (a b : ℕ), a ≤ n → b ≤ n → a < b → x a < x b}
⊢ StrictMonoOn v (Iic n)

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_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
suffices : w ∈ J.pi (α := fun (i : ℕ) ↦ α) k
⊢ StrictMonoOn v (Iic n)

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]
-- 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
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
⊢ ∀ (i : ℕ), u i ∈ k i

Tactic:
have A i : u i ∈ k i := mem_of_mem_nhds (k_mem i)
-- 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
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
A : ∀ (i : ℕ), u i ∈ k i
⊢ w ∈ J.pi (α := fun (i : ℕ) ↦ α) k

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_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))
⊢ 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
-- 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
this : c < ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i))
v_mono : StrictMonoOn v (Iic n)
⊢ ∀ i ≤ n, v i ∈ s

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_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))
v_mono : StrictMonoOn v (Iic n)
⊢ ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f s

Tactic:
exact sum_le_of_monotoneOn_Iic v_mono.monotoneOn (by grind)

Premises used: eVariationOn.sum_le_of_monotoneOn_Iic, StrictMonoOn.monotoneOn
-- 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 : α → E
apply : ∀ (x : α) (hx : Membership.mem (γ := Set α) univ x), MapClusterPt (Function.leftLim f x) (𝓝[univ] x) f
⊢ eVariationOn (Function.leftLim f) univ ≤ eVariationOn f univ

Tactic:
apply eVariationOn_le_of_mapClusterPt (fun x hx ↦ ?_)

Premises used: _private.0.eVariationOn.eVariationOn_le_of_mapClusterPt
-- 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 : α → E
x : α
hx : Membership.mem (γ := Set α) univ x
⊢ MapClusterPt (Function.leftLim f x) (𝓝[univ] x) f

Tactic:
apply (mapClusterPt_leftLim f x).mono (nhdsWithin_mono _ (subset_univ _))

Premises used: mapClusterPt_leftLim, Set.subset_univ, MapClusterPt.mono, nhdsWithin_mono
-- 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 : α → E
apply : ∀ (x : α) (hx : Membership.mem (γ := Set α) univ x), MapClusterPt (Function.rightLim f x) (𝓝[univ] x) f
⊢ eVariationOn (Function.rightLim f) univ ≤ eVariationOn f univ

Tactic:
apply eVariationOn_le_of_mapClusterPt (fun x hx ↦ ?_)

Premises used: _private.0.eVariationOn.eVariationOn_le_of_mapClusterPt
-- 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 : α → E
x : α
hx : Membership.mem (γ := Set α) univ x
⊢ MapClusterPt (Function.rightLim f x) (𝓝[univ] x) f

Tactic:
apply (mapClusterPt_rightLim f x).mono (nhdsWithin_mono _ (subset_univ _))

Premises used: Set.subset_univ, mapClusterPt_rightLim, MapClusterPt.mono, nhdsWithin_mono
-- 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 : α → E
hf : BoundedVariationOn f univ
⊢ BoundedVariationOn (Function.leftLim f) univ

Tactic:
(eVariationOn_leftLim_le.trans_lt hf.lt_top).ne

Premises used: Ne.lt_top, LE.le.trans_lt, eVariationOn.eVariationOn_leftLim_le, LT.lt.ne, BoundedVariationOn
-- 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 : α → E
hf : BoundedVariationOn f univ
⊢ BoundedVariationOn (Function.rightLim f) univ

Tactic:
(eVariationOn_rightLim_le.trans_lt hf.lt_top).ne

Premises used: eVariationOn.eVariationOn_rightLim_le, Ne.lt_top, LE.le.trans_lt, LT.lt.ne, BoundedVariationOn
-- 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 α
inst_4 : CompleteSpace E
inst_5 : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
⊢ 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
-- 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 α
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))
⊢ Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim f x))

Tactic:
rw [leftLim_leftLim (hf.tendsto_leftLim x)] at this

Premises used: BoundedVariationOn.tendsto_leftLim, leftLim_leftLim