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)
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_1 : 0 ≤ 2 / 3
refine_2 : 2 / 3 < 1
⊢ Tendsto (fun (t : ℕ) ↦ (2 / 3) ^ t * ‖f‖) atTop (𝓝 (0 * ‖f‖))

Tactic:
refine (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
-- 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))
⊢ 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)
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))
⊢ 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
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:
have hge : (limUnder atTop g).compContinuous e = f := by
    refine tendsto_nhds_unique this (tendsto_iff_dist_tendsto_zero.2 ?_)
    refine squeeze_zero (fun _ => dist_nonneg) hgf ?_
    rw [← zero_mul ‖f‖]
    refine (tendsto_pow_atTop_nhds_zero_of_lt_one ?_ ?_).mul tendsto_const_nhds <;> 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
hg_cau : CauchySeq g
this : Tendsto (fun (n : ℕ) ↦ (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))
hge : (limUnder atTop g).compContinuous e = f
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ = ‖f‖ ∧ g.compContinuous e = f

Tactic:
⟨limUnder atTop g, le_antisymm ?_ ?_, hge⟩

Premises used: Filter.atTop, le_antisymm, And.intro, Exists.intro, Filter.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))
hge : (limUnder atTop g).compContinuous e = f
refine_1 : ‖limUnder atTop g‖ ≤ ‖f‖
refine_2 : ‖f‖ ≤ ‖limUnder atTop g‖
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ = ‖f‖ ∧ g.compContinuous e = f

Tactic:
refine ⟨limUnder atTop g, le_antisymm ?_ ?_, hge⟩
-- 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))
hge : (limUnder atTop g).compContinuous e = f
refine_1 : dist (g 0) (limUnder atTop g) ≤ ‖f‖
⊢ ‖limUnder atTop g‖ ≤ ‖f‖

Tactic:
rw [← dist_zero_left, ← g0]

Premises used: dist_zero_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‖
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))
hge : (limUnder atTop g).compContinuous e = f
⊢ 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
hg_cau : CauchySeq g
this : Tendsto (fun (n : ℕ) ↦ (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))
hge : (limUnder atTop g).compContinuous e = f
refine_1 : 1 / 3 * ‖f‖ / (1 - 2 / 3) = ‖f‖
⊢ dist (g 0) (limUnder atTop g) ≤ ‖f‖

Tactic:
refine
      (dist_le_of_le_geometric_of_tendsto₀ _ _ (by norm_num1)
        hg_dist hg_cau.tendsto_limUnder).trans_eq ?_

Premises used: LE.le.trans_eq, dist_le_of_le_geometric_of_tendsto₀, CauchySeq.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))
hge : (limUnder atTop g).compContinuous e = f
⊢ 1 / 3 * ‖f‖ / (1 - 2 / 3) = ‖f‖

Tactic:
ring
-- 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))
hge : (limUnder atTop g).compContinuous e = f
refine_2 : ‖(limUnder atTop g).compContinuous e‖ ≤ ‖limUnder atTop g‖
⊢ ‖f‖ ≤ ‖limUnder atTop g‖

Tactic:
rw [← hge]
-- 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))
hge : (limUnder atTop g).compContinuous e = f
⊢ ‖(limUnder atTop g).compContinuous e‖ ≤ ‖limUnder atTop g‖

Tactic:
norm_compContinuous_le _ _

Premises used: BoundedContinuousFunction.norm_compContinuous_le, setOf
-- 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))
hge : (limUnder atTop g).compContinuous e = f
⊢ ‖(limUnder atTop g).compContinuous e‖ ≤ ‖limUnder atTop g‖

Tactic:
exact norm_compContinuous_le _ _

Premises used: BoundedContinuousFunction.norm_compContinuous_le
-- 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 : X → Y
he : IsClosedEmbedding e
rcases :
  ∀ (g : Y →ᵇ ℝ) (hg : ‖g‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ : C(X, Y) }‖),
    ∃ (g_1 : Y →ᵇ ℝ),
      ‖g_1‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ : C(X, Y) }‖ ∧
        Eq (α := X → ℝ) ((⇑g_1 : (a : Y) → ℝ) ∘ e)
          (⇑(g.compContinuous { toFun := e, continuous_toFun := ⋯ : C(X, Y) }) : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ = ‖f‖ ∧ Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
rcases exists_extension_norm_eq_of_isClosedEmbedding' f ⟨e, he.continuous⟩ he with ⟨g, hg, rfl⟩

Premises used: ContinuousMap.mk, Topology.IsClosedEmbedding.continuous, rfl, BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding'
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
e : X → Y
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hg : ‖g‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ : C(X, Y) }‖
⊢ ∃ (g_1 : Y →ᵇ ℝ),
    ‖g_1‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ : C(X, Y) }‖ ∧
      Eq (α := X → ℝ) ((⇑g_1 : (a : Y) → ℝ) ∘ e)
        (⇑(g.compContinuous { toFun := e, continuous_toFun := ⋯ : C(X, Y) }) : (a : X) → ℝ)

Tactic:
⟨g, hg, rfl⟩

