awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x_1 y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
T : (n : ℕ) → Set α
h : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), (T n).Countable
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)
x : α
n : ℕ
hn : x ∈ compactCovering α n
⊢ Membership.mem (γ := Set α) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (n : ℕ), T n)) x

Tactic:
closure_mono (subset_iUnion _ n) (hsubT _ hn)

Premises used: closure_mono, Set.subset_iUnion
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x_1 y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
T : (n : ℕ) → Set α
h : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), (T n).Countable
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)
x : α
n : ℕ
hn : x ∈ compactCovering α n
⊢ Membership.mem (γ := Set α) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (n : ℕ), T n)) x

Tactic:
exact closure_mono (subset_iUnion _ n) (hsubT _ hn)

Premises used: closure_mono, Set.subset_iUnion
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
suffices : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
⊢ ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Subset.{u} (α := Set α) univ (⋃ x ∈ t, closedEBall x ε)

Tactic:
simpa only [univ_subset_iff] using hs

Premises used: Set.univ_subset_iff
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
⊢ ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Subset.{u} (α := Set α) univ (⋃ x ∈ t, closedEBall x ε)

Tactic:
have : ∀ ε > 0, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, closedEBall x ε := by
    simpa only [univ_subset_iff] using hs
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
this : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Subset.{u} (α := Set α) univ (⋃ x ∈ t, closedEBall x ε)
rcases :
  ∀ (t : Set α) (htc : t.Countable) (ht : univ ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t),
    SeparableSpace α
⊢ SeparableSpace α

Tactic:
rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩

Premises used: Set.univ, EMetric.subset_countable_closure_of_almost_dense_set
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
this : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Subset.{u} (α := Set α) univ (⋃ x ∈ t, closedEBall x ε)
t : Set α
htc : t.Countable
ht : univ ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ SeparableSpace α

Tactic:
⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩

Premises used: And.intro, Exists.intro, Set.mem_univ, TopologicalSpace.SeparableSpace.mk
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
this : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Subset.{u} (α := Set α) univ (⋃ x ∈ t, closedEBall x ε)
t : Set α
htc : t.Countable
ht : univ ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ SeparableSpace α

Tactic:
exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
β : Type v
γ : Type w
inst : EMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : γ → β
rw :
  IsUniformInducing f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
rw₁ :
  (UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ) ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
rw₂ rw₃ :
  ((∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ) ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
⊢ IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]

Premises used: EMetric.uniformContinuous_iff, isUniformEmbedding_iff_isUniformInducing, EMetric.isUniformInducing_iff
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
γ : Type w
inst : EMetricSpace γ
s : Set γ
hs : IsCompact s
rcases :
  ∀ (t : Set γ) (hts : t ⊆ s) (htc : t.Countable)
    (hsub : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t),
    ∃ t ⊆ s, t.Countable ∧ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
rcases subset_countable_closure_of_compact hs with ⟨t, hts, htc, hsub⟩

Premises used: EMetric.subset_countable_closure_of_compact
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
γ : Type w
inst : EMetricSpace γ
s : Set γ
hs : IsCompact s
t : Set γ
hts : t ⊆ s
htc : t.Countable
hsub : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
⟨t, hts, htc, hsub.antisymm (closure_minimal hts hs.isClosed)⟩

Premises used: closure_minimal, HasSubset.Subset.antisymm, And.intro, Exists.intro, IsCompact.isClosed
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
γ : Type w
inst : EMetricSpace γ
s : Set γ
hs : IsCompact s
t : Set γ
hts : t ⊆ s
htc : t.Countable
hsub : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
exact ⟨t, hts, htc, hsub.antisymm (closure_minimal hts hs.isClosed)⟩
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
x y : X
⊢ edist (α := SeparationQuotient X) (mk x) (mk y) = edist x y

Tactic:
rfl

Premises used: SeparationQuotient.lift₂, rfl, Quotient.liftOn₂'
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
γ : Type w
inst_1 : EMetricSpace γ
inst_2 : PseudoEMetricSpace X
⊢ Eq.{u_1 + 1} (α := Filter (X × X))
    (comap (β := SeparationQuotient X × SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk)
      (𝓤 (SeparationQuotient X)))
    (comap (β := SeparationQuotient X × SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk)
      (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : SeparationQuotient X × SeparationQuotient X | edist p.1 p.2 < ε}))

Tactic:
simp [comap_mk_uniformity, PseudoEMetricSpace.uniformity_edist]

Premises used: SeparationQuotient.comap_mk_uniformity, PseudoEMetricSpace.uniformity_edist
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ (i : ι), eball x δ ⊆ c i

