case a.h
X✝ : Type ?u.252121
Y : Type ?u.252124
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252139
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ ↑(trans (refl a) (refl a)) x✝ = ↑(refl a) x✝
X✝ : Type ?u.252121
Y : Type ?u.252124
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252139
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a : X
⊢ trans (refl a) (refl a) = refl a
ext
case a.h
X✝ : Type ?u.252121
Y : Type ?u.252124
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252139
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ ↑{ toContinuousMap := ContinuousMap.mk ((fun t => a) ∘ Subtype.val),
          source' := (_ : ContinuousMap.toFun (ContinuousMap.mk ((fun t => a) ∘ Subtype.val)) 0 = a),
          target' := (_ : ContinuousMap.toFun (ContinuousMap.mk ((fun t => a) ∘ Subtype.val)) 1 = a) }
      x✝ =
    ↑(refl a) x✝
case a.h
X✝ : Type ?u.252121
Y : Type ?u.252124
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252139
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ ↑(trans (refl a) (refl a)) x✝ = ↑(refl a) x✝
simp only [Path.trans, ite_self, one_div, Path.refl_extend]
no goals
case a.h
X✝ : Type ?u.252121
Y : Type ?u.252124
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252139
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ ↑{ toContinuousMap := ContinuousMap.mk ((fun t => a) ∘ Subtype.val),
          source' := (_ : ContinuousMap.toFun (ContinuousMap.mk ((fun t => a) ∘ Subtype.val)) 0 = a),
          target' := (_ : ContinuousMap.toFun (ContinuousMap.mk ((fun t => a) ∘ Subtype.val)) 1 = a) }
      x✝ =
    ↑(refl a) x✝
rfl