awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x : (↑I : Type)
rw :
  Eq (α := X) (((γ.subpath t₀ t₂).trans (γ.subpath t₂ t₂) : (a : (↑I : Type)) → X) (1, x).2 : X)
    ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
            ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
          (a : (↑I : Type)) → X)
        x :
      X)
rw₁ :
  Eq (α := X)
    (((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂)) : (a : (↑I : Type)) → X) (1, x).2 : X)
    ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
            ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
          (a : (↑I : Type)) → X)
        x :
      X)
rw₂ rw₃ :
  Eq (α := X)
    (((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂)) : (a : (↑I : Type)) → X) (1, x).2 : X)
    (((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂)) : (a : (↑I : Type)) → X) x : X)
⊢ Eq (α := X)
    ((Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (1, x).1))
            (γ.subpath t₀ (Icc.convexComb t₁ t₂ (1, x).1)) (γ.subpath (Icc.convexComb t₁ t₂ (1, x).1) t₂) :
          (a : (↑I : Type)) → X)
        (1, x).2 :
      X)
    ((toContinuousMap (y := (γ : (a : (↑I : Type)) → X) t₂)
            ((γ.subpath t₀ t₂).trans (Path.refl ((γ : (a : (↑I : Type)) → X) t₂))) :
          (a : (↑I : Type)) → X)
        x :
      X)

Tactic:
rw [Icc.convexComb_one, subpath_self, coe_toContinuousMap]

Premises used: Set.Icc.convexComb_one, Path.subpath_self, Path.coe_toContinuousMap
-- Module: Mathlib.Topology.Subpath
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)
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 := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        1 :
      X)
    ((((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).toContinuousMap : (a : (↑I : Type)) → X) 1 : 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)

Tactic:
rcases hx with rfl | rfl

Premises used: rfl
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x : (↑I : Type)
⊢ Eq (α := X)
    (({
            toFun := fun (x_1 : (↑I : Type)) ↦
              (Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (x, x_1).1))
                    (γ.subpath t₀ (Icc.convexComb t₁ t₂ (x, x_1).1)) (γ.subpath (Icc.convexComb t₁ t₂ (x, x_1).1) t₂) :
                  (a : (↑I : Type)) → X)
                (x, x_1).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)

Tactic:
simp
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ x : (↑I : Type)
⊢ Eq (α := X)
    (({
            toFun := fun (x_1 : (↑I : Type)) ↦
              (Path.trans (y := (γ : (a : (↑I : Type)) → X) (Icc.convexComb t₁ t₂ (x, x_1).1))
                    (γ.subpath t₀ (Icc.convexComb t₁ t₂ (x, x_1).1)) (γ.subpath (Icc.convexComb t₁ t₂ (x, x_1).1) t₂) :
                  (a : (↑I : Type)) → X)
                (x, x_1).2,
            continuous_toFun := ⋯ : 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:
simp
-- Module: Mathlib.Topology.Subpath
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))
rw₁ rw₂ : Eq (α := Path (p 0) (p (last 0))) (refl (p 0)) (refl (p 0))
⊢ concat p F = refl (p 0)

Tactic:
rw [concat, dfoldl_zero]

Premises used: Path.concat, Fin.dfoldl_zero
-- Module: Mathlib.Topology.Subpath
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)
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))
⊢ concat p F = trans (concat (p ∘ castSucc) fun (k : Fin n) ↦ F k.castSucc) (F (last n))

Tactic:
rw [concat, dfoldl_succ_last]

Premises used: Path.concat, Fin.dfoldl_succ_last
-- Module: Mathlib.Topology.Subpath
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)
⊢ 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:
rfl
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
zero zero₁ : Eq (α := Path x x) (refl x) (refl 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)

Tactic:
rw [concat_zero]

Premises used: Path.concat_zero
-- Module: Mathlib.Topology.Subpath
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)
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)
⊢ 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:
rw [concat_succ]

Premises used: Path.concat_succ
-- Module: Mathlib.Topology.Subpath
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 (α := Path x x) (trans (refl x) (refl x)) (refl x)

Tactic:
refl_trans_refl

Premises used: Path.refl_trans_refl
-- Module: Mathlib.Topology.Subpath
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)
    (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:
convert! refl_trans_refl

Premises used: Path.refl_trans_refl
-- Module: Mathlib.Topology.Subpath
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)
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)
⊢ 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)

Tactic:
induction n with
  | zero => rw [concat_zero]
  | succ _ _ =>
    rw [concat_succ]
    convert! refl_trans_refl

Premises used: Fin.succ, Path.concat_zero, Path.concat_succ, Path.refl_trans_refl
-- Module: Mathlib.Topology.Subpath
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)
zero : Homotopy (Path.refl (p 0)) (Path.refl (p 0))
⊢ (concat p F).Homotopy (concat p G)

Tactic:
rw [concat_zero, concat_zero]

Premises used: Path.concat_zero
-- Module: Mathlib.Topology.Subpath
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)
⊢ Homotopy (Path.refl (p 0)) (Path.refl (p 0))

Tactic:
exact refl (Path.refl _)

Premises used: Path.Homotopy.refl, Path.refl
-- Module: Mathlib.Topology.Subpath
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)
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)))
⊢ (concat p F).Homotopy (concat p G)

Tactic:
rw [concat_succ, concat_succ]