Tactic:
simpa only [eball, UniformSpace.ball, preimage_setOf_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma hs hc₁ hc₂

Premises used: PseudoEMetricSpace.edist_comm, uniformity_basis_edist, Metric.eball, UniformSpace.ball, Set.preimage_setOf_eq, Filter.HasBasis.lebesgue_number_lemma
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
c : (x : α) → x ∈ s → Set α
hs : IsCompact s
hc : ∀ (x : α) (hx : x ∈ s), c x hx ∈ 𝓝 x
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ (y : (↑s : Type u)), eball x δ ⊆ c (↑y : α) ⋯

Tactic:
simpa only [eball, UniformSpace.ball, preimage_setOf_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhds' hs hc

Premises used: PseudoEMetricSpace.edist_comm, uniformity_basis_edist, Metric.eball, UniformSpace.ball, Set.preimage_setOf_eq, Filter.HasBasis.lebesgue_number_lemma_nhds'
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
c : α → Set α
hs : IsCompact s
hc : ∀ x ∈ s, c x ∈ 𝓝 x
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ (y : α), eball x δ ⊆ c y

Tactic:
simpa only [eball, UniformSpace.ball, preimage_setOf_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhds hs hc

Premises used: PseudoEMetricSpace.edist_comm, Filter.HasBasis.lebesgue_number_lemma_nhds, uniformity_basis_edist, Metric.eball, UniformSpace.ball, Set.preimage_setOf_eq
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
c : (x : α) → x ∈ s → Set α
hs : IsCompact s
hc : ∀ (x : α) (hx : x ∈ s), c x hx ∈ 𝓝[s] x
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ (y : (↑s : Type u)), eball x δ ∩ s ⊆ c (↑y : α) ⋯

Tactic:
simpa only [eball, UniformSpace.ball, preimage_setOf_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhdsWithin' hs hc

Premises used: PseudoEMetricSpace.edist_comm, uniformity_basis_edist, Metric.eball, UniformSpace.ball, Set.preimage_setOf_eq, Filter.HasBasis.lebesgue_number_lemma_nhdsWithin'
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
c : α → Set α
hs : IsCompact s
hc : ∀ x ∈ s, c x ∈ 𝓝[s] x
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ (y : α), eball x δ ∩ s ⊆ c y

Tactic:
simpa only [eball, UniformSpace.ball, preimage_setOf_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhdsWithin hs hc

Premises used: PseudoEMetricSpace.edist_comm, uniformity_basis_edist, Metric.eball, UniformSpace.ball, Set.preimage_setOf_eq, Filter.HasBasis.lebesgue_number_lemma_nhdsWithin
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃₀ c
⊢ s ⊆ ⋃ (i : (↑c : Type u)), (↑i : Set α)

Tactic:
rw [sUnion_eq_iUnion] at hc₂

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ (i : (↑c : Type u)), (↑i : Set α)
⊢ ∀ (i : (↑c : Type u)), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑i : Set α)

Tactic:
simpa
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ (i : (↑c : Type u)), (↑i : Set α)
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, eball x δ ⊆ t

Tactic:
simpa using lebesgue_number_lemma_of_emetric hs (by simpa) hc₂

Premises used: lebesgue_number_lemma_of_emetric
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
hs : s.Nonempty
obtain : ∀ (x : α) (hx : x ∈ s), Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
⊢ Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }

Tactic:
obtain ⟨x, hx⟩ := hs
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }

Tactic:
⟨⟨fun _ => x, fun i j _ => le_rfl, fun _ => hx⟩⟩

Premises used: le_rfl, Nonempty.intro, Subtype.mk, And.intro
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }

Tactic:
exact ⟨⟨fun _ => x, fun i j _ => le_rfl, fun _ => hx⟩⟩
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
e_s :
  ∀ (p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
    Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i)))
      (∑ i ∈ Finset.range p.1, edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i)))
⊢ Eq (α := ℝ≥0∞)
    (⨆ (p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
      ∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i)))
    (⨆ (p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
      ∑ i ∈ Finset.range p.1, edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i)))

Tactic:
congr 1 with p : 1
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
e_s :
  ∀ (i : ℕ),
    edist (f ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i)) =
      edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i))
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range p.1, edist (f ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i)))
    (∑ i ∈ Finset.range p.1, edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i)))

Tactic:
congr 1 with i : 1
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
i : ℕ
e_s :
  edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i)) =
    edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i))
e_s₁ e_s₂ :
  edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i)) =
    edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i))
⊢ edist (f ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i)) =
    edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i))

Tactic:
rw [edist_congr_right (h <| p.snd.prop.2 (i + 1)), edist_congr_left (h <| p.snd.prop.2 i)]

