awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this :
  Function.rightLim f a - Function.leftLim f a + (↑hf.vectorMeasure : Set α → E) (Ioi a) =
    limUnder atTop f - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) (Ioi a) = limUnder atTop f - Function.rightLim f a

Tactic:
grind
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
⊢ Tendsto f atBot (𝓝 (limUnder atBot f))

Tactic:
have hlim : Tendsto f atBot (𝓝 (limUnder atBot f)) := hf.tendsto_atBot_limUnder
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
⊢ ∃ (u : ℕ → α), Antitone u ∧ Tendsto u atTop atBot

Tactic:
Filter.exists_seq_antitone_tendsto_atTop_atBot α

Premises used: Filter.exists_seq_antitone_tendsto_atTop_atBot
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
obtain :
  ∀ (u : ℕ → α) (u_anti : Antitone u) (hu : Tendsto u atTop atBot),
    (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f
⊢ (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f

Tactic:
obtain ⟨u, u_anti, hu⟩ : ∃ u, Antitone u ∧ Tendsto u atTop atBot :=
    Filter.exists_seq_antitone_tendsto_atTop_atBot α

Premises used: Filter.exists_seq_antitone_tendsto_atTop_atBot
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
⊢ ⋃ (n : ℕ), Icc (u n) a ≤ Iic a

Tactic:
simp [Icc_subset_Iic_self]

Premises used: Set.Icc_subset_Iic_self
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
apply : Iic a ≤ ⋃ (n : ℕ), Icc (u n) a
⊢ Iic a = ⋃ (n : ℕ), Icc (u n) a

Tactic:
apply le_antisymm ?_ (by simp [Icc_subset_Iic_self])

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
x : α
x₁ : ∀ (hx : x ≤ a), Membership.mem (γ := Set α) (⋃ (n : ℕ), Icc (u n) a) x
⊢ x ∈ Iic a → Membership.mem (γ := Set α) (⋃ (n : ℕ), Icc (u n) a) x

Tactic:
(hx : x ≤ a)
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
x : α
hx : x ≤ a
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), Icc (u n) a) x

Tactic:
simpa [hx] using (hu.eventually (Iic_mem_atBot x)).exists

Premises used: Filter.Eventually.exists, Filter.Iic_mem_atBot, Filter.Tendsto.eventually
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
⊢ Iic a = ⋃ (n : ℕ), Icc (u n) a

Tactic:
have : Iic a = ⋃ n, Icc (u n) a := by
      apply le_antisymm ?_ (by simp [Icc_subset_Iic_self])
      intro x (hx : x ≤ a)
      simpa [hx] using (hu.eventually (Iic_mem_atBot x)).exists
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
this : Iic a = ⋃ (n : ℕ), Icc (u n) a
rw :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (⋃ (n : ℕ), Icc (u n) a)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
this : Iic a = ⋃ (n : ℕ), Icc (u n) a
i j : ℕ
hij : i ≤ j
x : α
hx : Membership.mem (γ := Set α) ((fun (n : ℕ) ↦ Icc (u n) a) i) x
⊢ Membership.mem (γ := Set α) ((fun (n : ℕ) ↦ Icc (u n) a) j) x

Tactic:
grind [Antitone]

Premises used: Antitone
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
this : Iic a = ⋃ (n : ℕ), Icc (u n) a
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (⋃ (n : ℕ), Icc (u n) a)))

Tactic:
exact hf.vectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat (s := fun n ↦ Icc (u n) a)
      (fun i j hij x hx ↦ by grind [Antitone]) (fun i ↦ measurableSet_Icc)

Premises used: measurableSet_Icc, MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))

Tactic:
have A : Tendsto (fun n ↦ hf.vectorMeasure (Icc (u n) a)) atTop
      (𝓝 (hf.vectorMeasure (Iic a))) := by
    have : Iic a = ⋃ n, Icc (u n) a := by
      apply le_antisymm ?_ (by simp [Icc_subset_Iic_self])
      intro x (hx : x ≤ a)
      simpa [hx] using (hu.eventually (Iic_mem_atBot x)).exists
    rw [this]
    exact hf.vectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat (s := fun n ↦ Icc (u n) a)
      (fun i j hij x hx ↦ by grind [Antitone]) (fun i ↦ measurableSet_Icc)
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
⊢ ∀ (b : α), ∃ (a : ℕ), ∀ b_1 ≥ a, u b_1 ≤ b

Tactic:
simp only [tendsto_atBot, eventually_atTop] at hu

Premises used: Filter.tendsto_atBot, Filter.eventually_atTop
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
hu : ∀ (b : α), ∃ (a : ℕ), ∀ b_1 ≥ a, u b_1 ≤ b
⊢ ∀ᶠ (n : ℕ) in atTop, u n ≤ a

