awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hpq : (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
⊢ (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ * (↑t : ℝ≥0∞) =
    (↑(ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑(p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹)⁻¹ : ℝ))) :
          ℝ≥0∞) *
        (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) *
      eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
ring
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hpq : (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑q : ℝ)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E) : ℝ≥0)⁻¹)⁻¹
hp' : (↑p'⁻¹ : ℝ) = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
this : (↑q : ℝ≥0∞) ≤ (↑p' : ℝ≥0∞)
t : ℝ≥0 := ENNReal.toNNReal ((μ : (a : Set E) → ℝ≥0∞) s) ^ (1 / (↑q : ℝ) - 1 / (↑p' : ℝ))
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)
calc : eLpNorm u (↑q : ℝ≥0∞) μ = eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s)
calc₁ : eLpNorm u (↑q : ℝ≥0∞) (μ.restrict s) ≤ eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞)
calc₂ : eLpNorm u (↑p' : ℝ≥0∞) (μ.restrict s) * (↑t : ℝ≥0∞) = eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
calc₃ :
  eLpNorm u (↑p' : ℝ≥0∞) μ * (↑t : ℝ≥0∞) ≤
    (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ * (↑t : ℝ≥0∞)
calc₄ :
  (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ * (↑t : ℝ≥0∞) =
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
⊢ eLpNorm u (↑q : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p q) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
calc eLpNorm u q μ
      = eLpNorm u q (μ.restrict s) := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ eLpNorm u p' (μ.restrict s) * t := by
        convert! eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
        rw [ENNReal.coe_rpow_of_nonneg]
        · simp [ENNReal.coe_toNNReal hs.measure_lt_top.ne]
        · rw [one_div, one_div]
          norm_cast
          rw [hp']
          simpa using hpq
    _ = eLpNorm u p' μ * t := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
    _ ≤ (C * eLpNorm (fderiv ℝ u) p μ) * t := by
        have h2u' : HasCompactSupport u := by
          apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
          exact h2u.trans subset_closure
        rel [eLpNorm_le_eLpNorm_fderiv_of_eq μ hu h2u' hp (mod_cast h2p.pos) hp']
    _ = eLpNormLESNormFDerivOfLeConst F μ s p q * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]; ring

Premises used: Real, ENNReal.ofNNReal, HMul.hMul, MeasureTheory.Measure.restrict, fderiv, MeasureTheory.eLpNormLESNormFDerivOfLeConst, MeasureTheory.eLpNorm
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hs : Bornology.IsBounded s
⊢ eLpNorm u (↑p : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p p) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
eLpNorm_le_eLpNorm_fderiv_of_le μ hu h2u hp h2p ?_ hs

Premises used: MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_le
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hs : Bornology.IsBounded s
refine : (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑p : ℝ)⁻¹
⊢ eLpNorm u (↑p : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfLeConst F μ s p p) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ

Tactic:
refine eLpNorm_le_eLpNorm_fderiv_of_le μ hu h2u hp h2p ?_ hs

Premises used: MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_le
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hs : Bornology.IsBounded s
simp : LE.le (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)⁻¹
⊢ (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹ ≤ (↑p⁻¹ : ℝ)

Tactic:
simp only [tsub_le_iff_right, le_add_iff_nonneg_right]

Premises used: le_add_iff_nonneg_right, tsub_le_iff_right
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
inst_8 : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p : ℝ≥0
hp : 1 ≤ p
h2p : p < (↑(finrank ℝ E) : ℝ≥0)
hs : Bornology.IsBounded s
⊢ LE.le (α := ℝ) 0 (↑(finrank ℝ E) : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
by_contra! :
  ∀
    (H :
      ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
        ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y),
    False
⊢ ∃ ε' > 0, ∃ (x' : X), ε' ≤ ε ∧ d x' x ≤ 2 * ε ∧ ε * ϕ x ≤ ε' * ϕ x' ∧ ∀ (y : X), d x' y ≤ ε' → ϕ y ≤ 2 * ϕ x'

Tactic:
by_contra! H
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H :
  ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
    ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
rw : 0 < HPow.hPow (α := ℝ) 2 k
⊢ ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'

Tactic:
rw [div_mul_eq_mul_div, le_div_iff₀, mul_assoc, mul_le_mul_iff_right₀ ε_pos, mul_comm]

Premises used: mul_assoc, div_mul_eq_mul_div, mul_comm, le_div_iff₀, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H :
  ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
    ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ 0 < HPow.hPow (α := ℝ) 2 k

Tactic:
positivity
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H :
  ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
    ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
⊢ ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'

Tactic:
have reformulation : ∀ (x') (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x' := by
    intro x' k
    rw [div_mul_eq_mul_div, le_div_iff₀, mul_assoc, mul_le_mul_iff_right₀ ε_pos, mul_comm]
    positivity
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H :
  ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
    ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
k : ℕ
x' : X
⊢ ε / HPow.hPow (α := ℝ) 2 k > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H :
  ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
    ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
k : ℕ
x' : X
⊢ ∀ (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x'),
    ∃ (y : X), d x' y ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ y

Tactic:
have := H (ε / 2 ^ k) (by positivity) x' (div_le_self ε_pos.le <| one_le_pow₀ one_le_two)
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H :
  ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
    ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
k : ℕ
x' : X
this :
  ∀ (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x'),
    ∃ (y : X), d x' y ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ y
⊢ d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' → ∃ (y : X), d x' y ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ y

Tactic:
simpa [reformulation] using this
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H :
  ∀ (ε' : ℝ) (_ : ε' > 0) (x' : X) (_ : ε' ≤ ε) (_ : d x' x ≤ 2 * ε) (_ : ε * ϕ x ≤ ε' * ϕ x'),
    ∃ (y : X), d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
⊢ ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      ∃ (y : X), d x' y ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ y

Tactic:
replace H : ∀ k : ℕ, ∀ x', d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' →
      ∃ y, d x' y ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ y := by
    intro k x'
    have := H (ε / 2 ^ k) (by positivity) x' (div_le_self ε_pos.le <| one_le_pow₀ one_le_two)
    simpa [reformulation] using this
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
H :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      ∃ (y : X), d x' y ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ y
⊢ Nonempty X

Tactic:
haveI : Nonempty X := ⟨x⟩
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
H :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      ∃ (y : X), d x' y ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ y
this : Nonempty X
choose! :
  ∀ (F : (k : ℕ) → (x' : X) → X)
    (hF :
      ∀ (k : ℕ) (x' : X),
        d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
          d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')),
    False
⊢ False

Tactic:
choose! F hF using H
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
this : Nonempty X
F : (k : ℕ) → (x' : X) → X
hF :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ X) n x F
⊢ ∀ (n : ℕ),
    d (u n) x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 n * ϕ x ≤ ϕ (u n) →
      d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))

Tactic:
fun n ↦ hF n (u n)
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
this : Nonempty X
F : (k : ℕ) → (x' : X) → X
hF :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ X) n x F
⊢ ∀ (n : ℕ),
    d (u n) x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 n * ϕ x ≤ ϕ (u n) →
      d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))

Tactic:
exact fun n ↦ hF n (u n)
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
this : Nonempty X
F : (k : ℕ) → (x' : X) → X
hF :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ X) n x F
⊢ ∀ (n : ℕ),
    d (u n) x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 n * ϕ x ≤ ϕ (u n) →
      d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))

Tactic:
have hu :
    ∀ n,
      d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) →
        d (u n) (u <| n + 1) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u <| n + 1) := by
    exact fun n ↦ hF n (u n)
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
this : Nonempty X
F : (k : ℕ) → (x' : X) → X
hF :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ X) n x F
hu :
  ∀ (n : ℕ),
    d (u n) x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 n * ϕ x ≤ ϕ (u n) →
      d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
⊢ d (u 0) (u (HAdd.hAdd (α := ℕ) 0 1)) ≤ ε / HPow.hPow (α := ℝ) (β := ℕ) 2 0 ∧
    2 * ϕ (u 0) < ϕ (u (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
simpa [u, ε_pos.le] using hu 0

Premises used: LT.lt.le, OfNat.ofNat
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
this : Nonempty X
F : (k : ℕ) → (x' : X) → X
hF :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ X) n x F
hu :
  ∀ (n : ℕ),
    d (u n) x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 n * ϕ x ≤ ϕ (u n) →
      d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
rw : d x (u (n + 1)) ≤ 2 * ε
⊢ d (u (n + 1)) x ≤ 2 * ε

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
this : Nonempty X
F : (k : ℕ) → (x' : X) → X
hF :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ X) n x F
hu :
  ∀ (n : ℕ),
    d (u n) x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 n * ϕ x ≤ ϕ (u n) →
      d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
r : Finset ℕ := range (n + 1)
⊢ d (u 0) (u (n + 1)) ≤ ∑ i ∈ r, d (u i) (u (i + 1))

Tactic:
dist_le_range_sum_dist u (n + 1)

Premises used: dist_le_range_sum_dist, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
this : Nonempty X
F : (k : ℕ) → (x' : X) → X
hF :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ X) n x F
hu :
  ∀ (n : ℕ),
    d (u n) x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 n * ϕ x ≤ ϕ (u n) →
      d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
r : Finset ℕ := range (n + 1)
⊢ LE.le (α := ℝ) (∑ i ∈ r, d (u i) (u (i + 1))) (∑ i ∈ r, ε / HPow.hPow (α := ℝ) 2 i)

Tactic:
(sum_le_sum fun i i_in => (IH i <| Nat.lt_succ_iff.mp <| Finset.mem_range.mp i_in).1)

Premises used: Finset.mem_range, Nat.lt_succ_iff, And.left, Iff.mp, Finset.sum_le_sum
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
this : Nonempty X
F : (k : ℕ) → (x' : X) → X
hF :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ X) n x F
hu :
  ∀ (n : ℕ),
    d (u n) x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 n * ϕ x ≤ ϕ (u n) →
      d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
r : Finset ℕ := range (n + 1)
rw : Eq (α := ℝ) (∑ i ∈ r, ε / HPow.hPow (α := ℝ) 2 i) (∑ i ∈ r, (1 / 2) ^ i * ε)
⊢ ∑ i ∈ r, ε / HPow.hPow (α := ℝ) 2 i = (∑ i ∈ r, (1 / 2) ^ i) * ε

Tactic:
rw [Finset.sum_mul]

Premises used: Finset.sum_mul
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
this : Nonempty X
F : (k : ℕ) → (x' : X) → X
hF :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ X) n x F
hu :
  ∀ (n : ℕ),
    d (u n) x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 n * ϕ x ≤ ϕ (u n) →
      d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
r : Finset ℕ := range (n + 1)
simp : Eq (α := ℝ) (∑ i ∈ r, ε / HPow.hPow (α := ℝ) 2 i) (∑ x ∈ r, (HPow.hPow (α := ℝ) 2 x)⁻¹ * ε)
⊢ Eq (α := ℝ) (∑ i ∈ r, ε / HPow.hPow (α := ℝ) 2 i) (∑ i ∈ r, (1 / 2) ^ i * ε)

Tactic:
simp
-- Module: Mathlib.Analysis.Hofer
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / HPow.hPow (α := ℝ) 2 k * ϕ x' ↔ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x'
this : Nonempty X
F : (k : ℕ) → (x' : X) → X
hF :
  ∀ (k : ℕ) (x' : X),
    d x' x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 k * ϕ x ≤ ϕ x' →
      d x' (F k x') ≤ ε / HPow.hPow (α := ℝ) 2 k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ X) n x F
hu :
  ∀ (n : ℕ),
    d (u n) x ≤ 2 * ε ∧ HPow.hPow (α := ℝ) 2 n * ϕ x ≤ ϕ (u n) →
      d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
r : Finset ℕ := range (n + 1)
⊢ Eq (α := ℝ) (∑ i ∈ r, ε / HPow.hPow (α := ℝ) 2 i) (∑ x ∈ r, (HPow.hPow (α := ℝ) 2 x)⁻¹ * ε)

Tactic:
field_simp