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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : (f : (a : X) → ℝ) x ≤ -‖f‖ / 3
rw :
  |HSub.hSub (β := ℝ) (Function.const.{1, u_2 + 1} Y (-‖f‖ / 3) ((e : (a : X) → Y) x : Y)) ((f : (a : X) → ℝ) x : ℝ)| =
    HSub.hSub (β := ℝ) (-‖f‖ / 3) ((f : (a : X) → ℝ) x : ℝ)
rw₁ :
  |HSub.hSub (β := ℝ) (-‖f‖ / 3) ((f : (a : X) → ℝ) x : ℝ)| = HSub.hSub (β := ℝ) (-‖f‖ / 3) ((f : (a : X) → ℝ) x : ℝ)
rw₂ rw₃ :
  HSub.hSub (β := ℝ) (-‖f‖ / 3) ((f : (a : X) → ℝ) x : ℝ) = HSub.hSub (β := ℝ) (-‖f‖ / 3) ((f : (a : X) → ℝ) x : ℝ)
⊢ |HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : Y) → ℝ) ((e : (a : X) → Y) x : Y) : ℝ) ((f : (a : X) → ℝ) x : ℝ)| =
    HSub.hSub (β := ℝ) (-‖f‖ / 3) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
rw [hg₁ (mem_image_of_mem _ hle₁), Function.const_apply,
            abs_of_nonneg (sub_nonneg.2 hle₁)]

Premises used: Function.const_apply, Iff.mpr, Set.mem_image_of_mem, abs_of_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 →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : (f : (a : X) → ℝ) x ≤ -‖f‖ / 3
f₁ :
  |HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : Y) → ℝ) ((e : (a : X) → Y) x : Y) : ℝ) ((f : (a : X) → ℝ) x : ℝ)| =
    HSub.hSub (β := ℝ) (-‖f‖ / 3) ((f : (a : X) → ℝ) x : ℝ)
f₂ : HSub.hSub (β := ℝ) (-‖f‖ / 3) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖
⊢ dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖

Tactic:
calc
        |g (e x) - f x| = -‖f‖ / 3 - f x := by
          rw [hg₁ (mem_image_of_mem _ hle₁), Function.const_apply,
            abs_of_nonneg (sub_nonneg.2 hle₁)]
        _ ≤ 2 / 3 * ‖f‖ := by linarith

Premises used: DFunLike.coe
-- 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
inr :
  ∀ (hle₂ : (f : (a : X) → ℝ) x ≤ ‖f‖ / 3),
    dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖
inr₁ :
  ∀ (hle₂ : ‖f‖ / 3 ≤ (f : (a : X) → ℝ) x),
    dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖
⊢ dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖

Tactic:
rcases le_total (f x) (‖f‖ / 3) with hle₂ | hle₂

Premises used: Norm.norm, HDiv.hDiv, le_total, OfNat.ofNat, DFunLike.coe
-- 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
hle₂ : (f : (a : X) → ℝ) x ≤ ‖f‖ / 3
⊢ -(‖f‖ / 3) < ‖f‖ / 3

Tactic:
simp only [neg_div] at *

Premises used: neg_div
-- 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
hle₂ : (f : (a : X) → ℝ) x ≤ ‖f‖ / 3
hf3₁ : -(‖f‖ / 3) < ‖f‖ / 3
⊢ IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))

Tactic:
simp only [neg_div] at *

Premises used: neg_div
-- 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
hle₂ : (f : (a : X) → ℝ) x ≤ ‖f‖ / 3
hf3₁ : -(‖f‖ / 3) < ‖f‖ / 3
hc₃ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
⊢ Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))

Tactic:
simp only [neg_div] at *

Premises used: neg_div
-- 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
hle₂ : (f : (a : X) → ℝ) x ≤ ‖f‖ / 3
hf3₁ : -(‖f‖ / 3) < ‖f‖ / 3
hc₃ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
hd₁ :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
⊢ EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-(‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))

Tactic:
simp only [neg_div] at *

Premises used: neg_div
-- 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
hle₂ : (f : (a : X) → ℝ) x ≤ ‖f‖ / 3
hf3₁ : -(‖f‖ / 3) < ‖f‖ / 3
hc₃ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
hd₁ :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hg₃ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-(‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
⊢ ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-(‖f‖ / 3)) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)

Tactic:
simp only [neg_div] at *

Premises used: neg_div
-- 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
hle₂ : (f : (a : X) → ℝ) x ≤ ‖f‖ / 3
hf3₁ : -(‖f‖ / 3) < ‖f‖ / 3
hc₃ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
hd₁ :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hg₃ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-(‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
hgf₁ : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-(‖f‖ / 3)) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
⊢ -(‖f‖ / 3) ≤ (f : (a : X) → ℝ) x

Tactic:
simp only [neg_div] at *