Premises used: And.intro, Exists.intro, 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
e : X → Y
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hg : ‖g‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ : C(X, Y) }‖
⊢ ∃ (g_1 : Y →ᵇ ℝ),
    ‖g_1‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ : C(X, Y) }‖ ∧
      Eq (α := X → ℝ) ((⇑g_1 : (a : Y) → ℝ) ∘ e)
        (⇑(g.compContinuous { toFun := e, continuous_toFun := ⋯ : C(X, Y) }) : (a : X) → ℝ)

Tactic:
exact ⟨g, hg, rfl⟩
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type u_2
inst : TopologicalSpace Y
inst_1 : NormalSpace Y
s : Set Y
f : (↑s : Type u_2) →ᵇ ℝ
hs : IsClosed[inst] s
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ = ‖f‖ ∧ g.restrict s = f

Tactic:
exists_extension_norm_eq_of_isClosedEmbedding' f ((ContinuousMap.id _).restrict s)
    hs.isClosedEmbedding_subtypeVal

Premises used: ContinuousMap.id, IsClosed.isClosedEmbedding_subtypeVal, ContinuousMap.restrict, BoundedContinuousFunction.restrict, BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding'
-- 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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
rcases :
  ∀ (g : Y →ᵇ ℝ) (hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖)
    (hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)),
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
rcases exists_extension_norm_eq_of_isClosedEmbedding (f - const X ((a + b) / 2)) he with
    ⟨g, hgf, hge⟩

Premises used: BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding, HSub.hSub, HDiv.hDiv, BoundedContinuousFunction.const, HAdd.hAdd, OfNat.ofNat
-- 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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
⟨const Y ((a + b) / 2) + g, fun y => ?_, ?_⟩

Premises used: HDiv.hDiv, BoundedContinuousFunction.const, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- 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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)
refine_1 : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((const Y ((a + b) / 2) + g : (a : Y) → ℝ) y : ℝ)
refine_2 : Eq (α := X → ℝ) ((⇑(const Y ((a + b) / 2) + g) : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
refine ⟨const Y ((a + b) / 2) + g, fun y => ?_, ?_⟩
-- 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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)
y : Y
this : ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2
⊢ Membership.mem (α := ℝ) (Icc a b) ((const Y ((a + b) / 2) + g : (a : Y) → ℝ) y : ℝ)

Tactic:
simpa [Real.Icc_eq_closedBall, add_mem_closedBall_iff_norm] using
        (norm_coe_le_norm g y).trans (hgf.trans_le this)

Premises used: Eq.trans_le, add_mem_closedBall_iff_norm, BoundedContinuousFunction.norm_coe_le_norm, LE.le.trans, Real.Icc_eq_closedBall
-- 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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)
y : Y
refine_1 : ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2
⊢ Membership.mem (α := ℝ) (Icc a b) ((const Y ((a + b) / 2) + g : (a : Y) → ℝ) y : ℝ)

Tactic:
suffices ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2 by
      simpa [Real.Icc_eq_closedBall, add_mem_closedBall_iff_norm] using
        (norm_coe_le_norm g y).trans (hgf.trans_le this)
-- 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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)
y : Y
⊢ ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2

Tactic:
(norm_le <| div_nonneg (sub_nonneg.2 hle) zero_le_two).2 fun x => ?_

Premises used: Iff.mpr, BoundedContinuousFunction.norm_le, zero_le_two, div_nonneg, sub_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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)
y : Y
refine_1 : ∀ (x : X), norm (E := ℝ) ((f - const X ((a + b) / 2) : (a : X) → ℝ) x : ℝ) ≤ (b - a) / 2
⊢ ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2

Tactic:
refine (norm_le <| div_nonneg (sub_nonneg.2 hle) zero_le_two).2 fun x => ?_

Premises used: Iff.mpr, BoundedContinuousFunction.norm_le, zero_le_two, div_nonneg, sub_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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)
y : Y
x : X
⊢ norm (E := ℝ) ((f - const X ((a + b) / 2) : (a : X) → ℝ) x : ℝ) ≤ (b - a) / 2

Tactic:
simpa only [Real.Icc_eq_closedBall] using hf x

Premises used: Real.Icc_eq_closedBall
-- 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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)
refine_2 : ∀ (x : X), Eq (α := ℝ) (((⇑(const Y ((a + b) / 2) + g) : (a : Y) → ℝ) ∘ e) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ Eq (α := X → ℝ) ((⇑(const Y ((a + b) / 2) + g) : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
ext x
-- 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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)
x : X
⊢ (g : (a : Y) → ℝ) (e x) = HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((a + b) / 2)

Tactic:
have : g (e x) = f x - (a + b) / 2 := congr_fun hge x
-- 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 →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑(f - const X ((a + b) / 2)) : (a : X) → ℝ)
x : X
this : (g : (a : Y) → ℝ) (e x) = HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((a + b) / 2)
⊢ Eq (α := ℝ) (((⇑(const Y ((a + b) / 2) + g) : (a : Y) → ℝ) ∘ e) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
simp [this]