awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
⊢ ∃ (y : X), Tendsto u atTop (𝓝 y)

Tactic:
CompleteSpace.complete cauchy_u

Premises used: Filter.Tendsto, CompleteSpace.complete
-- 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
obtain : ∀ (y : X) (limy : Tendsto u atTop (𝓝 y)), False
⊢ False

Tactic:
obtain ⟨y, limy⟩ : ∃ y, Tendsto u atTop (𝓝 y) := CompleteSpace.complete cauchy_u

Premises used: CompleteSpace.complete
-- 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_1 : 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (ϕ ∘ u) (n + 1)
this : Tendsto v atTop atTop
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Tendsto (ϕ ∘ u) atTop atTop), Tendsto (ϕ ∘ u) atTop atTop
⊢ Tendsto (ϕ ∘ u) atTop atTop

Tactic:
rwa [tendsto_add_atTop_iff_nat] at this

Premises used: Filter.tendsto_add_atTop_iff_nat
-- 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (ϕ ∘ u) (n + 1)
suffices : Tendsto v atTop atTop
⊢ Tendsto (ϕ ∘ u) atTop atTop

Tactic:
suffices Tendsto v atTop atTop by rwa [tendsto_add_atTop_iff_nat] at 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'
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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (ϕ ∘ u) (n + 1)
⊢ 0 ≤ ϕ x

