case mk.mk.mk.mk
X : Type u_1
Y : Type ?u.11489
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.11504
x : ↑I → X
h11 : Continuous x
h12 : ContinuousMap.toFun (ContinuousMap.mk x) 0 = x✝
h13 : ContinuousMap.toFun (ContinuousMap.mk x) 1 = y
h21 : Continuous ↑{ toContinuousMap := ContinuousMap.mk x, source' := h12, target' := h13 }
h22 :
  ContinuousMap.toFun (ContinuousMap.mk ↑{ toContinuousMap := ContinuousMap.mk x, source' := h12, target' := h13 }) 0 =
    x✝
h23 :
  ContinuousMap.toFun (ContinuousMap.mk ↑{ toContinuousMap := ContinuousMap.mk x, source' := h12, target' := h13 }) 1 =
    y
⊢ { toContinuousMap := ContinuousMap.mk x, source' := h12, target' := h13 } =
    { toContinuousMap := ContinuousMap.mk ↑{ toContinuousMap := ContinuousMap.mk x, source' := h12, target' := h13 },
      source' := h22, target' := h23 }
X : Type u_1
Y : Type ?u.11489
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.11504
⊢ ∀ {γ₁ γ₂ : Path x y}, ↑γ₁ = ↑γ₂ → γ₁ = γ₂
rintro ⟨⟨x, h11⟩, h12, h13⟩ ⟨⟨x, h21⟩, h22, h23⟩ rfl
no goals
case mk.mk.mk.mk
X : Type u_1
Y : Type ?u.11489
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.11504
x : ↑I → X
h11 : Continuous x
h12 : ContinuousMap.toFun (ContinuousMap.mk x) 0 = x✝
h13 : ContinuousMap.toFun (ContinuousMap.mk x) 1 = y
h21 : Continuous ↑{ toContinuousMap := ContinuousMap.mk x, source' := h12, target' := h13 }
h22 :
  ContinuousMap.toFun (ContinuousMap.mk ↑{ toContinuousMap := ContinuousMap.mk x, source' := h12, target' := h13 }) 0 =
    x✝
h23 :
  ContinuousMap.toFun (ContinuousMap.mk ↑{ toContinuousMap := ContinuousMap.mk x, source' := h12, target' := h13 }) 1 =
    y
⊢ { toContinuousMap := ContinuousMap.mk x, source' := h12, target' := h13 } =
    { toContinuousMap := ContinuousMap.mk ↑{ toContinuousMap := ContinuousMap.mk x, source' := h12, target' := h13 },
      source' := h22, target' := h23 }
rfl