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
a : α
hf : BoundedVariationOn f univ
pos : ∀ (ha : IsBot a), (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
neg : ∀ (ha : ¬IsBot a), (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a

Tactic:
by_cases ha : IsBot a

Premises used: IsBot
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
⊢ ∃ (x : α), IsBot x

Tactic:
have h : ∃ x, IsBot x := ⟨a, ha⟩
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
⊢ h.choose (p := IsBot) = a

Tactic:
have heqa : h.choose = a := subsingleton_isBot _ h.choose_spec ha
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
rw :
  (↑(Exists.choose (p := fun (m : VectorMeasure α E) ↦
            (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
              (↑m : Set α → E) botSet = 0 ∧
                ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s)
            ⋯) :
        Set α → E)
      botSet =
    0
⊢ (↑(Exists.choose (p := fun (m : VectorMeasure α E) ↦
            (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
              (↑m : Set α → E) botSet = 0 ∧
                ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s)
            ⋯) :
        Set α → E)
      {a} =
    0

Tactic:
rw [← botSet_eq_singleton_of_isBot ha]

Premises used: botSet_eq_singleton_of_isBot
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
⊢ (↑(Exists.choose (p := fun (m : VectorMeasure α E) ↦
            (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
              (↑m : Set α → E) botSet = 0 ∧
                ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s)
            ⋯) :
        Set α → E)
      botSet =
    0

Tactic:
hf.exists_vectorMeasure_le_measureAux.choose_spec.2.1

Premises used: _private.0.BoundedVariationOn.exists_vectorMeasure_le_measureAux, Exists.choose_spec, And.right, And.left
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
⊢ (↑(Exists.choose (p := fun (m : VectorMeasure α E) ↦
            (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
              (↑m : Set α → E) botSet = 0 ∧
                ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s)
            ⋯) :
        Set α → E)
      botSet =
    0

Tactic:
exact hf.exists_vectorMeasure_le_measureAux.choose_spec.2.1

Premises used: _private.0.BoundedVariationOn.exists_vectorMeasure_le_measureAux, Exists.choose_spec, And.right, And.left
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
⊢ (↑(Exists.choose (p := fun (m : VectorMeasure α E) ↦
            (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
              (↑m : Set α → E) botSet = 0 ∧
                ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s)
            ⋯) :
        Set α → E)
      {a} =
    0

Tactic:
have A : hf.exists_vectorMeasure_le_measureAux.choose {a} = 0 := by
      rw [← botSet_eq_singleton_of_isBot ha]
      exact hf.exists_vectorMeasure_le_measureAux.choose_spec.2.1
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
A :
  (↑(Exists.choose (p := fun (m : VectorMeasure α E) ↦
            (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
              (↑m : Set α → E) botSet = 0 ∧
                ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s)
            ⋯) :
        Set α → E)
      {a} =
    0
pos :
  (↑(VectorMeasure.dirac (⋯.choose (p := fun (x : α) ↦ IsBot x))
            (Function.rightLim f (⋯.choose (p := fun (x : α) ↦ IsBot x)) - f (⋯.choose (p := fun (x : α) ↦ IsBot x)))) :
        Set α → E)
      {a} =
    Function.rightLim f a - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a

Tactic:
simp only [vectorMeasure, h, ↓reduceDIte, VectorMeasure.coe_add, Pi.add_apply, A,
      zero_add]

Premises used: BoundedVariationOn.vectorMeasure, reduceDIte, zero_add, Pi.add_apply, MeasureTheory.VectorMeasure.coe_add
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
A :
  (↑(Exists.choose (p := fun (m : VectorMeasure α E) ↦
            (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
              (↑m : Set α → E) botSet = 0 ∧
                ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s)
            ⋯) :
        Set α → E)
      {a} =
    0
pos :
  Function.rightLim f (⋯.choose (p := fun (x : α) ↦ IsBot x)) - f (⋯.choose (p := fun (x : α) ↦ IsBot x)) =
    Function.rightLim f a - Function.leftLim f a
pos₁ : Membership.mem (γ := Set α) {a} (⋯.choose (p := fun (x : α) ↦ IsBot x))
⊢ (↑(VectorMeasure.dirac (⋯.choose (p := fun (x : α) ↦ IsBot x))
            (Function.rightLim f (⋯.choose (p := fun (x : α) ↦ IsBot x)) - f (⋯.choose (p := fun (x : α) ↦ IsBot x)))) :
        Set α → E)
      {a} =
    Function.rightLim f a - Function.leftLim f a

Tactic:
rw [VectorMeasure.dirac_apply_of_mem (MeasurableSet.singleton a)]

Premises used: MeasurableSet.singleton, MeasureTheory.VectorMeasure.dirac_apply_of_mem
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
A :
  (↑(Exists.choose (p := fun (m : VectorMeasure α E) ↦
            (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
              (↑m : Set α → E) botSet = 0 ∧
                ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s)
            ⋯) :
        Set α → E)
      {a} =
    0
⊢ Function.rightLim f (⋯.choose (p := fun (x : α) ↦ IsBot x)) - f (⋯.choose (p := fun (x : α) ↦ IsBot x)) =
    Function.rightLim f a - Function.leftLim f a

Tactic:
simpa only [heqa, sub_right_inj] using (leftLim_eq_of_isBot ha).symm

Premises used: sub_right_inj, leftLim_eq_of_isBot, Eq.symm
-- 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
a : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ (x : α), IsBot x
heqa : h.choose (p := IsBot) = a
A :
  (↑(Exists.choose (p := fun (m : VectorMeasure α E) ↦
            (∀ (u v : α), u ≤ v → (↑m : Set α → E) (Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
              (↑m : Set α → E) botSet = 0 ∧
                ∀ (s : Set α), ‖(↑m : Set α → E) s‖ₑ ≤ ((hf.measureAux : Measure α) : (a : Set α) → ℝ≥0∞) s)
            ⋯) :
        Set α → E)
      {a} =
    0
⊢ Membership.mem (γ := Set α) {a} (⋯.choose (p := fun (x : α) ↦ IsBot x))

Tactic:
simp [heqa]
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
⊢ ∃ (b : α), b < a

Tactic:
simpa only [IsBot, not_forall, not_le] using ha

Premises used: not_le, IsBot, Classical.not_forall
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
neg : ∀ (b : α) (hb : b < a), (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a

Tactic:
obtain ⟨b, hb⟩ : ∃ b, b < a := by simpa only [IsBot, not_forall, not_le] using ha
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo b a) ∧ Tendsto u atTop (𝓝 a)

Tactic:
exists_seq_strictMono_tendsto' hb

Premises used: exists_seq_strictMono_tendsto'
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
neg :
  ∀ (u : ℕ → α) (u_mono : StrictMono u) (u_lt_a : ∀ (n : ℕ), u n ∈ Ioo b a) (u_lim : Tendsto u atTop (𝓝 a)),
    (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a
⊢ (↑hf.vectorMeasure : Set α → E) {a} = Function.rightLim f a - Function.leftLim f a

Tactic:
obtain ⟨u, u_mono, u_lt_a, u_lim⟩ :
      ∃ u : ℕ → α, StrictMono u ∧ (∀ n : ℕ, u n ∈ Ioo b a) ∧ Tendsto u atTop (𝓝 a) :=
    exists_seq_strictMono_tendsto' hb

Premises used: exists_seq_strictMono_tendsto'
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lt_a : ∀ (n : ℕ), u n ∈ Ioo b a
u_lim : Tendsto u atTop (𝓝 a)
⊢ ∀ (n : ℕ), u n < a

Tactic:
replace u_lt_a n : u n < a := (u_lt_a n).2
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : α
hx : Membership.mem (γ := Set α) {a} x
⊢ Membership.mem (γ := Set α) (⋂ (n : ℕ), Ioc (u n) a) x

Tactic:
simp [mem_singleton_iff.1 hx, u_lt_a]

Premises used: Set.mem_singleton_iff, Iff.mp
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
refine : ∀ (x : α) (hx : Membership.mem (γ := Set α) (⋂ (n : ℕ), Ioc (u n) a) x), Membership.mem (γ := Set α) {a} x
⊢ Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)

Tactic:
refine Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => ?_

Premises used: Set.Subset.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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : α
hx : Membership.mem (γ := Set α) (⋂ (n : ℕ), Ioc (u n) a) x
⊢ ∀ (i : ℕ), u i < x ∧ x ≤ a

Tactic:
simpa using hx
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : α
hx : Membership.mem (γ := Set α) (⋂ (n : ℕ), Ioc (u n) a) x
⊢ ∀ (i : ℕ), u i < x ∧ x ≤ a

Tactic:
replace hx : ∀ (i : ℕ), u i < x ∧ x ≤ a := by simpa using hx
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : α
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
⊢ a ≤ x

Tactic:
have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : α
hx : ∀ (i : ℕ), u i < x ∧ x ≤ a
this : a ≤ x
⊢ Membership.mem (γ := Set α) {a} x

Tactic:
simp [le_antisymm this (hx 0).2]

Premises used: le_antisymm, And.right, OfNat.ofNat
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
⊢ Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)

Tactic:
have A : {a} = ⋂ n, Ioc (u n) a := by
    refine Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => ?_
    replace hx : ∀ (i : ℕ), u i < x ∧ x ≤ a := by simpa using hx
    have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
    simp [le_antisymm this (hx 0).2]
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
rw :
  Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (⋂ (n : ℕ), Ioc (u n) a)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))

Tactic:
rw [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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
apply : Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ Ioc (u n) a
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop
    (𝓝 ((↑hf.vectorMeasure : Set α → E) (⋂ (n : ℕ), Ioc (u n) a)))

Tactic:
apply VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat ?_ (fun n ↦ measurableSet_Ioc)

Premises used: MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat, measurableSet_Ioc
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
⊢ Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ Ioc (u n) a

Tactic:
fun m n hmn ↦ Ioc_subset_Ioc_left (u_mono.monotone hmn)

Premises used: StrictMono.monotone, Set.Ioc_subset_Ioc_left, 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
⊢ Antitone.{0, u_1} (β := Set α) fun (n : ℕ) ↦ Ioc (u n) a

Tactic:
exact fun m n hmn ↦ Ioc_subset_Ioc_left (u_mono.monotone hmn)

Premises used: StrictMono.monotone, Set.Ioc_subset_Ioc_left
-- 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
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : Eq (α := Set α) {a} (⋂ (n : ℕ), Ioc (u n) a)
⊢ Tendsto (fun (n : ℕ) ↦ (↑hf.vectorMeasure : Set α → E) (Ioc (u n) a)) atTop (𝓝 ((↑hf.vectorMeasure : Set α → E) {a}))

Tactic:
have L1 : Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop (𝓝 (hf.vectorMeasure {a})) := by
    rw [A]
    apply VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat ?_ (fun n ↦ measurableSet_Ioc)
    exact fun m n hmn ↦ Ioc_subset_Ioc_left (u_mono.monotone hmn)