awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
have simp_rw : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Iio x ∩ Ici y)) (𝓝[s ∩ Iio x] x) (𝓝 0)
Tactic: simp_rw [← Iio_inter_Ici, ← inter_assoc]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s] x) (𝓝 0)
have A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
Tactic: have A : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0) := by
    simp_rw [← Iio_inter_Ici, ← inter_assoc]
    exact (hf.mono inter_subset_left).tendsto_eVariationOn_Ici_zero_of_filter (𝓝[s ∩ Iio x] x)
      (fun y hy ↦ inter_mem_nhdsWithin _ (Ici_mem_nhds hy.2))
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
have apply : (𝓝[s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)
Tactic: apply tendsto_const_nhds.congr'
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
⊢ (𝓝[s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x_1 : α |
      x_1 ∈ s ∩ Ici x →
        Membership.mem (γ := Set α)
          {x_2 : α |
            (fun (x_3 : α) ↦
                Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (0 : ℝ≥0∞)) x_3) ((fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) x_3))
              x_2}
          x_1}
    a
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha using by simp [show Ico a x = ∅ by grind]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        x_1 ∈ s ∩ Ici x →
          Membership.mem (γ := Set α)
            {x_2 : α |
              (fun (x_3 : α) ↦
                  Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (0 : ℝ≥0∞)) x_3) ((fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) x_3))
                x_2}
            x_1}
      a
⊢ (𝓝[s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)
have h₁ : ∀ a ∈ s ∩ Ici x, 0 = eVariationOn f (s ∩ Ico a x)
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha using by simp [show Ico a x = ∅ by grind]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s] x) (𝓝 0)
have B : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
Tactic: have B : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0) := by
    apply tendsto_const_nhds.congr'
    filter_upwards [self_mem_nhdsWithin] with a ha using by simp [show Ico a x = ∅ by grind]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
B : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s] x) (𝓝 0)
have nth_rewrite : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x ∪ s ∩ Ici x] x) (𝓝 0)
Tactic: nth_rewrite 2 [show s = (s ∩ Iio x) ∪ (s ∩ Ici x) by grind]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
A : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
B : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x ∪ s ∩ Ici x] x) (𝓝 0)
have rw : Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0) ∧
  Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Ici x] x) (𝓝 0)
Tactic: rw [nhdsWithin_union, tendsto_sup]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
⊢ Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
have h : ∀ (y : α),
  eVariationOn f (s ∩ Ioc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x y : α
⊢ eVariationOn f (s ∩ Ioc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
have h : eVariationOn f (s ∩ Ioc x y) =
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc x y)
Tactic: rw [Ico_toDual, ← preimage_inter, comp_ofDual]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x y : α
h :
  eVariationOn f (s ∩ Ioc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc x y)
⊢ eVariationOn f (s ∩ Ioc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
have h₁ : eVariationOn f (s ∩ Ioc x y) =
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Ioc x y))
Tactic: rw [Ico_toDual, ← preimage_inter, comp_ofDual]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x y : α
h :
  eVariationOn f (s ∩ Ioc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc x y)
h₁ :
  eVariationOn f (s ∩ Ioc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Ioc x y))
⊢ eVariationOn f (s ∩ Ioc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
have h₂ : eVariationOn f (s ∩ Ioc x y) = eVariationOn f (s ∩ Ioc x y)
Tactic: rw [Ico_toDual, ← preimage_inter, comp_ofDual]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) (𝓝[s] x) (𝓝 0)
have this : Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) fun (y : α) ↦
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
Tactic: have : (fun y ↦ eVariationOn f (s ∩ Ioc x y)) =
      (fun y ↦ eVariationOn (f ∘ ofDual) (ofDual ⁻¹' s ∩ Ico (toDual y) (toDual x))) := by
    ext y
    rw [Ico_toDual, ← preimage_inter, comp_ofDual]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
this :
  Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Ioc x y)) (𝓝[s] x) (𝓝 0)
have rw : Tendsto (β := ℝ≥0∞)
  (fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ))
  (𝓝[s] x) (𝓝 0)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)