Premises used: neg_div
-- 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₂ : (f : (a : X) → ℝ) x ≤ ‖f‖ / 3
hf3 : -(‖f‖ / 3) < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-(‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-(‖f‖ / 3)) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
hle₁ : -(‖f‖ / 3) ≤ (f : (a : X) → ℝ) x
⊢ dist (α := ℝ) ((g : (a : Y) → ℝ) ((e : (a : X) → Y) x : Y) : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) (|(g : (a : Y) → ℝ) ((e : (a : X) → Y) x : Y)| : ℝ) (|(f : (a : X) → ℝ) x| : ℝ)

Tactic:
dist_le_norm_add_norm _ _

Premises used: dist_le_norm_add_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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₂ : (f : (a : X) → ℝ) x ≤ ‖f‖ / 3
hf3 : -(‖f‖ / 3) < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-(‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-(‖f‖ / 3)) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
hle₁ : -(‖f‖ / 3) ≤ (f : (a : X) → ℝ) x
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) (|(g : (a : Y) → ℝ) ((e : (a : X) → Y) x : Y)| : ℝ) (|(f : (a : X) → ℝ) x| : ℝ) ≤
    ‖f‖ / 3 + ‖f‖ / 3

Tactic:
(add_le_add (abs_le.2 <| hgf _) (abs_le.2 ⟨hle₁, hle₂⟩))

Premises used: Iff.mpr, abs_le, add_le_add, And.intro
-- 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₂ : (f : (a : X) → ℝ) x ≤ ‖f‖ / 3
hf3 : -(‖f‖ / 3) < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-(‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-(‖f‖ / 3))))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-(‖f‖ / 3)) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
hle₁ : -(‖f‖ / 3) ≤ (f : (a : X) → ℝ) x
dist : ‖f‖ / 3 + ‖f‖ / 3 = 2 / 3 * ‖f‖
⊢ Dist.dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖

Tactic:
calc
          dist (g (e x)) (f x) ≤ |g (e x)| + |f x| := dist_le_norm_add_norm _ _
          _ ≤ ‖f‖ / 3 + ‖f‖ / 3 := (add_le_add (abs_le.2 <| hgf _) (abs_le.2 ⟨hle₁, hle₂⟩))
          _ = 2 / 3 * ‖f‖ := by linarith

Premises used: Iff.mpr, dist_le_norm_add_norm, abs_le, add_le_add, And.intro, Dist.dist, DFunLike.coe
-- 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
hle₂ : ‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
rw :
  |HSub.hSub (β := ℝ) (Function.const.{1, u_2 + 1} Y (‖f‖ / 3) ((e : (a : X) → Y) x : Y)) ((f : (a : X) → ℝ) x : ℝ)| =
    HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (‖f‖ / 3)
rw₁ :
  |HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (Function.const.{1, u_2 + 1} Y (‖f‖ / 3) ((e : (a : X) → Y) x : Y))| =
    HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (‖f‖ / 3)
rw₂ : |HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (‖f‖ / 3)| = HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (‖f‖ / 3)
rw₃ rw₄ :
  HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (‖f‖ / 3) = HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (‖f‖ / 3)
⊢ |HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : Y) → ℝ) ((e : (a : X) → Y) x : Y) : ℝ) ((f : (a : X) → ℝ) x : ℝ)| =
    HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (‖f‖ / 3)

Tactic:
rw [hg₂ (mem_image_of_mem _ hle₂), abs_sub_comm, Function.const_apply,
              abs_of_nonneg (sub_nonneg.2 hle₂)]

Premises used: Function.const_apply, Iff.mpr, Set.mem_image_of_mem, abs_of_nonneg, abs_sub_comm, 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 →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hd :
  Disjoint.{u_2} (α := Set Y) (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (-‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))
hg₂ :
  EqOn (⇑g : (a : Y) → ℝ) (Function.const Y (‖f‖ / 3))
    (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), Membership.mem (α := ℝ) (Icc (-‖f‖ / 3) (‖f‖ / 3)) ((g : (a : Y) → ℝ) x : ℝ)
x : X
hfx : -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
hle₂ : ‖f‖ / 3 ≤ (f : (a : X) → ℝ) x
f₁ :
  |HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : Y) → ℝ) ((e : (a : X) → Y) x : Y) : ℝ) ((f : (a : X) → ℝ) x : ℝ)| =
    HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (‖f‖ / 3)
f₂ : HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (‖f‖ / 3) ≤ 2 / 3 * ‖f‖
⊢ dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖

Tactic:
calc
          |g (e x) - f x| = f x - ‖f‖ / 3 := by
            rw [hg₂ (mem_image_of_mem _ hle₂), abs_sub_comm, Function.const_apply,
              abs_of_nonneg (sub_nonneg.2 hle₂)]
          _ ≤ 2 / 3 * ‖f‖ := by linarith

Premises used: DFunLike.coe