awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
choose :
  ∀ (F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ) (hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3)
    (hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖),
    ∃ (g : Y →ᵇ ℝ), ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ = ‖f‖ ∧ g.compContinuous e = f

Tactic:
choose F hF_norm hF_dist using fun f : X →ᵇ ℝ => tietze_extension_step f e he

Premises used: BoundedContinuousFunction.tietze_extension_step
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
⊢ g 0 = 0

Tactic:
have g0 : g 0 = 0 := rfl
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
⊢ ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)

Tactic:
have g_succ : ∀ n, g (n + 1) = g n + F (f - (g n).compContinuous e) := fun n =>
    Function.iterate_succ_apply' _ _ _
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
⊢ dist ((g 0).compContinuous e) f ≤ HPow.hPow (β := ℕ) (2 / 3) 0 * ‖f‖

Tactic:
simp [g0]
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
succ :
  dist ((F (f - (g n).compContinuous e)).compContinuous e) (f - (g n).compContinuous e) ≤ 2 / 3 * ((2 / 3) ^ n * ‖f‖)
⊢ dist ((g (n + 1)).compContinuous e) f ≤ (2 / 3) ^ (n + 1) * ‖f‖

Tactic:
rw [g_succ n, add_compContinuous, ← dist_sub_right, add_sub_cancel_left, pow_succ', mul_assoc]

Premises used: dist_sub_right, add_sub_cancel_left, mul_assoc, pow_succ', BoundedContinuousFunction.add_compContinuous
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ 0 ≤ 2 / 3

Tactic:
norm_num1
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
succ : ‖f - (g n).compContinuous e‖ ≤ (2 / 3) ^ n * ‖f‖
⊢ dist ((F (f - (g n).compContinuous e)).compContinuous e) (f - (g n).compContinuous e) ≤ 2 / 3 * ((2 / 3) ^ n * ‖f‖)

Tactic:
refine (hF_dist _).trans (mul_le_mul_of_nonneg_left ?_ (by norm_num1))

Premises used: LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
succ succ₁ succ₂ succ₃ : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ ‖f - (g n).compContinuous e‖ ≤ (2 / 3) ^ n * ‖f‖

Tactic:
rwa [← dist_eq_norm']

Premises used: dist_eq_norm'
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
zero : dist ((g 0).compContinuous e) f ≤ HPow.hPow (β := ℕ) (2 / 3) 0 * ‖f‖
succ :
  ∀ (n : ℕ) (ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖),
    dist ((g (n + 1)).compContinuous e) f ≤ (2 / 3) ^ (n + 1) * ‖f‖
⊢ dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖

Tactic:
induction n with
    | zero => simp [g0]
    | succ n ihn =>
      rw [g_succ n, add_compContinuous, ← dist_sub_right, add_sub_cancel_left, pow_succ', mul_assoc]
      refine (hF_dist _).trans (mul_le_mul_of_nonneg_left ?_ (by norm_num1))
      rwa [← dist_eq_norm']

Premises used: dist_sub_right, add_sub_cancel_left, mul_assoc, dist_eq_norm', LE.le.trans, mul_le_mul_of_nonneg_left, pow_succ', BoundedContinuousFunction.add_compContinuous
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
⊢ ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖

Tactic:
have hgf : ∀ n, dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖ := by
    intro n
    induction n with
    | zero => simp [g0]
    | succ n ihn =>
      rw [g_succ n, add_compContinuous, ← dist_sub_right, add_sub_cancel_left, pow_succ', mul_assoc]
      refine (hF_dist _).trans (mul_le_mul_of_nonneg_left ?_ (by norm_num1))
      rwa [← dist_eq_norm']
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
rw : dist (g n) (g n + F (f - (g n).compContinuous e)) = ‖F (f - (g n).compContinuous e)‖
rw₁ : ‖g n + F (f - (g n).compContinuous e) - g n‖ = ‖F (f - (g n).compContinuous e)‖
rw₂ rw₃ : ‖F (f - (g n).compContinuous e)‖ = ‖F (f - (g n).compContinuous e)‖
⊢ dist (g n) (g (n + 1)) = ‖F (f - (g n).compContinuous e)‖

Tactic:
rw [g_succ, dist_eq_norm', add_sub_cancel_left]

Premises used: add_sub_cancel_left, dist_eq_norm'
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ ‖F (f - (g n).compContinuous e)‖ ≤ ‖f - (g n).compContinuous e‖ / 3

Tactic:
hF_norm _
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
rw : ‖f - (g n).compContinuous e‖ / 3 = 1 / 3 * ‖f - (g n).compContinuous e‖
rw₁ : ‖f - (g n).compContinuous e‖ / 3 = 3⁻¹ * ‖f - (g n).compContinuous e‖
rw₂ rw₃ : 3⁻¹ * ‖f - (g n).compContinuous e‖ = 3⁻¹ * ‖f - (g n).compContinuous e‖
⊢ ‖f - (g n).compContinuous e‖ / 3 = 1 / 3 * dist ((g n).compContinuous e) f

Tactic:
rw [dist_eq_norm', one_div, div_eq_inv_mul]

Premises used: dist_eq_norm', one_div, div_eq_inv_mul
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ 0 ≤ 1 / 3

Tactic:
norm_num1
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ 1 / 3 * ((2 / 3) ^ n * ‖f‖) = 1 / 3 * ‖f‖ * (2 / 3) ^ n

Tactic:
ac_rfl
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), Dist.dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), Dist.dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
dist : Dist.dist (g n) (g (n + 1)) = ‖F (f - (g n).compContinuous e)‖
dist₁ : ‖f - (g n).compContinuous e‖ / 3 = 1 / 3 * Dist.dist ((g n).compContinuous e) f
dist₂ : 1 / 3 * ((2 / 3) ^ n * ‖f‖) = 1 / 3 * ‖f‖ * (2 / 3) ^ n
⊢ Dist.dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n

Tactic:
calc
      dist (g n) (g (n + 1)) = ‖F (f - (g n).compContinuous e)‖ := by
        rw [g_succ, dist_eq_norm', add_sub_cancel_left]
      _ ≤ ‖f - (g n).compContinuous e‖ / 3 := hF_norm _
      _ = 1 / 3 * dist ((g n).compContinuous e) f := by rw [dist_eq_norm', one_div, div_eq_inv_mul]
      _ ≤ 1 / 3 * ((2 / 3) ^ n * ‖f‖) := mul_le_mul_of_nonneg_left (hgf n) (by norm_num1)
      _ = 1 / 3 * ‖f‖ * (2 / 3) ^ n := by ac_rfl

Premises used: Norm.norm, HMul.hMul, HSub.hSub, HDiv.hDiv, BoundedContinuousFunction.compContinuous, HPow.hPow, HAdd.hAdd, Dist.dist, OfNat.ofNat, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n

Tactic:
have hg_dist : ∀ n, dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n := by
    intro n
    calc
      dist (g n) (g (n + 1)) = ‖F (f - (g n).compContinuous e)‖ := by
        rw [g_succ, dist_eq_norm', add_sub_cancel_left]
      _ ≤ ‖f - (g n).compContinuous e‖ / 3 := hF_norm _
      _ = 1 / 3 * dist ((g n).compContinuous e) f := by rw [dist_eq_norm', one_div, div_eq_inv_mul]
      _ ≤ 1 / 3 * ((2 / 3) ^ n * ‖f‖) := mul_le_mul_of_nonneg_left (hgf n) (by norm_num1)
      _ = 1 / 3 * ‖f‖ * (2 / 3) ^ n := by ac_rfl
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
⊢ 2 / 3 < 1

Tactic:
norm_num1
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
⊢ CauchySeq g

Tactic:
have hg_cau : CauchySeq g := cauchySeq_of_le_geometric _ _ (by norm_num1) hg_dist
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
⊢ Tendsto (fun (n : ℕ) ↦ (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))

Tactic:
have :
    Tendsto (fun n => (g n).compContinuous e) atTop
      (𝓝 <| (limUnder atTop g).compContinuous e) :=
    ((continuous_compContinuous e).tendsto _).comp hg_cau.tendsto_limUnder
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun (n : ℕ) ↦ (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))
⊢ (limUnder atTop g).compContinuous e = f

Tactic:
tendsto_nhds_unique this (tendsto_iff_dist_tendsto_zero.2 ?_)

Premises used: Iff.mpr, tendsto_iff_dist_tendsto_zero, tendsto_nhds_unique
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun (n : ℕ) ↦ (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))
refine : Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist ((g b).compContinuous e) f) atTop (𝓝 0)
⊢ (limUnder atTop g).compContinuous e = f

Tactic:
refine tendsto_nhds_unique this (tendsto_iff_dist_tendsto_zero.2 ?_)

Premises used: Iff.mpr, tendsto_iff_dist_tendsto_zero, tendsto_nhds_unique
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun (n : ℕ) ↦ (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))
⊢ Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist ((g b).compContinuous e) f) atTop (𝓝 0)

Tactic:
squeeze_zero (fun _ => dist_nonneg) hgf ?_

Premises used: squeeze_zero, dist_nonneg
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun (n : ℕ) ↦ (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))
refine : Tendsto (β := ℝ) (fun (t : ℕ) ↦ (2 / 3) ^ t * ‖f‖) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist ((g b).compContinuous e) f) atTop (𝓝 0)

Tactic:
refine squeeze_zero (fun _ => dist_nonneg) hgf ?_

Premises used: squeeze_zero, dist_nonneg
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun (n : ℕ) ↦ (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))
rw : Tendsto (fun (t : ℕ) ↦ (2 / 3) ^ t * ‖f‖) atTop (𝓝 (0 * ‖f‖))
⊢ Tendsto (β := ℝ) (fun (t : ℕ) ↦ (2 / 3) ^ t * ‖f‖) atTop (𝓝 0)

Tactic:
rw [← zero_mul ‖f‖]

Premises used: Norm.norm, MulZeroClass.zero_mul
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
F : (f : X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun (n : ℕ) ↦ (fun (g : Y →ᵇ ℝ) ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun (n : ℕ) ↦ (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))
⊢ Tendsto (fun (t : ℕ) ↦ (2 / 3) ^ t * ‖f‖) atTop (𝓝 (0 * ‖f‖))

Tactic:
(tendsto_pow_atTop_nhds_zero_of_lt_one ?_ ?_).mul tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.mul, tendsto_pow_atTop_nhds_zero_of_lt_one