no goals
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }
continuity
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ ↑(Path.trans p (Path.refl x₁)) x✝ =
    ↑(Path.reparam p (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) })
          (_ : Continuous fun x => { val := transReflReparamAux x, property := (_ : transReflReparamAux x ∈ I) })
          (_ : (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }) 0 = 0)
          (_ : (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }) 1 = 1))
      x✝
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Path.trans p (Path.refl x₁) =
    Path.reparam p (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) })
      (_ : Continuous fun x => { val := transReflReparamAux x, property := (_ : transReflReparamAux x ∈ I) })
      (_ : (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }) 0 = 0)
      (_ : (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }) 1 = 1)
ext
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ ↑(Path.trans p (Path.refl x₁)) x✝ =
    ↑(Path.reparam p (fun t => { val := if ↑t ≤ 1 / 2 then 2 * ↑t else 1, property := (_ : transReflReparamAux t ∈ I) })
          (_ :
            Continuous fun x =>
              { val := if ↑x ≤ 1 / 2 then 2 * ↑x else 1, property := (_ : transReflReparamAux x ∈ I) })
          (_ :
            (fun t => { val := if ↑t ≤ 1 / 2 then 2 * ↑t else 1, property := (_ : transReflReparamAux t ∈ I) }) 0 = 0)
          (_ :
            (fun t => { val := if ↑t ≤ 1 / 2 then 2 * ↑t else 1, property := (_ : transReflReparamAux t ∈ I) }) 1 = 1))
      x✝
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ ↑(Path.trans p (Path.refl x₁)) x✝ =
    ↑(Path.reparam p (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) })
          (_ : Continuous fun x => { val := transReflReparamAux x, property := (_ : transReflReparamAux x ∈ I) })
          (_ : (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }) 0 = 0)
          (_ : (fun t => { val := transReflReparamAux t, property := (_ : transReflReparamAux t ∈ I) }) 1 = 1))
      x✝
unfold transReflReparamAux
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (if h : ↑x✝ ≤ 2⁻¹ then ↑p { val := 2 * ↑x✝, property := (_ : 2 * ↑x✝ ∈ I) } else x₁) =
    ↑p
      { val := if ↑x✝ ≤ 2⁻¹ then 2 * ↑x✝ else 1, property := (_ : (fun x => x ∈ I) (if ↑x✝ ≤ 2⁻¹ then 2 * ↑x✝ else 1)) }
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ ↑(Path.trans p (Path.refl x₁)) x✝ =
    ↑(Path.reparam p (fun t => { val := if ↑t ≤ 1 / 2 then 2 * ↑t else 1, property := (_ : transReflReparamAux t ∈ I) })
          (_ :
            Continuous fun x =>
              { val := if ↑x ≤ 1 / 2 then 2 * ↑x else 1, property := (_ : transReflReparamAux x ∈ I) })
          (_ :
            (fun t => { val := if ↑t ≤ 1 / 2 then 2 * ↑t else 1, property := (_ : transReflReparamAux t ∈ I) }) 0 = 0)
          (_ :
            (fun t => { val := if ↑t ≤ 1 / 2 then 2 * ↑t else 1, property := (_ : transReflReparamAux t ∈ I) }) 1 = 1))
      x✝
simp only [Path.trans_apply, not_le, coe_reparam, Function.comp_apply, one_div, Path.refl_apply]
case a.h.inl.inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ↑x✝ ≤ 2⁻¹
h✝ : ↑x✝ ≤ 2⁻¹
⊢ ↑p { val := 2 * ↑x✝, property := (_ : 2 * ↑x✝ ∈ I) } =
    ↑p { val := 2 * ↑x✝, property := (_ : (fun x => x ∈ I) (2 * ↑x✝)) }

case a.h.inl.inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ↑x✝ ≤ 2⁻¹
h✝ : ¬↑x✝ ≤ 2⁻¹
⊢ ↑p { val := 2 * ↑x✝, property := (_ : 2 * ↑x✝ ∈ I) } =
    ↑p { val := 2 * ↑x✝, property := (_ : (fun x => x ∈ I) (2 * ↑x✝)) }

case a.h.inr.inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ¬↑x✝ ≤ 2⁻¹
h✝ : ↑x✝ ≤ 2⁻¹
⊢ x₁ = ↑p { val := 1, property := (_ : (fun x => x ∈ I) 1) }

case a.h.inr.inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ¬↑x✝ ≤ 2⁻¹
h✝ : ¬↑x✝ ≤ 2⁻¹
⊢ x₁ = ↑p { val := 1, property := (_ : (fun x => x ∈ I) 1) }
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (if h : ↑x✝ ≤ 2⁻¹ then ↑p { val := 2 * ↑x✝, property := (_ : 2 * ↑x✝ ∈ I) } else x₁) =
    ↑p
      { val := if ↑x✝ ≤ 2⁻¹ then 2 * ↑x✝ else 1, property := (_ : (fun x => x ∈ I) (if ↑x✝ ≤ 2⁻¹ then 2 * ↑x✝ else 1)) }
split_ifs
no goals
case a.h.inl.inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ↑x✝ ≤ 2⁻¹
h✝ : ↑x✝ ≤ 2⁻¹
⊢ ↑p { val := 2 * ↑x✝, property := (_ : 2 * ↑x✝ ∈ I) } =
    ↑p { val := 2 * ↑x✝, property := (_ : (fun x => x ∈ I) (2 * ↑x✝)) }
rfl
no goals
case a.h.inl.inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ↑x✝ ≤ 2⁻¹
h✝ : ¬↑x✝ ≤ 2⁻¹
⊢ ↑p { val := 2 * ↑x✝, property := (_ : 2 * ↑x✝ ∈ I) } =
    ↑p { val := 2 * ↑x✝, property := (_ : (fun x => x ∈ I) (2 * ↑x✝)) }
rfl
no goals
case a.h.inr.inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ¬↑x✝ ≤ 2⁻¹
h✝ : ↑x✝ ≤ 2⁻¹
⊢ x₁ = ↑p { val := 1, property := (_ : (fun x => x ∈ I) 1) }
simp
no goals
case a.h.inr.inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ¬↑x✝ ≤ 2⁻¹
h✝ : ¬↑x✝ ≤ 2⁻¹
⊢ x₁ = ↑p { val := 1, property := (_ : (fun x => x ∈ I) 1) }
simp