case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ ↑(delayReflRight 0 γ) t = ↑(trans γ (refl y)) t
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflRight 0 γ = trans γ (refl y)
ext t
case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ ↑γ (qRight (t, 0)) = if h : ↑t ≤ 1 / 2 then ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) } else y
case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ ↑(delayReflRight 0 γ) t = ↑(trans γ (refl y)) t
simp only [delayReflRight, trans_apply, refl_extend, Path.coe_mk_mk, Function.comp_apply,
  refl_apply]
case a.h.inl
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }

case a.h.inr
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = y
case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ ↑γ (qRight (t, 0)) = if h : ↑t ≤ 1 / 2 then ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) } else y
split_ifs with h
case a.h.inr
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = y

case a.h.inl
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
case a.h.inl
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }

case a.h.inr
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = y
swap
case a.h.inr
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ 1

case a.h.inl
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
case a.h.inr
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = y

case a.h.inl
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
conv_rhs => rw [← γ.target]
case a.h.inr.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑1

case a.h.inl.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑{ val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
case a.h.inr
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ 1

case a.h.inl
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
all_goals apply congr_arg γ; ext1; rw [qRight_zero_right]
no goals
case a.h.inr.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑1

case a.h.inl.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑{ val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
exacts [if_neg h, if_pos h]
case a.h.inl
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ qRight (t, 0) = { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
case a.h.inl
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
apply congr_arg γ
case a.h.inl.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑(qRight (t, 0)) = ↑{ val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
case a.h.inl
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ qRight (t, 0) = { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
ext1
case a.h.inl.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑{ val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
case a.h.inl.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑(qRight (t, 0)) = ↑{ val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
rw [qRight_zero_right]