awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u_2
inst : EMetricSpace α
⊢ Nontrivial α ↔ NontrivialTopology α
have simp_rw : (∃ (x : α) (y : α), x ≠ y) ↔ NontrivialTopology α
Tactic: simp_rw [nontrivial_iff, TopologicalSpace.nontrivial_iff_exists_not_inseparable,
    EMetric.inseparable_iff, edist_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u_2
inst : EMetricSpace α
simp_rw : (∃ (x : α) (y : α), x ≠ y) ↔ NontrivialTopology α
⊢ Nontrivial α ↔ NontrivialTopology α
have simp_rw₁ : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (x : α) (y : α), ¬Inseparable x y
Tactic: simp_rw [nontrivial_iff, TopologicalSpace.nontrivial_iff_exists_not_inseparable,
    EMetric.inseparable_iff, edist_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u_2
inst : EMetricSpace α
simp_rw : (∃ (x : α) (y : α), x ≠ y) ↔ NontrivialTopology α
simp_rw₁ : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (x : α) (y : α), ¬Inseparable x y
⊢ Nontrivial α ↔ NontrivialTopology α
have simp_rw₂ : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (x : α) (y : α), ¬edist x y = 0
Tactic: simp_rw [nontrivial_iff, TopologicalSpace.nontrivial_iff_exists_not_inseparable,
    EMetric.inseparable_iff, edist_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
have hs₁ : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
Tactic: apply UniformSpace.subset_countable_closure_of_almost_dense_set
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
have hs₁ : ∀ (ε : ℝ≥0∞) (hε : 0 < ε) (hεU : {p : α × α | edist p.1 p.2 ≤ ε} ⊆ U),
  ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
Tactic: obtain ⟨ε, hε, hεU⟩ := uniformity_basis_edist_le.mem_iff.1 hU
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p : α × α | edist p.1 p.2 ≤ ε} ⊆ U
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
have hs₁ : ∀ (t : Set α) (tC : t.Countable) (ht : s ⊆ ⋃ x ∈ t, closedEBall x ε),
  ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
Tactic: obtain ⟨t, tC, ht⟩ := hs ε hε
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p : α × α | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
have hs₁ : ∀ (x : α) (hx : x ∈ t) (y : α) (hy : y ∈ closedEBall x ε), y ∈ UniformSpace.ball x {p : α × α | edist p.1 p.2 ≤ ε}
Tactic: refine ⟨t, tC, ht.trans (iUnion₂_mono fun x hx y hy => UniformSpace.ball_mono hεU x ?_)⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p : α × α | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
x : α
hx : x ∈ t
y : α
hy : y ∈ closedEBall x ε
⊢ y ∈ UniformSpace.ball x {p : α × α | edist p.1 p.2 ≤ ε}
have hs₁ : ∀ (hy : edist y x ≤ ε), y ∈ UniformSpace.ball x {p : α × α | edist p.1 p.2 ≤ ε}
Tactic: rwa [mem_closedEBall, edist_comm] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p : α × α | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
x : α
hx : x ∈ t
y : α
hy : y ∈ closedEBall x ε
hs₁ : ∀ (hy : edist y x ≤ ε), y ∈ UniformSpace.ball x {p : α × α | edist p.1 p.2 ≤ ε}
⊢ y ∈ UniformSpace.ball x {p : α × α | edist p.1 p.2 ≤ ε}
have hs₂ : ∀ (hy : edist x y ≤ ε), y ∈ UniformSpace.ball x {p : α × α | edist p.1 p.2 ≤ ε}
Tactic: rwa [mem_closedEBall, edist_comm] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
have refine : ∀ (ε : ℝ≥0∞) (hε : ε > 0), ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
Tactic: refine subset_countable_closure_of_almost_dense_set s fun ε hε => ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
have rcases : ∀ (t : Set α) (htf : t.Finite) (hst : s ⊆ ⋃ y ∈ t, eball y ε), ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
Tactic: rcases totallyBounded_iff'.1 hs.totallyBounded ε hε with ⟨t, -, htf, hst⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
⊢ SecondCountableTopology α
have suffices : SeparableSpace α
Tactic: suffices SeparableSpace α by exact UniformSpace.secondCountable_of_separable α
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
⊢ SeparableSpace α
have choose : ∀ (T : (n : ℕ) → Set α),
  (∀ (n : ℕ), T n ⊆ compactCovering α n) →
    ∀ (hTc : ∀ (n : ℕ), (T n).Countable)
      (hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)),
      SeparableSpace α
Tactic: choose T _ hTc hsubT using fun n =>
    subset_countable_closure_of_compact (isCompact_compactCovering α n)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x 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)