Premises used: edist_congr_left, And.right, HAdd.hAdd, Subtype.prop, edist_congr_right, OfNat.ofNat, Prod.snd
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : EqOn f f' s
x : α
xs : x ∈ s
rw : edist (f' x) (f' x) = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ edist (f x) (f' x) = 0

Tactic:
rw [h xs, edist_self]

Premises used: PseudoEMetricSpace.edist_self
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
le_iSup_of_le ⟨n, u, hu, us⟩ le_rfl

Premises used: le_rfl, Prod.mk, eVariationOn, Subtype.mk, le_iSup_of_le, And.intro
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
inl : ∀ (hnm : n ≤ m), ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
inr : ∀ (hmn : m ≤ n), ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
rcases le_total n m with hnm | hmn

Premises used: le_total
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hnm : n ≤ m
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
simp [Finset.Ico_eq_empty_of_le hnm]

Premises used: Finset.Ico_eq_empty_of_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : (x : ℕ) → (↑(Icc m n) : Type) := projIcc m n hmn
v : (i : ℕ) → α := fun (i : ℕ) ↦ u (↑(π i) : ℕ)
i : ℕ
hi : i ∈ Finset.Ico m n
⊢ m ≤ i ∧ i < n

Tactic:
rw [Finset.mem_Ico] at hi

Premises used: Finset.mem_Ico
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : (x : ℕ) → (↑(Icc m n) : Type) := projIcc m n hmn
v : (i : ℕ) → α := fun (i : ℕ) ↦ u (↑(π i) : ℕ)
i : ℕ
hi : m ≤ i ∧ i < n
⊢ edist (f (u (i + 1))) (f (u i)) = edist (f (v (i + 1))) (f (v i))

Tactic:
simp only [v, π, projIcc_of_mem hmn ⟨hi.1, hi.2.le⟩,
          projIcc_of_mem hmn ⟨hi.1.trans i.le_succ, hi.2⟩]

Premises used: LT.lt.le, Nat.le_succ, Set.projIcc_of_mem, And.right, And.left, And.intro, LE.le.trans
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : (x : ℕ) → (↑(Icc m n) : Type) := projIcc m n hmn
v : (i : ℕ) → α := fun (i : ℕ) ↦ u (↑(π i) : ℕ)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ico m n, edist (f (v (i + 1))) (f (v i)))
    (∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)))

Tactic:
Finset.sum_mono_set _ (Nat.Iio_eq_range n ▸ Finset.Ico_subset_Iio_self)

Premises used: Finset.sum_mono_set, Eq.rec, Finset.Ico_subset_Iio_self, Nat.Iio_eq_range
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : (x : ℕ) → (↑(Icc m n) : Type) := projIcc m n hmn
v : (i : ℕ) → α := fun (i : ℕ) ↦ u (↑(π i) : ℕ)
⊢ ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) ≤ eVariationOn f s

Tactic:
sum_le (fun i j h ↦ hu (π i).2 (π j).2 (monotone_projIcc hmn h)) fun i ↦ us _ (π i).2

Premises used: eVariationOn.sum_le, Set.monotone_projIcc, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
π : (x : ℕ) → (↑(Icc m n) : Type) := projIcc m n hmn
v : (i : ℕ) → α := fun (i : ℕ) ↦ u (↑(π i) : ℕ)
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
calc
    ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i))
        = ∑ i ∈ Finset.Ico m n, edist (f (v (i + 1))) (f (v i)) :=
      Finset.sum_congr rfl fun i hi ↦ by
        rw [Finset.mem_Ico] at hi
        simp only [v, π, projIcc_of_mem hmn ⟨hi.1, hi.2.le⟩,
          projIcc_of_mem hmn ⟨hi.1.trans i.le_succ, hi.2⟩]
    _ ≤ ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) :=
      Finset.sum_mono_set _ (Nat.Iio_eq_range n ▸ Finset.Ico_subset_Iio_self)
    _ ≤ eVariationOn f s :=
      sum_le (fun i j h ↦ hu (π i).2 (π j).2 (monotone_projIcc hmn h)) fun i ↦ us _ (π i).2

Premises used: Finset.sum_mono_set, Finset.Ico, eVariationOn, Finset.range, eVariationOn.sum_le, Set.monotone_projIcc, Subtype.val, Finset.sum_congr, rfl, Subtype.property
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
hu : MonotoneOn u (Iic n)
us : ∀ i ≤ n, u i ∈ s
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
simpa using sum_le_of_monotoneOn_Icc (m := 0) (hu.mono Icc_subset_Iic_self) fun i hi ↦ us i hi.2

Premises used: eVariationOn.sum_le_of_monotoneOn_Icc, Set.Icc_subset_Iic_self, And.right, MonotoneOn.mono
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a :
  eVariationOn f s ≤
    ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i + 1)))
          (f ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α) i))
a₁ :
  ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i + 1)))
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              i)) ≤
    eVariationOn f s
⊢ eVariationOn f s =
    ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i + 1)))
          (f ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α) i))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a :
  ∀ (i : ℕ × { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
    LE.le (α := ℝ≥0∞) (∑ i_1 ∈ Finset.range i.1, edist (f ((↑i.2 : ℕ → α) (i_1 + 1))) (f ((↑i.2 : ℕ → α) i_1)))
      (⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
        ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
          edist
            (f
              ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
                (i + 1)))
            (f
              ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
                i)))
⊢ eVariationOn f s ≤
    ⨆ (p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }),
      ∑ i ∈ Finset.range (p.fst (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })),
        edist
          (f
            ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α)
              (i + 1)))
          (f ((↑(p.snd (β := fun (n : ℕ) ↦ { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s })) : ℕ → α) i))

Tactic:
apply iSup_le

Premises used: iSup_le