Premises used: Path.concat_succ
-- Module: Mathlib.Topology.Subpath
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)
⊢ (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:
exact hcomp (ih _ _ _ (fun k ↦ H k.castSucc)) (H (last n))

Premises used: Path.Homotopy.hcomp
-- Module: Mathlib.Topology.Subpath
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)
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)
⊢ (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))

Premises used: Fin.succ, Path.Homotopy.refl, Path.concat_zero, Path.concat_succ, Path.refl
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
n : ℕ
γ : Path a b
t : Fin (HAdd.hAdd (α := ℕ) 0 1) → (↑I : Type)
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))
⊢ 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:
simp only [concat_zero, reduceLast, subpath_self]

Premises used: Path.subpath_self, Path.concat_zero, Fin.reduceLast
-- Module: Mathlib.Topology.Subpath
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 : 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:
exact refl _

Premises used: Path.Homotopy.refl
-- Module: Mathlib.Topology.Subpath
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)
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))))
⊢ 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:
rw [concat_succ]

Premises used: Path.concat_succ
-- Module: Mathlib.Topology.Subpath
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) (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:
exact trans ((ih (t ∘ castSucc)).hcomp (refl _)) (subpathTransSubpath γ _ _ _)

Premises used: Path.Homotopy.trans, Path.Homotopy.refl, Path.Homotopy.hcomp, Function.comp, Path.Homotopy.subpathTransSubpath, Fin.castSucc
-- Module: Mathlib.Topology.Subpath
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)))
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))))
⊢ 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)))

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 γ _ _ _)

Premises used: Path.subpath_self, Fin.succ, Path.Homotopy.refl, Path.concat_zero, Path.concat_succ, Fin.reduceLast
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
p : Fin 2 → X
F : (k : Fin 1) → Path (p k.castSucc) (p k.succ)
⊢ (concat p F).Homotopic (F 0)

Tactic:
simpa [concat_succ] using ⟨Homotopy.reflTrans _⟩

Premises used: Path.concat_succ
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
p : Fin 3 → X
F : (k : Fin 2) → Path (p k.castSucc) (p k.succ)
⊢ (concat p F).Homotopic (Path.trans (F 0) (F 1))

Tactic:
simpa [concat_succ] using hcomp ⟨Homotopy.reflTrans _⟩ (refl _)

Premises used: Path.Homotopic.refl, Path.Homotopy.reflTrans, Path.concat_succ, Nonempty.intro, Path.Homotopic.hcomp
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace 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).Homotopic (G k)
⊢ (concat p F).Homotopic (concat p G)

Tactic:
⟨Homotopy.concat p F G (fun k ↦ (h k).some)⟩

Premises used: Nonempty.some, Nonempty.intro, Path.Homotopy.concat, Path.Homotopic
-- Module: Mathlib.Topology.Subpath
Goal:
X : Type u_1
inst : TopologicalSpace X
a b : X
n : ℕ
γ : Path a b
t : Fin (n + 1) → (↑I : Type)
⊢ Homotopic (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)))

Tactic:
⟨Homotopy.concatSubpath γ t⟩

Premises used: Nonempty.intro, Path.Homotopic, Path.Homotopy.concatSubpath
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
Y : Type v
inst_2 : TopologicalSpace Y
inst_3 : TietzeExtension Y
hs : IsClosed[inst] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
⊢ ∃ (g : C(X, Y)), restrict s g = f

Tactic:
TietzeExtension.exists_restrict_eq' s hs f

Premises used: TietzeExtension.exists_restrict_eq'
-- Module: Mathlib.Topology.TietzeExtension
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
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 := ⋯ : C(X₁, X) } = f
⊢ ∃ (g : C(X, Y)), g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } = f

Tactic:
obtain ⟨g, hg⟩ := (f.comp e'.symm).exists_restrict_eq he.isClosed_range

Premises used: ContinuousMap.comp, ContinuousMap.exists_restrict_eq, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.TietzeExtension
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₁))
h :
  ∀ (x : X₁),
    Eq.{v + 1} (α := Y) ((g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } : (a : X₁) → Y) x : Y)
      ((f : (a : X₁) → Y) x : Y)
⊢ g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } = f

Tactic:
ext x
-- Module: Mathlib.Topology.TietzeExtension
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₁))
x : X₁
⊢ Eq.{v + 1} (α := Y) ((g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } : (a : X₁) → Y) x : Y)
    ((f : (a : X₁) → Y) x : Y)

Tactic:
simpa using congr($(hg) ⟨e' x, x, rfl⟩)
-- Module: Mathlib.Topology.TietzeExtension
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 : C(X, Y)), g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } = f

Tactic:
exact ⟨g, by ext x; simpa using congr($(hg) ⟨e' x, x, rfl⟩)⟩
-- Module: Mathlib.Topology.TietzeExtension
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
h : ∀ (x : X₁), Eq.{v + 1} (α := Y) (((⇑g : (a : X) → Y) ∘ e) x : Y) ((f : (a : X₁) → Y) x : Y)
⊢ Eq (α := X₁ → Y) ((⇑g : (a : X) → Y) ∘ e) (⇑f : (a : X₁) → Y)

Tactic:
ext x
-- Module: Mathlib.Topology.TietzeExtension
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
x : X₁
⊢ Eq.{v + 1} (α := Y) (((⇑g : (a : X) → Y) ∘ e) x : Y) ((f : (a : X₁) → Y) x : Y)

Tactic:
congrm($(hg) x)