Tactic:
simp [hu]
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
⊢ ∀ᶠ (n : ℕ) in atTop, u n ≤ a

Tactic:
have : ∀ᶠ n in atTop, u n ≤ a := by
        simp only [tendsto_atBot, eventually_atTop] at hu
        simp [hu]
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this : ∀ᶠ (n : ℕ) in atTop, u n ≤ a
n : ℕ
hn : u n ≤ a
rw rw₁ : Function.rightLim f a - Function.leftLim f (u n) = Function.rightLim f a - Function.leftLim f (u n)
⊢ Function.rightLim f a - Function.leftLim f (u n) = (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)

Tactic:
rw [hf.vectorMeasure_Icc hn]

Premises used: BoundedVariationOn.vectorMeasure_Icc
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this : ∀ᶠ (n : ℕ) in atTop, u n ≤ a
h :
  ∀ (a_1 : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ u n ≤ a) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  Eq.{u_2 + 1} (α := E) ((fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) x)
                    ((fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) x))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (n : ℕ) (hn : u n ≤ a),
    Function.rightLim f a - Function.leftLim f (u n) = (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
⊢ EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)

Tactic:
filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
⊢ EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)

Tactic:
have : (fun n ↦ f.rightLim a - f.leftLim (u n)) =ᶠ[atTop]
        (fun n ↦ hf.vectorMeasure (Icc (u n) a)) := by
      have : ∀ᶠ n in atTop, u n ≤ a := by
        simp only [tendsto_atBot, eventually_atTop] at hu
        simp [hu]
      filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this :
  EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
apply :
  Tendsto (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) atTop
    (𝓝 (Function.rightLim f a - limUnder atBot f))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 (Function.rightLim f a - limUnder atBot f))

Tactic:
apply Tendsto.congr' this

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this :
  EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
apply : Tendsto (fun (x : ℕ) ↦ Function.leftLim f (u x)) atTop (𝓝 (limUnder atBot f))
⊢ Tendsto (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) atTop
    (𝓝 (Function.rightLim f a - limUnder atBot f))

Tactic:
apply Tendsto.sub tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this :
  EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
⊢ Tendsto (fun (x : ℕ) ↦ Function.leftLim f (u x)) atTop (𝓝 (limUnder atBot f))

Tactic:
(tendsto_leftLim_atBot_of_tendsto hf.tendsto_atBot_limUnder).comp hu

Premises used: tendsto_leftLim_atBot_of_tendsto, Filter.Tendsto.comp, BoundedVariationOn.tendsto_atBot_limUnder, Function.leftLim, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this_1 : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
this :
  EventuallyEq.{0, u_2} (β := E) atTop (fun (n : ℕ) ↦ Function.rightLim f a - Function.leftLim f (u n)) fun (n : ℕ) ↦
    (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)
⊢ Tendsto (fun (x : ℕ) ↦ Function.leftLim f (u x)) atTop (𝓝 (limUnder atBot f))

Tactic:
exact (tendsto_leftLim_atBot_of_tendsto hf.tendsto_atBot_limUnder).comp hu

Premises used: tendsto_leftLim_atBot_of_tendsto, Filter.Tendsto.comp, BoundedVariationOn.tendsto_atBot_limUnder
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 (Function.rightLim f a - limUnder atBot f))

Tactic:
have B : Tendsto (fun n ↦ hf.vectorMeasure (Icc (u n) a)) atTop
      (𝓝 (f.rightLim a - limUnder atBot f)) := by
    have : (fun n ↦ f.rightLim a - f.leftLim (u n)) =ᶠ[atTop]
        (fun n ↦ hf.vectorMeasure (Icc (u n) a)) := by
      have : ∀ᶠ n in atTop, u n ≤ a := by
        simp only [tendsto_atBot, eventually_atTop] at hu
        simp [hu]
      filter_upwards [this] with n hn using by rw [hf.vectorMeasure_Icc hn]
    apply Tendsto.congr' this
    apply Tendsto.sub tendsto_const_nhds
    exact (tendsto_leftLim_atBot_of_tendsto hf.tendsto_atBot_limUnder).comp hu
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
B :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 (Function.rightLim f a - limUnder atBot f))
⊢ (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f

Tactic:
tendsto_nhds_unique A B

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
inst_5 : CompactIccSpace α
hα : MeasurableSpace α
inst_6 : BorelSpace α
E : Type u_2
inst_7 : NormedAddCommGroup E
inst_8 : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (limUnder atBot f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
A :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (Iic a)))
B :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Icc (u n) a)) atTop
    (𝓝 (Function.rightLim f a - limUnder atBot f))
⊢ (↑hf.vectorMeasure : Set α → E) (Iic a) = Function.rightLim f a - limUnder atBot f

Tactic:
exact tendsto_nhds_unique A B

Premises used: tendsto_nhds_unique