-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem lowerSemicontinuous_aux {ι : Type*} {F : ι → α → E} {p : Filter ι} {f : α → E} {s : Set α}
    (Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))) {v : ℝ≥0∞} (hv : v < eVariationOn f s) :
    ∀ᶠ n : ι in p, v < eVariationOn (F n) s

Proof state:
case intro.mk.mk.intro
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt : v < ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i))
⊢ ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s

Tactic:
have : Tendsto (fun j => ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))) := by
  apply tendsto_finset_sum
  exact fun i _ => Tendsto.edist (Ffs (u i.succ) (us i.succ)) (Ffs (u i) (us i))

Result:
case intro.mk.mk.intro
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt : v < ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i))
this :
  Tendsto (fun j => ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
⊢ ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
⊢ ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s

Tactic:
obtain ⟨⟨n, ⟨u, um, us⟩⟩, hlt⟩ :
  ∃ p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ i, u i ∈ s },
    v < ∑ i ∈ Finset.range p.1, edist (f ((p.2 : ℕ → α) (i + 1))) (f ((p.2 : ℕ → α) i)) :=
  lt_iSup_iff.mp hv

Result:
case intro.mk.mk.intro
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt : v < ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i))
⊢ ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt : v < ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i))
⊢ Tendsto (fun j => ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))

Tactic:
apply tendsto_finset_sum

Result:
case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt : v < ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i))
⊢ ∀ i ∈ Finset.range n, Tendsto (fun b => edist (F b (u (i + 1))) (F b (u i))) p (𝓝 (edist (f (u (i + 1))) (f (u i))))

Proof state:
case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt : v < ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i))
⊢ ∀ i ∈ Finset.range n, Tendsto (fun b => edist (F b (u (i + 1))) (F b (u i))) p (𝓝 (edist (f (u (i + 1))) (f (u i))))

Tactic:
exact fun i _ => Tendsto.edist (Ffs (u i.succ) (us i.succ)) (Ffs (u i) (us i))

Result:
no goals

Proof state:
case intro.mk.mk.intro
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
n : ℕ
u : ℕ → α
um : Monotone u
us : ∀ (i : ℕ), u i ∈ s
hlt : v < ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i))
this :
  Tendsto (fun j => ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
    (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))
⊢ ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s

Tactic:
exact (this.eventually_const_lt hlt).mono fun i h => h.trans_le (sum_le (F i) n um us)

Result:
no goals