awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
e : Y ≃ₜ Z
⊢ Eq (α := C(Y, Y)) (ContinuousMap.comp (↑e.symm : C(Z, Y)) (↑e : C(Y, Z))) (ContinuousMap.id Y)

Tactic:
simp
-- 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)
⊢ LT.lt (α := ℝ) 0 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)
⊢ LT.lt (α := ℝ) 0 3

Tactic:
have h3 : (0 : ℝ) < 3 := by 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)
h3 : LT.lt (α := ℝ) 0 3
⊢ 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)
h3 : LT.lt (α := ℝ) 0 3
⊢ 0 < 2 / 3

Tactic:
have h23 : 0 < (2 / 3 : ℝ) := by 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)
h3 : LT.lt (α := ℝ) 0 3
h23 : 0 < 2 / 3
inl :
  ∃ (g : Y →ᵇ ℝ),
    ‖g‖ ≤ norm.{u_1} (E := X →ᵇ ℝ) 0 / 3 ∧ dist (g.compContinuous e) 0 ≤ 2 / 3 * norm.{u_1} (E := X →ᵇ ℝ) 0
inr : ∀ (hf : f ≠ 0), ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
rcases eq_or_ne f 0 with (rfl | hf)

Premises used: eq_or_ne, OfNat.ofNat, 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 : 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
⊢ ∃ (g : Y →ᵇ ℝ),
    ‖g‖ ≤ norm.{u_1} (E := X →ᵇ ℝ) 0 / 3 ∧ dist (g.compContinuous e) 0 ≤ 2 / 3 * norm.{u_1} (E := X →ᵇ ℝ) 0

Tactic:
simp
-- 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 : f ≠ 0
⊢ 0 < ‖f‖

Tactic:
replace hf : 0 < ‖f‖ := norm_pos_iff.2 hf
-- 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‖
⊢ -‖f‖ / 3 < ‖f‖ / 3

Tactic:
have hf3 : -‖f‖ / 3 < ‖f‖ / 3 := (div_lt_div_iff_of_pos_right h3).2 (Left.neg_lt_self hf)
-- 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
⊢ IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Iic (-‖f‖ / 3)))

Tactic:
have hc₁ : IsClosed (e '' f ⁻¹' Iic (-‖f‖ / 3)) :=
    he.isClosedMap _ (isClosed_Iic.preimage f.continuous)
-- 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)))
⊢ IsClosed[inst_1] (image (α := X) (⇑e : (a : X) → Y) ((⇑f : (a : X) → ℝ) ⁻¹' Ici (‖f‖ / 3)))

Tactic:
have hc₂ : IsClosed (e '' f ⁻¹' Ici (‖f‖ / 3)) :=
    he.isClosedMap _ (isClosed_Ici.preimage f.continuous)
-- 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)))
⊢ 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:
disjoint_image_of_injective he.injective (Disjoint.preimage _ ?_)

Premises used: Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Disjoint.preimage, Set.disjoint_image_of_injective
-- 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)))
refine : Disjoint (Iic (-‖f‖ / 3)) (Ici (‖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:
refine disjoint_image_of_injective he.injective (Disjoint.preimage _ ?_)

Premises used: Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Disjoint.preimage, Set.disjoint_image_of_injective
-- 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)))
rwa : ¬‖f‖ / 3 ≤ -‖f‖ / 3
rwa₁ rwa₂ rwa₃ rwa₄ : -‖f‖ / 3 < ‖f‖ / 3
⊢ Disjoint (Iic (-‖f‖ / 3)) (Ici (‖f‖ / 3))

Tactic:
rwa [Iic_disjoint_Ici, not_le]

Premises used: not_le, Set.Iic_disjoint_Ici
-- 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)))
⊢ 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:
have hd : Disjoint (e '' f ⁻¹' Iic (-‖f‖ / 3)) (e '' f ⁻¹' Ici (‖f‖ / 3)) := by
    refine disjoint_image_of_injective he.injective (Disjoint.preimage _ ?_)
    rwa [Iic_disjoint_Ici, not_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 : 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)))
inr :
  ∀ (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 : ℝ)),
    ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
rcases exists_bounded_mem_Icc_of_closed_of_le hc₁ hc₂ hd hf3.le with ⟨g, hg₁, hg₂, hgf⟩

Premises used: LT.lt.le, exists_bounded_mem_Icc_of_closed_of_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 : 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 : ℝ)
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
⟨g, ?_, ?_⟩

Premises used: And.intro, Exists.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‖
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 : ℝ)
inr : ‖g‖ ≤ ‖f‖ / 3
inr₁ : dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
refine ⟨g, ?_, ?_⟩
-- 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 : ℝ)
⊢ ‖g‖ ≤ ‖f‖ / 3

Tactic:
(norm_le <| div_nonneg hf.le h3.le).mpr fun y => ?_

Premises used: Iff.mpr, BoundedContinuousFunction.norm_le, LT.lt.le, div_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 : ℝ)
inr : ∀ (y : Y), norm (E := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ≤ ‖f‖ / 3
⊢ ‖g‖ ≤ ‖f‖ / 3

Tactic:
refine (norm_le <| div_nonneg hf.le h3.le).mpr fun y => ?_

Premises used: Iff.mpr, BoundedContinuousFunction.norm_le, LT.lt.le, div_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 : ℝ)
y : Y
⊢ norm (E := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ≤ ‖f‖ / 3

Tactic:
simpa [abs_le, neg_div] using hgf y

Premises used: neg_div, abs_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 : 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 : ℝ)
⊢ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
(dist_le <| mul_nonneg h23.le hf.le).mpr fun x => ?_

Premises used: Iff.mpr, mul_nonneg, BoundedContinuousFunction.dist_le, LT.lt.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 : 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 : ℝ)
inr : ∀ (x : X), dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖
⊢ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
refine (dist_le <| mul_nonneg h23.le hf.le).mpr fun x => ?_

Premises used: Iff.mpr, mul_nonneg, BoundedContinuousFunction.dist_le, LT.lt.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 : 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
⊢ -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖

Tactic:
simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm x

Premises used: abs_le, BoundedContinuousFunction.norm_coe_le_norm, Real.norm_eq_abs
-- 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
⊢ -‖f‖ ≤ (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ ‖f‖

Tactic:
have hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖ := by
      simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm 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 →ᵇ ℝ
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‖
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, Neg.neg