awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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‖
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
have refine_2 : ‖f‖ ≤ ‖limUnder atTop g‖
Tactic: refine ⟨limUnder atTop g, le_antisymm ?_ ?_, hge⟩
-- 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)
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‖ ≤ ‖f‖
have refine_1 : dist (g 0) (limUnder atTop g) ≤ ‖f‖
Tactic: rw [← dist_zero_left, ← g0]
-- 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)
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
⊢ dist (g 0) (limUnder atTop g) ≤ ‖f‖
have refine_1 : 1 / 3 * ‖f‖ / (1 - 2 / 3) = ‖f‖
Tactic: refine
      (dist_le_of_le_geometric_of_tendsto₀ _ _ (by norm_num1)
        hg_dist hg_cau.tendsto_limUnder).trans_eq ?_
-- 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)
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
⊢ ‖f‖ ≤ ‖limUnder atTop g‖
have refine_2 : ‖(limUnder atTop g).compContinuous e‖ ≤ ‖limUnder atTop g‖
Tactic: rw [← hge]
-- 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 : X → Y
he : IsClosedEmbedding e
⊢ ∃ (g : Y →ᵇ ℝ), ‖g‖ = ‖f‖ ∧ Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have rcases : ∀ (g : Y →ᵇ ℝ) (hg : ‖g‖ = ‖g.compContinuous { toFun := e, continuous_toFun := sorry : C(X, Y) }‖),
  ∃ (g_1 : Y →ᵇ ℝ),
    ‖g_1‖ = ‖g.compContinuous { toFun := e, continuous_toFun := sorry : C(X, Y) }‖ ∧
      Eq (α := X → ℝ) ((⇑g_1 : (a : Y) → ℝ) ∘ e)
        (⇑(g.compContinuous { toFun := e, continuous_toFun := sorry : C(X, Y) }) : (a : X) → ℝ)
Tactic: rcases exists_extension_norm_eq_of_isClosedEmbedding' f ⟨e, he.continuous⟩ he with ⟨g, hg, rfl⟩
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 →ᵇ ℝ
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 →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have 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) → ℝ)
Tactic: rcases exists_extension_norm_eq_of_isClosedEmbedding (f - const X ((a + b) / 2)) he with
    ⟨g, hgf, hge⟩
-- 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 →ᵇ ℝ
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) → ℝ)
have refine_1 : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((const Y ((a + b) / 2) + g : (a : Y) → ℝ) y : ℝ)
Tactic: refine ⟨const Y ((a + b) / 2) + g, 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 →ᵇ ℝ
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 : ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have refine_2 : Eq (α := X → ℝ) ((⇑(const Y ((a + b) / 2) + g) : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: refine ⟨const Y ((a + b) / 2) + g, 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 →ᵇ ℝ
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
⊢ Membership.mem (α := ℝ) (Icc a b) ((const Y ((a + b) / 2) + g : (a : Y) → ℝ) y : ℝ)
have refine_1 : ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2
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)
-- 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 →ᵇ ℝ
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
have refine_1 : ∀ (x : X), norm (E := ℝ) ((f - const X ((a + b) / 2) : (a : X) → ℝ) x : ℝ) ≤ (b - a) / 2
Tactic: refine (norm_le <| div_nonneg (sub_nonneg.2 hle) zero_le_two).2 fun 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 →ᵇ ℝ
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) → ℝ)
⊢ Eq (α := X → ℝ) ((⇑(const Y ((a + b) / 2) + g) : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have refine_2 : ∀ (x : X), Eq (α := ℝ) (((⇑(const Y ((a + b) / 2) + g) : (a : Y) → ℝ) ∘ e) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
Tactic: ext 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 →ᵇ ℝ
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
⊢ Eq (α := ℝ) (((⇑(const Y ((a + b) / 2) + g) : (a : Y) → ℝ) ∘ e) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
have this : (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
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inhabit : ∀ (inhabited_h : Inhabited X),
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: inhabit 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have obtain : ∀ (a : ℝ) (ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a),
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: obtain ⟨a, ha⟩ : ∃ a, IsGLB (range f) a := ⟨_, isGLB_ciInf f.isBounded_range.bddBelow⟩
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have obtain : ∀ (b : ℝ) (hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b),
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: obtain ⟨b, hb⟩ : ∃ b, IsLUB (range f) b := ⟨_, isLUB_ciSup f.isBounded_range.bddAbove⟩
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
Tactic: have hmem : ∀ x, f x ∈ Icc a b := fun x => ⟨ha.1 ⟨x, rfl⟩, hb.1 ⟨x, rfl⟩⟩
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have hle : a ≤ b
Tactic: have hle : a ≤ b := (hmem default).1.trans (hmem default).2
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inl : ∀ (hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) a)
  (hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a a) ((f : (a : X) → ℝ) x : ℝ)) (hle : a ≤ a),
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: rcases hle.eq_or_lt with (rfl | hlt)
Cleared hypotheses: b, hb, hmem, 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
inl :
  ∀ (hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) a)
    (hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a a) ((f : (a : X) → ℝ) x : ℝ)) (hle : a ≤ a),
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y),
          ∃ (x₁ : X) (x₂ : X),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
              ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inr : ∀ (hlt : a < b),
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: rcases hle.eq_or_lt with (rfl | hlt)
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) a
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a a) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ a
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have this : ∀ (x : X), (f : (a : X) → ℝ) x = a
Tactic: have : ∀ x, f x = a := by simpa using hmem
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) a
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a a) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ a
this : ∀ (x : X), (f : (a : X) → ℝ) x = a
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have h : (∀ (y : Y),
    ∃ (x₁ : X) (x₂ : X),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
        ((const Y a : (a : Y) → ℝ) y : ℝ)) ∧
  Eq (α := X → ℝ) ((⇑(const Y a) : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: use const Y a
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have hac : a < c
Tactic: have hac : a < c := left_lt_add_div_two.2 hlt
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have hcb : c < b
Tactic: have hcb : c < b := add_div_two_lt_right.2 hlt
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have hsub : c - a = b - c
Tactic: have hsub : c - a = b - c := by
    simp [c]
    ring
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have rcases : ∀ (g : Y →ᵇ ℝ) (hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ))
  (hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)),
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: rcases exists_extension_forall_mem_Icc_of_isClosedEmbedding f hmem hle he with ⟨g, hg_mem, hgf⟩