⊢ SeparableSpace α
have refine : ∀ (x : α),
  Membership.mem (γ := Set α) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (n : ℕ), T n)) x
Tactic: refine ⟨⟨⋃ n, T n, countable_iUnion hTc, fun x => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
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 : α
⊢ Membership.mem (γ := Set α) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (n : ℕ), T n)) x
have rcases : ∀ (n : ℕ) (hn : x ∈ compactCovering α n),
  Membership.mem (γ := Set α) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (n : ℕ), T n)) x
Tactic: rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering α) x with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
⊢ SecondCountableTopology α
have suffices : SeparableSpace α
Tactic: suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, closedEBall x ε) univ
⊢ SeparableSpace α
have this : ∀ ε > 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
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
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 ε)
⊢ SeparableSpace α
have rcases : ∀ (t : Set α) (htc : t.Countable) (ht : univ ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t),
  SeparableSpace α
Tactic: rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
β : Type v
γ : Type w
inst : EMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : γ → β
⊢ 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 < δ
have 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 < δ
Tactic: rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
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 < δ
⊢ 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 < δ
have 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 < δ
Tactic: rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
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 < δ
⊢ 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 < δ
have 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 < δ
Tactic: rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (goal)
Goal:
γ : Type w
inst : EMetricSpace γ
s : Set γ
hs : IsCompact s
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
have 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
Tactic: rcases subset_countable_closure_of_compact hs with ⟨t, hts, htc, hsub⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Basic (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃₀ c
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, eball x δ ⊆ t
have hc₃ : s ⊆ ⋃ (i : (↑c : Type u)), (↑i : Set α)
Tactic: rw [sUnion_eq_iUnion] at hc₂
Cleared hypotheses: hc₂
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
hs : s.Nonempty
⊢ Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
have obtain : ∀ (x : α) (hx : x ∈ s), Nonempty.{max (u_1 + 1) 1} { u : ℕ → α // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
Tactic: obtain ⟨x, hx⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ 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)))
have 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)))
Tactic: congr 1 with p : 1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 }
⊢ 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)))
have e_s : ∀ (i : ℕ),
  edist (f ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i)) =
    edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i))
Tactic: congr 1 with i : 1
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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 : ℕ
⊢ edist (f ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i)) =
    edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i))
have e_s : 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)]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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))
⊢ edist (f ((↑p.2 : ℕ → α) (i + 1))) (f ((↑p.2 : ℕ → α) i)) =
    edist (f' ((↑p.2 : ℕ → α) (i + 1))) (f' ((↑p.2 : ℕ → α) i))
have e_s₁ : 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)]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ edist (f x) (f' x) = 0
have rw : edist (f' x) (f' x) = 0
Tactic: rw [h xs, edist_self]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ edist (f x) (f' x) = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [h xs, edist_self]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
have inl : ∀ (hnm : n ≤ m), ∑ 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
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
have inr : ∀ (hmn : m ≤ n), ∑ 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
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (hypothesis)
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
⊢ edist (f (u (i + 1))) (f (u i)) = edist (f (v (i + 1))) (f (v i))
have hi₁ : m ≤ i ∧ i < n
Tactic: rw [Finset.mem_Ico] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ 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))
have 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))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
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))
⊢ 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))
have 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
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ 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))
have 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)))
Tactic: apply iSup_le