case a.h
X : Type u_1
Y✝ : Type ?u.304721
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x y z : X
ι : Type ?u.304736
γ✝ γ : Path x y
γ' : Path y z
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
h : Continuous f
t : ↑I
⊢ ↑(map (trans γ γ') h) t = ↑(trans (map γ h) (map γ' h)) t
X : Type u_1
Y✝ : Type ?u.304721
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x y z : X
ι : Type ?u.304736
γ✝ γ : Path x y
γ' : Path y z
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
h : Continuous f
⊢ map (trans γ γ') h = trans (map γ h) (map γ' h)
ext t
case a.h
X : Type u_1
Y✝ : Type ?u.304721
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x y z : X
ι : Type ?u.304736
γ✝ γ : Path x y
γ' : Path y z
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
h : Continuous f
t : ↑I
⊢ f
      (if h : ↑t ≤ 1 / 2 then ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
      else ↑γ' { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) }) =
    if h_1 : ↑t ≤ 1 / 2 then ↑(map γ h) { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
    else ↑(map γ' h) { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) }
case a.h
X : Type u_1
Y✝ : Type ?u.304721
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x y z : X
ι : Type ?u.304736
γ✝ γ : Path x y
γ' : Path y z
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
h : Continuous f
t : ↑I
⊢ ↑(map (trans γ γ') h) t = ↑(trans (map γ h) (map γ' h)) t
rw [trans_apply, map_coe, Function.comp_apply, trans_apply]
no goals
case a.h
X : Type u_1
Y✝ : Type ?u.304721
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y✝
x y z : X
ι : Type ?u.304736
γ✝ γ : Path x y
γ' : Path y z
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
h : Continuous f
t : ↑I
⊢ f
      (if h : ↑t ≤ 1 / 2 then ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
      else ↑γ' { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) }) =
    if h_1 : ↑t ≤ 1 / 2 then ↑(map γ h) { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
    else ↑(map γ' h) { val := 2 * ↑t - 1, property := (_ : 2 * ↑t - 1 ∈ I) }
split_ifs <;> rfl