have inl : ∀ (h' : 𝓝[s ∩ Iio x] x = ⊥), Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)
Tactic: rcases eq_or_neBot (𝓝[s ∩ Iio x] x) with h' | h'
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
inl : ∀ (h' : 𝓝[s ∩ Iio x] x = ⊥), Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)
have inr : ∀ (h' : (𝓝[s ∩ Iio x] x).NeBot), Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)
Tactic: rcases eq_or_neBot (𝓝[s ∩ Iio x] x) with h' | h'
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)
have inl : (𝓝[s] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)
Tactic: apply tendsto_const_nhds.congr'
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
⊢ (𝓝[s] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)
have this : s = s ∩ Iio x ∪ s ∩ Ici x
Tactic: have : s = (s ∩ Iio x) ∪ (s ∩ Ici x) := by grind
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
this : s = s ∩ Iio x ∪ s ∩ Ici x
⊢ (𝓝[s] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)
have inl : (𝓝[s ∩ Iio x ∪ s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)
Tactic: nth_rewrite 1 [this]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
this : s = s ∩ Iio x ∪ s ∩ Ici x
⊢ (𝓝[s ∩ Iio x ∪ s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)
have inl : (𝓝[s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)
Tactic: simp only [nhdsWithin_union, h', bot_le, sup_of_le_right]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : 𝓝[s ∩ Iio x] x = ⊥
this : s = s ∩ Iio x ∪ s ∩ Ici x
⊢ (𝓝[s ∩ Ici x] x).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ 0) fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)
have h₁ : ∀ (y : α) (hy : y ∈ s ∩ Ici x), 0 = eVariationOn f (s ∩ Icc y x)
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
⊢ Tendsto (β := ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s] x) (𝓝 0)
have apply : ∀ (y : α), eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
Tactic: apply (hf.tendsto_eVariationOn_Ico_zero x).congr (fun y ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
have inl : ∀ (hy : x ≤ y), eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
Tactic: rcases le_or_gt x y with hy | hy
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
inl : ∀ (hy : x ≤ y), eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
have inr : ∀ (hy : y < x), eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
Tactic: rcases le_or_gt x y with hy | hy
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : x ≤ y
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
have inl : (s ∩ Icc y x).Subsingleton
Tactic: rw [eVariationOn.subsingleton, eVariationOn.subsingleton]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : x ≤ y
inl : (s ∩ Icc y x).Subsingleton
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
have inl₁ : (s ∩ Ico y x).Subsingleton
Tactic: rw [eVariationOn.subsingleton, eVariationOn.subsingleton]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
have inr : ∀ (W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)),
  eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
Tactic: have W := eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt (f := f)
    (s := s ∩ Icc y x) (a := x) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
inr :
  ∀ (W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)),
    eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
have inr₁ : (𝓝[s ∩ Icc y x ∩ Iio x] x).NeBot
Tactic: have W := eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt (f := f)
    (s := s ∩ Icc y x) (a := x) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
inr :
  ∀ (W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)),
    eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
inr₁ : (𝓝[s ∩ Icc y x ∩ Iio x] x).NeBot
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
have inr₂ : ContinuousWithinAt f (s ∩ Icc y x ∩ Iic x) x
Tactic: have W := eVariationOn_inter_Iio_eq_inter_Iic_of_continuousWithinAt (f := f)
    (s := s ∩ Icc y x) (a := x) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
have h₁ : s ∩ Ico y x = s ∩ Icc y x ∩ Iio x
Tactic: convert! W using 2
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
W : eVariationOn f (s ∩ Icc y x ∩ Iio x) = eVariationOn f (s ∩ Icc y x ∩ Iic x)
h₁ : s ∩ Ico y x = s ∩ Icc y x ∩ Iio x
⊢ eVariationOn f (s ∩ Ico y x) = eVariationOn f (s ∩ Icc y x)
have h₂ : s ∩ Icc y x = s ∩ Icc y x ∩ Iic x
Tactic: convert! W using 2
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
⊢ (𝓝[s ∩ Icc y x ∩ Iio x] x).NeBot
have inr : Ici y ∈ 𝓝[s ∩ Iio x] x
Tactic: rwa [show s ∩ Icc y x ∩ Iio x = (s ∩ Iio x) ∩ Ici y by grind, nhdsWithin_inter_of_mem']
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Iic x) x
h' : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y < x
⊢ Ici y ∈ 𝓝[s ∩ Iio x] x
have inr : Ici y ∈ 𝓝 x
Tactic: apply mem_nhdsWithin_of_mem_nhds
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Ici x) x
⊢ Eq.{u_1 + 1} (α := (y : α) → ℝ≥0∞) (fun (y : α) ↦ eVariationOn f (s ∩ Icc x y)) fun (y : α) ↦
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
have h₁ : ∀ (y : α),
  eVariationOn f (s ∩ Icc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Ici x) x
y : α
⊢ eVariationOn f (s ∩ Icc x y) =
    eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → E)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) y) ((toDual : (a : α) → αᵒᵈ) x) : Set αᵒᵈ)
have h₁ : eVariationOn f (s ∩ Icc x y) =
  eVariationOn (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α))
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc x y)
Tactic: rw [Icc_toDual, ← preimage_inter, comp_ofDual]