Tactic:
specialize nonneg 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, _] ϕ
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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (ϕ ∘ u) (n + 1)
nonneg : 0 ≤ ϕ x
⊢ 0 ≤ 2 * ϕ (u 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
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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (ϕ ∘ u) (n + 1)
⊢ 2 * ϕ (u 0) < ϕ (u (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
key₂ 0

Premises used: 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (ϕ ∘ u) (n + 1)
ϕ₁ : 0 ≤ 2 * ϕ (u 0)
⊢ 0 < v 0

Tactic:
calc
        0 ≤ 2 * ϕ (u 0) := by specialize nonneg x; positivity
        _ < ϕ (u (0 + 1)) := key₂ 0

Premises used: 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (ϕ ∘ u) (n + 1)
⊢ 0 < v 0

Tactic:
have hv₀ : 0 < v 0 := by
      calc
        0 ≤ 2 * ϕ (u 0) := by specialize nonneg x; positivity
        _ < ϕ (u (0 + 1)) := key₂ 0
-- 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (ϕ ∘ u) (n + 1)
hv₀ : 0 < v 0
apply : ∀ (n : ℕ), 2 * v n ≤ v (n + 1)
⊢ Tendsto v atTop atTop

Tactic:
apply tendsto_atTop_of_geom_le hv₀ one_lt_two

Premises used: one_lt_two, tendsto_atTop_of_geom_le
-- 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (ϕ ∘ u) (n + 1)
hv₀ : 0 < v 0
⊢ ∀ (n : ℕ), 2 * v n ≤ v (n + 1)

Tactic:
fun n => (key₂ (n + 1)).le

Premises used: LT.lt.le, 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : (n : ℕ) → ℝ := fun (n : ℕ) ↦ (ϕ ∘ u) (n + 1)
hv₀ : 0 < v 0
⊢ ∀ (n : ℕ), 2 * v n ≤ v (n + 1)

Tactic:
exact fun n => (key₂ (n + 1)).le

Premises used: LT.lt.le, 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
⊢ Tendsto (ϕ ∘ u) atTop atTop

Tactic:
have lim_top : Tendsto (ϕ ∘ u) atTop atTop := by
    let v n := (ϕ ∘ u) (n + 1)
    suffices Tendsto v atTop atTop by rwa [tendsto_add_atTop_iff_nat] at this
    have hv₀ : 0 < v 0 := by
      calc
        0 ≤ 2 * ϕ (u 0) := by specialize nonneg x; positivity
        _ < ϕ (u (0 + 1)) := key₂ 0
    apply tendsto_atTop_of_geom_le hv₀ one_lt_two
    exact fun n => (key₂ (n + 1)).le
-- 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
lim_top : Tendsto (ϕ ∘ u) atTop atTop
⊢ Tendsto (ϕ ∘ u) atTop (𝓝 (ϕ y))

Tactic:
have lim : Tendsto (ϕ ∘ u) atTop (𝓝 (ϕ y)) := Tendsto.comp cont.continuousAt limy
-- 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
lim_top : Tendsto (ϕ ∘ u) atTop atTop
lim : Tendsto (ϕ ∘ u) atTop (𝓝 (ϕ y))
⊢ False

Tactic:
not_tendsto_atTop_of_tendsto_nhds lim lim_top

Premises used: not_tendsto_atTop_of_tendsto_nhds
-- 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))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / HPow.hPow (α := ℝ) 2 x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
lim_top : Tendsto (ϕ ∘ u) atTop atTop
lim : Tendsto (ϕ ∘ u) atTop (𝓝 (ϕ y))
⊢ False

Tactic:
exact not_tendsto_atTop_of_tendsto_nhds lim lim_top

Premises used: not_tendsto_atTop_of_tendsto_nhds
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
A : E →L[𝕜] F
x : F
⊢ Eq.{u_2 + 1} (α := E) ((((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) x : E)
    ((LinearIsometryEquiv.symm (toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E)
        ((((toSesqForm : (a : E →L[𝕜] F) → F →L⋆[𝕜] E →L[𝕜] 𝕜) A : F →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : F) → E →L[𝕜] 𝕜) x :
          E →L[𝕜] 𝕜) :
      E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
A : E →L[𝕜] F
x : E
y : F
rw :
  ⟪(LinearIsometryEquiv.symm (toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E)
        ((((toSesqForm : (a : E →L[𝕜] F) → F →L⋆[𝕜] E →L[𝕜] 𝕜) A : F →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : F) → E →L[𝕜] 𝕜) y :
          E →L[𝕜] 𝕜),
      x⟫_𝕜 =
    ⟪y, (A : (a : E) → F) x⟫_𝕜
rw₁ :
  (((((toSesqForm : (a : E →L[𝕜] F) → F →L⋆[𝕜] E →L[𝕜] 𝕜) A : F →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : F) → E →L[𝕜] 𝕜) y :
          E →L[𝕜] 𝕜) :
        (a : E) → 𝕜)
      x =
    ⟪y, (A : (a : E) → F) x⟫_𝕜
rw₂ : (comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y) A : (a : E) → 𝕜) x = ⟪y, (A : (a : E) → F) x⟫_𝕜
rw₃ :
  Function.comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := F) (⇑((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y : F →L[𝕜] 𝕜) : (a : F) → 𝕜)
      (⇑A : (a : E) → F) x =
    ⟪y, (A : (a : E) → F) x⟫_𝕜
rw₄ : ((fun (w : F) ↦ ⟪y, w⟫_𝕜) ∘ (⇑A : (a : E) → F)) x = ⟪y, (A : (a : E) → F) x⟫_𝕜
rw₅ rw₆ : ⟪y, (A : (a : E) → F) x⟫_𝕜 = ⟪y, (A : (a : E) → F) x⟫_𝕜
⊢ ⟪(((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) y, x⟫_𝕜 = ⟪y, (A : (a : E) → F) x⟫_𝕜

Tactic:
rw [adjointAux_apply, toDual_symm_apply, toSesqForm_apply_coe, coe_comp', coe_innerSL_apply,
    Function.comp_apply]

Premises used: ContinuousLinearMap.coe_comp', InnerProductSpace.toDual_symm_apply, ContinuousLinearMap.toSesqForm_apply_coe, coe_innerSL_apply, ContinuousLinearMap.adjointAux_apply, Function.comp_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
A : E →L[𝕜] F
x : E
y : F
rw :
  (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) y, x⟫_𝕜 =
    ⟪(A : (a : E) → F) x, y⟫_𝕜
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, (A : (a : E) → F) x⟫_𝕜 = ⟪(A : (a : E) → F) x, y⟫_𝕜
rw₂ rw₃ : ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪(A : (a : E) → F) x, y⟫_𝕜
⊢ ⟪x, (((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) y⟫_𝕜 = ⟪(A : (a : E) → F) x, y⟫_𝕜

Tactic:
rw [← inner_conj_symm, adjointAux_inner_left, inner_conj_symm]

Premises used: ContinuousLinearMap.adjointAux_inner_left, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
h :
  ∀ (v : E),
    Eq.{u_3 + 1} (α := F)
      ((((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) :
            (a : E) → F)
          v :
        F)
      ((A : (a : E) → F) v : F)
⊢ (adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) = A

Tactic:
ext v