case a.h.h
X : Type ?u.424517
Y : Type ?u.424520
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type u_2
γ : Path x y
χ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ ↑(trans (Path.pi γ₀) (Path.pi γ₁)) t i = ↑(Path.pi fun i => trans (γ₀ i) (γ₁ i)) t i
X : Type ?u.424517
Y : Type ?u.424520
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type u_2
γ : Path x y
χ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
⊢ trans (Path.pi γ₀) (Path.pi γ₁) = Path.pi fun i => trans (γ₀ i) (γ₁ i)
ext (t i)
case a.h.h
X : Type ?u.424517
Y : Type ?u.424520
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type u_2
γ : Path x y
χ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk
              ((fun t => if t ≤ 1 / 2 then extend (Path.pi γ₀) (2 * t) else extend (Path.pi γ₁) (2 * t - 1)) ∘
                Subtype.val),
          source' :=
            (_ :
              ((fun x => if x ≤ 1 / 2 then extend (Path.pi γ₀) (2 * x) else extend (Path.pi γ₁) (2 * x - 1)) ∘
                    Subtype.val)
                  0 =
                fun i => as i),
          target' :=
            (_ :
              ((fun x => if x ≤ 1 / 2 then extend (Path.pi γ₀) (2 * x) else extend (Path.pi γ₁) (2 * x - 1)) ∘
                    Subtype.val)
                  1 =
                fun i => cs i) }
      t i =
    ↑(Path.pi fun i =>
          {
            toContinuousMap :=
              ContinuousMap.mk
                ((fun t => if t ≤ 1 / 2 then extend (γ₀ i) (2 * t) else extend (γ₁ i) (2 * t - 1)) ∘ Subtype.val),
            source' :=
              (_ :
                ((fun x => if x ≤ 1 / 2 then extend (γ₀ i) (2 * x) else extend (γ₁ i) (2 * x - 1)) ∘ Subtype.val) 0 =
                  as i),
            target' :=
              (_ :
                ((fun x => if x ≤ 1 / 2 then extend (γ₀ i) (2 * x) else extend (γ₁ i) (2 * x - 1)) ∘ Subtype.val) 1 =
                  cs i) })
      t i
case a.h.h
X : Type ?u.424517
Y : Type ?u.424520
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type u_2
γ : Path x y
χ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ ↑(trans (Path.pi γ₀) (Path.pi γ₁)) t i = ↑(Path.pi fun i => trans (γ₀ i) (γ₁ i)) t i
unfold Path.trans
case a.h.h
X : Type ?u.424517
Y : Type ?u.424520
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type u_2
γ : Path x y
χ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ ite (↑t ≤ 1 / 2) (extend (Path.pi γ₀) (2 * ↑t)) (extend (Path.pi γ₁) (2 * ↑t - 1)) i =
    if ↑t ≤ 1 / 2 then extend (γ₀ i) (2 * ↑t) else extend (γ₁ i) (2 * ↑t - 1)
case a.h.h
X : Type ?u.424517
Y : Type ?u.424520
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type u_2
γ : Path x y
χ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk
              ((fun t => if t ≤ 1 / 2 then extend (Path.pi γ₀) (2 * t) else extend (Path.pi γ₁) (2 * t - 1)) ∘
                Subtype.val),
          source' :=
            (_ :
              ((fun x => if x ≤ 1 / 2 then extend (Path.pi γ₀) (2 * x) else extend (Path.pi γ₁) (2 * x - 1)) ∘
                    Subtype.val)
                  0 =
                fun i => as i),
          target' :=
            (_ :
              ((fun x => if x ≤ 1 / 2 then extend (Path.pi γ₀) (2 * x) else extend (Path.pi γ₁) (2 * x - 1)) ∘
                    Subtype.val)
                  1 =
                fun i => cs i) }
      t i =
    ↑(Path.pi fun i =>
          {
            toContinuousMap :=
              ContinuousMap.mk
                ((fun t => if t ≤ 1 / 2 then extend (γ₀ i) (2 * t) else extend (γ₁ i) (2 * t - 1)) ∘ Subtype.val),
            source' :=
              (_ :
                ((fun x => if x ≤ 1 / 2 then extend (γ₀ i) (2 * x) else extend (γ₁ i) (2 * x - 1)) ∘ Subtype.val) 0 =
                  as i),
            target' :=
              (_ :
                ((fun x => if x ≤ 1 / 2 then extend (γ₀ i) (2 * x) else extend (γ₁ i) (2 * x - 1)) ∘ Subtype.val) 1 =
                  cs i) })
      t i
simp only [Path.coe_mk_mk, Function.comp_apply, pi_coe]
no goals
case a.h.h
X : Type ?u.424517
Y : Type ?u.424520
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type u_2
γ : Path x y
χ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ ite (↑t ≤ 1 / 2) (extend (Path.pi γ₀) (2 * ↑t)) (extend (Path.pi γ₁) (2 * ↑t - 1)) i =
    if ↑t ≤ 1 / 2 then extend (γ₀ i) (2 * ↑t) else extend (γ₁ i) (2 * ↑t - 1)
split_ifs <;> rfl