awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x x_1 : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {0, 1} x_1
⊢ Eq (α := X)
    (({
            toFun := fun (x_2 : (↑I : Type)) ↦
              (Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (x, x_2).1))
                    (γ.subpath t₀ (Icc.convexComb t₁ t₂ (x, x_2).1)) (γ.subpath (Icc.convexComb t₁ t₂ (x, x_2).1) t₂) :
                  (a : (↑I : Type)) → X)
                (x, x_2).2,
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x_1 :
      X)
    ((((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap : (a : (↑I : Type)) → X) x_1 : X)
have inl : Eq (α := X)
  (({
          toFun := fun (x_2 : (↑I : Type)) ↦
            (Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (x, x_2).1))
                  (γ.subpath t₀ (Icc.convexComb t₁ t₂ (x, x_2).1)) (γ.subpath (Icc.convexComb t₁ t₂ (x, x_2).1) t₂) :
                (a : (↑I : Type)) → X)
              (x, x_2).2,
          continuous_toFun := sorry : C((↑I : Type), X) } :
        (a : (↑I : Type)) → X)
      0 :
    X)
  ((((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap : (a : (↑I : Type)) → X) 0 : X)
Tactic: rcases hx with rfl | rfl
Cleared hypotheses: x_1, hx
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x x_1 : (↑I : Type)
hx : Membership.mem (γ := Set (↑I : Type)) {0, 1} x_1
inl :
  Eq (α := X)
    (({
            toFun := fun (x_2 : (↑I : Type)) ↦
              (Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (x, x_2).1))
                    (γ.subpath t₀ (Icc.convexComb t₁ t₂ (x, x_2).1)) (γ.subpath (Icc.convexComb t₁ t₂ (x, x_2).1) t₂) :
                  (a : (↑I : Type)) → X)
                (x, x_2).2,
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        0 :
      X)
    ((((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap : (a : (↑I : Type)) → X) 0 : X)
⊢ Eq (α := X)
    (({
            toFun := fun (x_2 : (↑I : Type)) ↦
              (Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (x, x_2).1))
                    (γ.subpath t₀ (Icc.convexComb t₁ t₂ (x, x_2).1)) (γ.subpath (Icc.convexComb t₁ t₂ (x, x_2).1) t₂) :
                  (a : (↑I : Type)) → X)
                (x, x_2).2,
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x_1 :
      X)
    ((((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap : (a : (↑I : Type)) → X) x_1 : X)
have inr : Eq (α := X)
  (({
          toFun := fun (x_2 : (↑I : Type)) ↦
            (Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (x, x_2).1))
                  (γ.subpath t₀ (Icc.convexComb t₁ t₂ (x, x_2).1)) (γ.subpath (Icc.convexComb t₁ t₂ (x, x_2).1) t₂) :
                (a : (↑I : Type)) → X)
              (x, x_2).2,
          continuous_toFun := sorry : C((↑I : Type), X) } :
        (a : (↑I : Type)) → X)
      1 :
    X)
  ((((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap : (a : (↑I : Type)) → X) 1 : X)
Tactic: rcases hx with rfl | rfl
Cleared hypotheses: x_1, hx
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
p : Fin 1 → X
F : (k : Fin 0) → Path (p k.castSucc) (p k.succ)
⊢ concat p F = refl (p 0)
have rw : Eq.{u_1 + 1} (α := Path (p 0) (p (last 0)))
  (dfoldl.{u_1} 0 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ Path (p 0) (p i))
      (fun (i : Fin 0) (ih : Path (p 0) (p i.castSucc)) ↦ ih.trans (F i)) (refl (p 0)) :
    Path (p 0) (p (last 0)))
  (refl (p 0) : Path (p 0) (p 0))
Tactic: rw [concat, dfoldl_zero]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
p : Fin 1 → X
F : (k : Fin 0) → Path (p k.castSucc) (p k.succ)
rw :
  Eq.{u_1 + 1} (α := Path (p 0) (p (last 0)))
    (dfoldl.{u_1} 0 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ Path (p 0) (p i))
        (fun (i : Fin 0) (ih : Path (p 0) (p i.castSucc)) ↦ ih.trans (F i)) (refl (p 0)) :
      Path (p 0) (p (last 0)))
    (refl (p 0) : Path (p 0) (p 0))
⊢ concat p F = refl (p 0)
have rw₁ : Eq (α := Path (p 0) (p (last 0))) (refl (p 0)) (refl (p 0))
Tactic: rw [concat, dfoldl_zero]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
p : Fin (n + 2) → X
F : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
⊢ concat p F = trans (concat (p ∘ castSucc) fun (k : Fin n) ↦ F k.castSucc) (F (last n))
have rw : trans
    (dfoldl n ((fun (i : Fin (n + 1 + 1)) ↦ Path (p 0) (p i)) ∘ castSucc)
      (fun (x1 : Fin n) (x2 : ((fun (i : Fin (n + 1 + 1)) ↦ Path (p 0) (p i)) ∘ castSucc) x1.castSucc) ↦
        trans x2 (F x1.castSucc))
      (refl (p 0)))
    (F (last n)) =
  trans (concat (p ∘ castSucc) fun (k : Fin n) ↦ F k.castSucc) (F (last n))
Tactic: rw [concat, dfoldl_succ_last]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ Eq.{u_1 + 1} (α := Path x x)
    (concat.{u_1} (X := X) (n := 0) (fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x) fun (x_1 : Fin 0) ↦ refl x :
      Path x x)
    (refl x : Path x x)
have zero : Eq (α := Path x x) (refl x) (refl x)
Tactic: rw [concat_zero]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
n : ℕ
h :
  Eq.{u_1 + 1} (α := Path x x)
    (concat.{u_1} (X := X) (n := n) (fun (x_1 : Fin (n + 1)) ↦ x) fun (x_1 : Fin n) ↦ refl x : Path x x)
    (refl x : Path x x)
⊢ Eq.{u_1 + 1} (α := Path x x)
    (concat.{u_1} (X := X) (n := n + 1) (fun (x_1 : Fin (n + 1 + 1)) ↦ x) fun (x_1 : Fin (n + 1)) ↦ refl x : Path x x)
    (refl x : Path x x)
have succ : Eq.{u_1 + 1} (α := Path x x)
  (trans (concat ((fun (x_1 : Fin (n + 1 + 1)) ↦ x) ∘ castSucc) fun (k : Fin n) ↦ refl x) (refl x) :
    Path (((fun (x_1 : Fin (n + 1 + 1)) ↦ x) ∘ castSucc) 0) x)
  (refl x)
Tactic: rw [concat_succ]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
x : X
⊢ Eq.{u_1 + 1} (α := Path x x)
    (concat.{u_1} (X := X) (n := n) (fun (x_1 : Fin (n + 1)) ↦ x) fun (x_1 : Fin n) ↦ refl x : Path x x)
    (refl x : Path x x)
have zero : Eq.{u_1 + 1} (α := Path x x)
  (concat.{u_1} (X := X) (n := 0) (fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x) fun (x_1 : Fin 0) ↦ refl x : Path x x)
  (refl x : Path x x)
Tactic: induction n with
  | zero => rw [concat_zero]
  | succ _ _ =>
    rw [concat_succ]
    convert! refl_trans_refl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
x : X
zero :
  Eq.{u_1 + 1} (α := Path x x)
    (concat.{u_1} (X := X) (n := 0) (fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x) fun (x_1 : Fin 0) ↦ refl x :
      Path x x)
    (refl x : Path x x)
⊢ Eq.{u_1 + 1} (α := Path x x)
    (concat.{u_1} (X := X) (n := n) (fun (x_1 : Fin (n + 1)) ↦ x) fun (x_1 : Fin n) ↦ refl x : Path x x)
    (refl x : Path x x)
have succ : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := Path x x)
      (concat.{u_1} (X := X) (n := n) (fun (x_1 : Fin (n + 1)) ↦ x) fun (x_1 : Fin n) ↦ refl x : Path x x)
      (refl x : Path x x) →
    Eq.{u_1 + 1} (α := Path x x)
      (concat.{u_1} (X := X) (n := n + 1) (fun (x_1 : Fin (n + 1 + 1)) ↦ x) fun (x_1 : Fin (n + 1)) ↦ refl x : Path x x)
      (refl x : Path x x)
Tactic: induction n with
  | zero => rw [concat_zero]
  | succ _ _ =>
    rw [concat_succ]
    convert! refl_trans_refl
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
n : ℕ
p : Fin (HAdd.hAdd (α := ℕ) 0 1) → X
F G : (k : Fin 0) → Path (p k.castSucc) (p k.succ)
H : (k : Fin 0) → (F k).Homotopy (G k)
⊢ (concat p F).Homotopy (concat p G)
have zero : Homotopy (Path.refl (p 0)) (Path.refl (p 0))
Tactic: rw [concat_zero, concat_zero]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
n_1 n : ℕ
ih :
  (p : Fin (n + 1) → X) →
    (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
      (H : (k : Fin n) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
p : Fin (n + 1 + 1) → X
F G : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
H : (k : Fin (n + 1)) → (F k).Homotopy (G k)
⊢ (concat p F).Homotopy (concat p G)
have succ : (Path.trans (concat (p ∘ castSucc) fun (k : Fin n) ↦ F k.castSucc) (F (last n))).Homotopy
  (Path.trans (concat (p ∘ castSucc) fun (k : Fin n) ↦ G k.castSucc) (G (last n)))
Tactic: rw [concat_succ, concat_succ]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
n : ℕ
p : Fin (n + 1) → X
F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)
H : (k : Fin n) → (F k).Homotopy (G k)
⊢ (concat p F).Homotopy (concat p G)
have zero : (p : Fin (HAdd.hAdd (α := ℕ) 0 1) → X) →
  (F G : (k : Fin 0) → Path (p k.castSucc) (p k.succ)) →
    (H : (k : Fin 0) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
Tactic: induction n with
  | zero =>
    rw [concat_zero, concat_zero]
    exact refl (Path.refl _)
  | succ n ih =>
    rw [concat_succ, concat_succ]
    exact hcomp (ih _ _ _ (fun k ↦ H k.castSucc)) (H (last n))
Cleared hypotheses: p, F, G, H
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
n : ℕ
p : Fin (n + 1) → X
F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)
H : (k : Fin n) → (F k).Homotopy (G k)
zero :
  (p : Fin (HAdd.hAdd (α := ℕ) 0 1) → X) →
    (F G : (k : Fin 0) → Path (p k.castSucc) (p k.succ)) →
      (H : (k : Fin 0) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
⊢ (concat p F).Homotopy (concat p G)
have succ : (n : ℕ) →
  (ih :
      (p : Fin (n + 1) → X) →
        (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
          (H : (k : Fin n) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)) →
    (p : Fin (n + 1 + 1) → X) →
      (F G : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)) →
        (H : (k : Fin (n + 1)) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
Tactic: induction n with
  | zero =>
    rw [concat_zero, concat_zero]
    exact refl (Path.refl _)
  | succ n ih =>
    rw [concat_succ, concat_succ]
    exact hcomp (ih _ _ _ (fun k ↦ H k.castSucc)) (H (last n))
Cleared hypotheses: p, F, G, H
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
n : ℕ
γ : Path a b
t : Fin (HAdd.hAdd (α := ℕ) 0 1) → (↑I : Type)
⊢ Homotopy (X := X) (x₀ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0)
    (concat ((⇑γ : (a : (↑I : Type)) → X) ∘ t) fun (k : Fin 0) ↦ γ.subpath (t k.castSucc) (t k.succ))
    (γ.subpath (t 0) (t (last 0)))
have zero : Homotopy (X := X) (x₀ := (((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0 : X)) (x₁ := (((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0 : X))
  (Path.refl (((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0) :
    Path (X := X) (((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0) (((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0))
  (Path.refl ((γ : (a : (↑I : Type)) → X) (t 0)) :
    Path (X := X) ((γ : (a : (↑I : Type)) → X) (t 0) : X) ((γ : (a : (↑I : Type)) → X) (t 0) : X))
Tactic: simp only [concat_zero, reduceLast, subpath_self]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
n_1 : ℕ
γ : Path a b
n : ℕ
ih :
  (t : Fin (n + 1) → (↑I : Type)) →
    Homotopy (X := X) (x₀ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0)
      (concat ((⇑γ : (a : (↑I : Type)) → X) ∘ t) fun (k : Fin n) ↦ γ.subpath (t k.castSucc) (t k.succ))
      (γ.subpath (t 0) (t (last n)))
t : Fin (n + 1 + 1) → (↑I : Type)
⊢ Homotopy (X := X) (x₀ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0)
    (concat ((⇑γ : (a : (↑I : Type)) → X) ∘ t) fun (k : Fin (n + 1)) ↦ γ.subpath (t k.castSucc) (t k.succ))
    (γ.subpath (t 0) (t (last (n + 1))))
have succ : Homotopy (X := X) (x₀ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0) (x₁ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) (last (n + 1)))
  (Path.trans
      (concat (((⇑γ : (a : (↑I : Type)) → X) ∘ t) ∘ castSucc) fun (k : Fin n) ↦
        γ.subpath (t k.castSucc.castSucc) (t k.castSucc.succ))
      (γ.subpath (t (last n).castSucc) (t (last n).succ)) :
    Path (X := X) ((((⇑γ : (a : (↑I : Type)) → X) ∘ t) ∘ castSucc) 0)
      (((⇑γ : (a : (↑I : Type)) → X) ∘ t) (last n).succ))
  (γ.subpath (t 0) (t (last (n + 1))))
Tactic: rw [concat_succ]
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
n : ℕ
γ : Path a b
t : Fin (n + 1) → (↑I : Type)
⊢ Homotopy (X := X) (x₀ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0)
    (concat ((⇑γ : (a : (↑I : Type)) → X) ∘ t) fun (k : Fin n) ↦ γ.subpath (t k.castSucc) (t k.succ))
    (γ.subpath (t 0) (t (last n)))
have zero : (t : Fin (HAdd.hAdd (α := ℕ) 0 1) → (↑I : Type)) →
  Homotopy (X := X) (x₀ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0)
    (concat ((⇑γ : (a : (↑I : Type)) → X) ∘ t) fun (k : Fin 0) ↦ γ.subpath (t k.castSucc) (t k.succ))
    (γ.subpath (t 0) (t (last 0)))
Tactic: induction n with
  | zero =>
    simp only [concat_zero, reduceLast, subpath_self]
    exact refl _
  | succ n ih =>
    rw [concat_succ]
    exact trans ((ih (t ∘ castSucc)).hcomp (refl _)) (subpathTransSubpath γ _ _ _)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Topology.Subpath (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
n : ℕ
γ : Path a b
t : Fin (n + 1) → (↑I : Type)
zero :
  (t : Fin (HAdd.hAdd (α := ℕ) 0 1) → (↑I : Type)) →
    Homotopy (X := X) (x₀ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0)
      (concat ((⇑γ : (a : (↑I : Type)) → X) ∘ t) fun (k : Fin 0) ↦ γ.subpath (t k.castSucc) (t k.succ))
      (γ.subpath (t 0) (t (last 0)))
⊢ Homotopy (X := X) (x₀ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0)
    (concat ((⇑γ : (a : (↑I : Type)) → X) ∘ t) fun (k : Fin n) ↦ γ.subpath (t k.castSucc) (t k.succ))
    (γ.subpath (t 0) (t (last n)))
have succ : (n : ℕ) →
  (ih :
      (t : Fin (n + 1) → (↑I : Type)) →
        Homotopy (X := X) (x₀ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0)
          (concat ((⇑γ : (a : (↑I : Type)) → X) ∘ t) fun (k : Fin n) ↦ γ.subpath (t k.castSucc) (t k.succ))
          (γ.subpath (t 0) (t (last n)))) →
    (t : Fin (n + 1 + 1) → (↑I : Type)) →
      Homotopy (X := X) (x₀ := ((⇑γ : (a : (↑I : Type)) → X) ∘ t) 0)
        (concat ((⇑γ : (a : (↑I : Type)) → X) ∘ t) fun (k : Fin (n + 1)) ↦ γ.subpath (t k.castSucc) (t k.succ))
        (γ.subpath (t 0) (t (last (n + 1))))
Tactic: induction n with
  | zero =>
    simp only [concat_zero, reduceLast, subpath_self]
    exact refl _
  | succ n ih =>
    rw [concat_succ]
    exact trans ((ih (t ∘ castSucc)).hcomp (refl _)) (subpathTransSubpath γ _ _ _)
Cleared hypotheses: t
-- 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
e : X₁ → X
Y : Type v
inst_3 : TopologicalSpace Y
inst_4 : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : Homeomorph.{u₁, u} X₁ (↑(Set.range e) : Type u) := ⋯.toHomeomorph
⊢ ∃ (g : C(X, Y)), g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } = f
have obtain : ∀ (g : C(X, Y)) (hg : restrict (Set.range e) g = f.comp (↑e'.symm : C((↑(Set.range e) : Type u), X₁))),
  ∃ (g : C(X, Y)), g.comp { toFun := e, continuous_toFun := sorry : C(X₁, X) } = f
Tactic: obtain ⟨g, hg⟩ := (f.comp e'.symm).exists_restrict_eq he.isClosed_range
-- 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
e : X₁ → X
Y : Type v
inst_3 : TopologicalSpace Y
inst_4 : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : Homeomorph.{u₁, u} X₁ (↑(Set.range e) : Type u) := ⋯.toHomeomorph
g : C(X, Y)
hg : restrict (Set.range e) g = f.comp (↑e'.symm : C((↑(Set.range e) : Type u), X₁))
⊢ g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } = f
have h : ∀ (x : X₁),
  Eq.{v + 1} (α := Y) ((g.comp { toFun := e, continuous_toFun := sorry : C(X₁, X) } : (a : X₁) → Y) x : Y)
    ((f : (a : X₁) → Y) x : Y)
Tactic: ext 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
e : X₁ → X
Y : Type v
inst_3 : TopologicalSpace Y
inst_4 : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
g : C(X, Y)
hg : g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } = f
⊢ Eq (α := X₁ → Y) ((⇑g : (a : X) → Y) ∘ e) (⇑f : (a : X₁) → Y)
have h : ∀ (x : X₁), Eq.{v + 1} (α := Y) (((⇑g : (a : X) → Y) ∘ e) x : Y) ((f : (a : X₁) → Y) x : Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed[inst] s
Y : Type v
inst_2 : TopologicalSpace Y
f : ContinuousMap.{u, v} (↑s : Type u) Y
t : Set Y
hf : ∀ (x : (↑s : Type u)), Membership.mem (α := Y) t ((f : (a : (↑s : Type u)) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
⊢ ∃ (g : C(X, Y)), (∀ (x : X), Membership.mem (α := Y) t ((g : (a : X) → Y) x : Y)) ∧ restrict s g = f
have obtain : ∀ (g : ContinuousMap.{u, v} X (↑t : Type v))
  (hg : restrict s g = { toFun := Set.codRestrict (⇑f : (a : (↑s : Type u)) → Y) t hf, continuous_toFun := sorry }),
  ∃ (g : C(X, Y)), (∀ (x : X), Membership.mem (α := Y) t ((g : (a : X) → Y) x : Y)) ∧ restrict s g = f
Tactic: obtain ⟨g, hg⟩ := mk _ (map_continuous f |>.codRestrict hf) |>.exists_restrict_eq hs
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed[inst] s
Y : Type v
inst_2 : TopologicalSpace Y
f : ContinuousMap.{u, v} (↑s : Type u) Y
t : Set Y
hf : ∀ (x : (↑s : Type u)), Membership.mem (α := Y) t ((f : (a : (↑s : Type u)) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg : restrict s g = { toFun := Set.codRestrict (⇑f : (a : (↑s : Type u)) → Y) t hf, continuous_toFun := ⋯ }
⊢ restrict s
      (comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := ⋯ : C({ x : Y // x ∈ t }, Y) } g) =
    f
have h : ∀ (x : (↑s : Type u)),
  Eq.{v + 1} (α := Y)
    ((restrict s
            (comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := sorry : C({ x : Y // x ∈ t }, Y) }
              g) :
          (a : (↑s : Type u)) → Y)
        x :
      Y)
    ((f : (a : (↑s : Type u)) → Y) x : Y)
Tactic: ext 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
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst_3 : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), Membership.mem (α := Y) t ((f : (a : X₁) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
⊢ ∃ (g : C(X, Y)),
    (∀ (x : X), Membership.mem (α := Y) t ((g : (a : X) → Y) x : Y)) ∧
      g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } = f
have obtain : ∀ (g : ContinuousMap.{u, v} X (↑t : Type v))
  (hg :
    g.comp { toFun := e, continuous_toFun := sorry : C(X₁, X) } =
      { toFun := Set.codRestrict (⇑f : (a : X₁) → Y) t hf, continuous_toFun := sorry }),
  ∃ (g : C(X, Y)),
    (∀ (x : X), Membership.mem (α := Y) t ((g : (a : X) → Y) x : Y)) ∧
      g.comp { toFun := e, continuous_toFun := sorry : C(X₁, X) } = f
Tactic: obtain ⟨g, hg⟩ := mk _ (map_continuous f |>.codRestrict hf) |>.exists_extension he
-- 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
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst_3 : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), Membership.mem (α := Y) t ((f : (a : X₁) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg :
  g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } =
    { toFun := Set.codRestrict (⇑f : (a : X₁) → Y) t hf, continuous_toFun := ⋯ }
⊢ (comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := ⋯ : C({ x : Y // x ∈ t }, Y) } g).comp
      { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } =
    f
have h : ∀ (x : X₁),
  Eq.{v + 1} (α := Y)
    (((comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := sorry : C({ x : Y // x ∈ t }, Y) }
                g).comp
            { toFun := e, continuous_toFun := sorry : C(X₁, X) } :
          (a : X₁) → Y)
        x :
      Y)
    ((f : (a : X₁) → Y) x : Y)
Tactic: ext 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_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
ι : Type u_1
Y : ι → Type v
inst_5 : (i : ι) → TopologicalSpace (Y i)
inst_6 : ∀ (i : ι), TietzeExtension.{u, v} (Y i)
X_1 : Type u
inst_7 : TopologicalSpace X_1
inst_8 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_7] s
f : C((↑s : Type u), (i : ι) → Y i)
⊢ ∃ (g : C(X_1, (i : ι) → Y i)), ContinuousMap.restrict s g = f
have obtain : ∀ (g' : (x : ι) → ContinuousMap.{u, v} X_1 (Y x))
  (hg' :
    ∀ (x : ι),
      ContinuousMap.restrict s (g' x) =
        (Equiv.symm (ContinuousMap.piEquiv (↑s : Type u) Y) :
            (a : C((↑s : Type u), (i : ι) → Y i)) → (i : ι) → C((↑s : Type u), Y i))
          f x),
  ∃ (g : C(X_1, (i : ι) → Y i)), ContinuousMap.restrict s g = f
Tactic: obtain ⟨g', hg'⟩ := Classical.skolem.mp <| fun i ↦
      ContinuousMap.exists_restrict_eq hs (ContinuousMap.piEquiv _ _ |>.symm f i)
-- 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
ι : Type u_1
Y : ι → Type v
inst_5 : (i : ι) → TopologicalSpace (Y i)
inst_6 : ∀ (i : ι), TietzeExtension.{u, v} (Y i)
X_1 : Type u
inst_7 : TopologicalSpace X_1
inst_8 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_7] s
f : C((↑s : Type u), (i : ι) → Y i)
g' : (x : ι) → ContinuousMap.{u, v} X_1 (Y x)
hg' :
  ∀ (x : ι),
    ContinuousMap.restrict s (g' x) =
      (Equiv.symm (ContinuousMap.piEquiv (↑s : Type u) Y) :
          (a : C((↑s : Type u), (i : ι) → Y i)) → (i : ι) → C((↑s : Type u), Y i))
        f x
⊢ ContinuousMap.restrict s ((ContinuousMap.piEquiv X_1 Y : (a : (i : ι) → C(X_1, Y i)) → C(X_1, (i : ι) → Y i)) g') = f
have h : ∀ (x : (↑s : Type u)) (i : ι),
  Eq.{v + 1} (α := Y i)
    ((ContinuousMap.restrict s
            ((ContinuousMap.piEquiv X_1 Y : (a : (i : ι) → C(X_1, Y i)) → C(X_1, (i : ι) → Y i)) g') :
          (a : (↑s : Type u)) → (i : ι) → Y i)
        x i :
      Y i)
    ((f : (a : (↑s : Type u)) → (i : ι) → Y i) x i : Y i)
Tactic: ext x i
-- 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 × Z)), ContinuousMap.restrict s g = f
have obtain : ∀ (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
Tactic: obtain ⟨g₁, hg₁⟩ := (ContinuousMap.fst.comp f).exists_restrict_eq hs