awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
Y : Type v
Z : Type w
inst_5 : TopologicalSpace Y
inst_6 : TietzeExtension Y
inst_7 : TopologicalSpace Z
inst_8 : TietzeExtension Z
X_1 : Type u
inst_9 : TopologicalSpace X_1
inst_10 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_9] s
f : C((↑s : Type u), Y × Z)
g₁ : C(X_1, Y)
hg₁ : ContinuousMap.restrict s g₁ = ContinuousMap.comp ContinuousMap.fst f
⊢ ∃ (g : C(X_1, Y × Z)), ContinuousMap.restrict s g = f
have obtain : ∀ (g₂ : C(X_1, Z)) (hg₂ : ContinuousMap.restrict s g₂ = ContinuousMap.comp ContinuousMap.snd f),
  ∃ (g : C(X_1, Y × Z)), ContinuousMap.restrict s g = f
Tactic: obtain ⟨g₂, hg₂⟩ := (ContinuousMap.snd.comp f).exists_restrict_eq hs
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
Y : Type v
Z : Type w
inst_5 : TopologicalSpace Y
inst_6 : TietzeExtension Y
inst_7 : TopologicalSpace Z
inst_8 : TietzeExtension Z
X_1 : Type u
inst_9 : TopologicalSpace X_1
inst_10 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_9] s
f : C((↑s : Type u), Y × Z)
g₁ : C(X_1, Y)
hg₁ : ContinuousMap.restrict s g₁ = ContinuousMap.comp ContinuousMap.fst f
g₂ : C(X_1, Z)
hg₂ : ContinuousMap.restrict s g₂ = ContinuousMap.comp ContinuousMap.snd f
⊢ ContinuousMap.restrict s (g₁.prodMk g₂) = f
have h : ∀ (x : (↑s : Type u)),
  Eq (α := Y × Z) ((ContinuousMap.restrict s (g₁.prodMk g₂) : (a : (↑s : Type u)) → Y × Z) x : Y × Z)
    ((f : (a : (↑s : Type u)) → Y × Z) x : Y × Z)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
Y : Type v
inst_5 : TopologicalSpace Y
inst_6 : Nonempty Y
inst_7 : Subsingleton Y
X_1 : Type u
inst_8 : TopologicalSpace X_1
inst_9 : NormalSpace X_1
x : Set X_1
h : IsClosed[inst_8] x
f : ContinuousMap.{u, v} (↑x : Type u) Y
y : Y
⊢ ContinuousMap.restrict x (ContinuousMap.const X_1 y) = f
have h : ∀ (a : (↑x : Type u)),
  Eq.{v + 1} (α := Y) ((ContinuousMap.restrict x (ContinuousMap.const X_1 y) : (a : (↑x : Type u)) → Y) a : Y)
    ((f : (a : (↑x : Type u)) → Y) a : Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
⊢ ∃ (g : C(X, Y)), ContinuousMap.restrict s g = f
have obtain : ∀ (g : C(X, Z)) (hg : ContinuousMap.restrict s g = ι.comp f), ∃ (g : C(X, Y)), ContinuousMap.restrict s g = f
Tactic: obtain ⟨g, hg⟩ := (ι.comp f).exists_restrict_eq hs
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
g : C(X, Z)
hg : ContinuousMap.restrict s g = ι.comp f
⊢ ∃ (g : C(X, Y)), ContinuousMap.restrict s g = f
have h₁ : ContinuousMap.restrict s (r.comp g) = f
Tactic: use r.comp g
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
g : C(X, Z)
hg : ContinuousMap.restrict s g = ι.comp f
⊢ ContinuousMap.restrict s (r.comp g) = f
have h₁ : ∀ (x : (↑s : Type u)),
  Eq.{v + 1} (α := Y) ((ContinuousMap.restrict s (r.comp g) : (a : (↑s : Type u)) → Y) x : Y)
    ((f : (a : (↑s : Type u)) → Y) x : Y)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
g : C(X, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : (↑s : Type u)
⊢ Eq.{v + 1} (α := Y) ((ContinuousMap.restrict s (r.comp g) : (a : (↑s : Type u)) → Y) x : Y)
    ((f : (a : (↑s : Type u)) → Y) x : Y)
have this : r.comp (ContinuousMap.restrict s g) = r.comp (ι.comp f)
Tactic: have := congr(r.comp $(hg))
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
g : C(X, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : (↑s : Type u)
this : r.comp (ContinuousMap.restrict s g) = r.comp (ι.comp f)
⊢ Eq.{v + 1} (α := Y) ((ContinuousMap.restrict s (r.comp g) : (a : (↑s : Type u)) → Y) x : Y)
    ((f : (a : (↑s : Type u)) → Y) x : Y)
have this₁ : r.comp (ContinuousMap.restrict s g) = f
Tactic: rw [← r.comp_assoc ι, h, f.id_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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)
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have h3 : LT.lt (α := ℝ) 0 3
Tactic: have h3 : (0 : ℝ) < 3 := by norm_num1
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have h23 : 0 < 2 / 3
Tactic: have h23 : 0 < (2 / 3 : ℝ) := by norm_num1
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have inl : ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ norm.{u_1} (E := X →ᵇ ℝ) 0 / 3 ∧ dist (g.compContinuous e) 0 ≤ 2 / 3 * norm.{u_1} (E := X →ᵇ ℝ) 0
Tactic: rcases eq_or_ne f 0 with (rfl | hf)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have inr : ∀ (hf : f ≠ 0), ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
Tactic: rcases eq_or_ne f 0 with (rfl | hf)
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have hf₁ : 0 < ‖f‖
Tactic: replace hf : 0 < ‖f‖ := norm_pos_iff.2 hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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‖
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have hf3 : -‖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)
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have hc₁ : 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)
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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)))
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have hc₂ : 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)
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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)))
have refine : Disjoint (Iic (-‖f‖ / 3)) (Ici (‖f‖ / 3))
Tactic: refine disjoint_image_of_injective he.injective (Disjoint.preimage _ ?_)
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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 (Iic (-‖f‖ / 3)) (Ici (‖f‖ / 3))
have rwa : ¬‖f‖ / 3 ≤ -‖f‖ / 3
Tactic: rwa [Iic_disjoint_Ici, not_le]
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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)))
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have 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)))
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]
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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 →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have 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‖
Tactic: rcases exists_bounded_mem_Icc_of_closed_of_le hc₁ hc₂ hd hf3.le with ⟨g, hg₁, hg₂, hgf⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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‖
have inr : ‖g‖ ≤ ‖f‖ / 3
Tactic: refine ⟨g, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
have inr₁ : dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
Tactic: refine ⟨g, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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
have inr : ∀ (y : Y), norm (E := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ≤ ‖f‖ / 3
Tactic: refine (norm_le <| div_nonneg hf.le h3.le).mpr fun y => ?_
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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‖
have inr : ∀ (x : X), dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖
Tactic: refine (dist_le <| mul_nonneg h23.le hf.le).mpr fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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
⊢ dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖
have hfx : -‖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
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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‖
⊢ dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖
have inr : ∀ (hle₁ : (f : (a : X) → ℝ) x ≤ -‖f‖ / 3),
  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₁
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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‖
⊢ dist (α := ℝ) ((g.compContinuous e : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) ≤ 2 / 3 * ‖f‖
have inr₁ : ∀ (hle₁ : -‖f‖ / 3 ≤ (f : (a : X) → ℝ) x),
  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₁