[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous reflTransSymmAux
[PROOFSTEP]
refine' continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _
[GOAL]
case refine'_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.snd
[PROOFSTEP]
continuity
[GOAL]
case refine'_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 2
[PROOFSTEP]
continuity
[GOAL]
case refine'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.fst * 2 * ↑x.snd
[PROOFSTEP]
continuity
[GOAL]
case refine'_4
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x.fst * (2 - 2 * ↑x.snd)
[PROOFSTEP]
continuity
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I × ↑I), ↑x.snd = 1 / 2 → ↑x.fst * 2 * ↑x.snd = ↑x.fst * (2 - 2 * ↑x.snd)
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
hx : ↑x.snd = 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd = ↑x.fst * (2 - 2 * ↑x.snd)
[PROOFSTEP]
rw [hx, mul_assoc]
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
hx : ↑x.snd = 1 / 2
⊢ ↑x.fst * (2 * (1 / 2)) = ↑x.fst * (2 - 2 * (1 / 2))
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
⊢ reflTransSymmAux x ∈ I
[PROOFSTEP]
dsimp only [reflTransSymmAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
⊢ (if ↑x.snd ≤ 1 / 2 then ↑x.fst * 2 * ↑x.snd else ↑x.fst * (2 - 2 * ↑x.snd)) ∈ I
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd ∈ I
[PROOFSTEP]
constructor
[GOAL]
case pos.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * 2 * ↑x.snd
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case pos.left.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * 2
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case pos.left.ha.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst
[PROOFSTEP]
unit_interval
[GOAL]
case pos.left.ha.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
case pos.left.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.snd
[PROOFSTEP]
unit_interval
[GOAL]
case pos.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * 2 * ↑x.snd ≤ 1
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case pos.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 * ↑x.snd) ≤ 1
[PROOFSTEP]
apply mul_le_one
[GOAL]
case pos.right.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ ↑x.fst ≤ 1
[PROOFSTEP]
unit_interval
[GOAL]
case pos.right.hb'
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 * ↑x.snd
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case pos.right.hb'.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
case pos.right.hb'.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.snd
[PROOFSTEP]
unit_interval
[GOAL]
case pos.right.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ↑x.snd ≤ 1 / 2
⊢ 2 * ↑x.snd ≤ 1
[PROOFSTEP]
linarith
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 - 2 * ↑x.snd) ∈ I
[PROOFSTEP]
constructor
[GOAL]
case neg.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst * (2 - 2 * ↑x.snd)
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case neg.left.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ ↑x.fst
[PROOFSTEP]
unit_interval
[GOAL]
case neg.left.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.snd
[PROOFSTEP]
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
[GOAL]
case neg.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst * (2 - 2 * ↑x.snd) ≤ 1
[PROOFSTEP]
apply mul_le_one
[GOAL]
case neg.right.ha
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ ↑x.fst ≤ 1
[PROOFSTEP]
unit_interval
[GOAL]
case neg.right.hb'
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 0 ≤ 2 - 2 * ↑x.snd
[PROOFSTEP]
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
[GOAL]
case neg.right.hb
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I × ↑I
h✝ : ¬↑x.snd ≤ 1 / 2
⊢ 2 - 2 * ↑x.snd ≤ 1
[PROOFSTEP]
linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous fun x => ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) }
[PROOFSTEP]
continuity
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ ∀ (x : ↑I),
    ContinuousMap.toFun
        (ContinuousMap.mk fun x => ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) }) (0, x) =
      ↑(Path.refl x₀).toContinuousMap x
[PROOFSTEP]
simp [reflTransSymmAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
⊢ ContinuousMap.toFun
      (ContinuousMap.mk fun x => ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) }) (1, x) =
    ↑(Path.trans p (Path.symm p)).toContinuousMap x
[PROOFSTEP]
dsimp only [reflTransSymmAux, Path.coe_toContinuousMap, Path.trans]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
⊢ ↑p { val := if ↑x ≤ 1 / 2 then ↑1 * 2 * ↑x else ↑1 * (2 - 2 * ↑x), property := (_ : reflTransSymmAux (1, x) ∈ I) } =
    ↑(ContinuousMap.mk
          ((fun t => if t ≤ 1 / 2 then extend p (2 * t) else extend (Path.symm p) (2 * t - 1)) ∘ Subtype.val))
      x
[PROOFSTEP]
change _ = ite _ _ _
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
⊢ ↑p { val := if ↑x ≤ 1 / 2 then ↑1 * 2 * ↑x else ↑1 * (2 - 2 * ↑x), property := (_ : reflTransSymmAux (1, x) ∈ I) } =
    if ↑x ≤ 1 / 2 then extend p (2 * ↑x) else extend (Path.symm p) (2 * ↑x - 1)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ↑x ≤ 1 / 2
⊢ ↑p { val := ↑1 * 2 * ↑x, property := (_ : (fun x => x ∈ I) (↑1 * 2 * ↑x)) } = extend p (2 * ↑x)
[PROOFSTEP]
rw [Path.extend, Set.IccExtend_of_mem]
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ↑x ≤ 1 / 2
⊢ ↑p { val := ↑1 * 2 * ↑x, property := (_ : (fun x => x ∈ I) (↑1 * 2 * ↑x)) } =
    ↑p { val := 2 * ↑x, property := ?pos.hx✝ }
[PROOFSTEP]
norm_num
[GOAL]
case pos.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ↑x ≤ 1 / 2
⊢ 2 * ↑x ∈ Set.Icc 0 1
[PROOFSTEP]
rw [unitInterval.mul_pos_mem_iff zero_lt_two]
[GOAL]
case pos.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ↑x ≤ 1 / 2
⊢ ↑x ∈ Set.Icc 0 (1 / 2)
[PROOFSTEP]
exact ⟨unitInterval.nonneg x, h⟩
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ ↑p { val := ↑1 * (2 - 2 * ↑x), property := (_ : (fun x => x ∈ I) (↑1 * (2 - 2 * ↑x))) } =
    extend (Path.symm p) (2 * ↑x - 1)
[PROOFSTEP]
rw [Path.symm, Path.extend, Set.IccExtend_of_mem]
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ ↑p { val := ↑1 * (2 - 2 * ↑x), property := (_ : (fun x => x ∈ I) (↑1 * (2 - 2 * ↑x))) } =
    ↑{ toContinuousMap := ContinuousMap.mk (↑p ∘ σ),
          source' := (_ : ContinuousMap.toFun (ContinuousMap.mk (↑p ∘ σ)) 0 = x₁),
          target' := (_ : ContinuousMap.toFun (ContinuousMap.mk (↑p ∘ σ)) 1 = x₀) }
      { val := 2 * ↑x - 1, property := ?neg.hx✝ }
[PROOFSTEP]
simp only [Set.Icc.coe_one, one_mul, coe_mk_mk, Function.comp_apply]
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ ↑p { val := 2 - 2 * ↑x, property := (_ : (fun x => x ∈ I) (2 - 2 * ↑x)) } =
    ↑p (σ { val := 2 * ↑x - 1, property := ?neg.hx✝ })
[PROOFSTEP]
congr 1
[GOAL]
case neg.h.e_6.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ { val := 2 - 2 * ↑x, property := (_ : (fun x => x ∈ I) (2 - 2 * ↑x)) } = σ { val := 2 * ↑x - 1, property := ?neg.hx✝ }
[PROOFSTEP]
ext
  -- Porting note: norm_num ignores arguments.
[GOAL]
case neg.h.e_6.h.a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ ↑{ val := 2 - 2 * ↑x, property := (_ : (fun x => x ∈ I) (2 - 2 * ↑x)) } =
    ↑(σ { val := 2 * ↑x - 1, property := ?neg.hx✝ })
[PROOFSTEP]
simp [sub_sub_eq_add_sub]
[GOAL]
case neg.h.e_6.h.a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ 2 = 1 + 1
[PROOFSTEP]
norm_num
[GOAL]
case neg.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ 2 * ↑x - 1 ∈ Set.Icc 0 1
[PROOFSTEP]
rw [unitInterval.two_mul_sub_one_mem_iff]
[GOAL]
case neg.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
h : ¬↑x ≤ 1 / 2
⊢ ↑x ∈ Set.Icc (1 / 2) 1
[PROOFSTEP]
exact ⟨(not_le.1 h).le, unitInterval.le_one x⟩
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x ∈ {0, 1}
⊢ ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              {
                  toContinuousMap :=
                    ContinuousMap.mk fun x =>
                      ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) },
                  map_zero_left :=
                    (_ :
                      ∀ (a : ↑I),
                        ↑p { val := reflTransSymmAux (0, a), property := (_ : reflTransSymmAux (0, a) ∈ I) } = x₀),
                  map_one_left :=
                    (_ :
                      ∀ (x : ↑I),
                        ContinuousMap.toFun
                            (ContinuousMap.mk fun x =>
                              ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) })
                            (1, x) =
                          ↑(Path.trans p (Path.symm p)).toContinuousMap x) }.toContinuousMap
              (t, x))
        x =
      ↑(Path.refl x₀).toContinuousMap x ∧
    ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              {
                  toContinuousMap :=
                    ContinuousMap.mk fun x =>
                      ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) },
                  map_zero_left :=
                    (_ :
                      ∀ (a : ↑I),
                        ↑p { val := reflTransSymmAux (0, a), property := (_ : reflTransSymmAux (0, a) ∈ I) } = x₀),
                  map_one_left :=
                    (_ :
                      ∀ (x : ↑I),
                        ContinuousMap.toFun
                            (ContinuousMap.mk fun x =>
                              ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) })
                            (1, x) =
                          ↑(Path.trans p (Path.symm p)).toContinuousMap x) }.toContinuousMap
              (t, x))
        x =
      ↑(Path.trans p (Path.symm p)).toContinuousMap x
[PROOFSTEP]
simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at hx 
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0 ∨ x = 1
⊢ ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              {
                  toContinuousMap :=
                    ContinuousMap.mk fun x =>
                      ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) },
                  map_zero_left :=
                    (_ :
                      ∀ (a : ↑I),
                        ↑p { val := reflTransSymmAux (0, a), property := (_ : reflTransSymmAux (0, a) ∈ I) } = x₀),
                  map_one_left :=
                    (_ :
                      ∀ (x : ↑I),
                        ContinuousMap.toFun
                            (ContinuousMap.mk fun x =>
                              ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) })
                            (1, x) =
                          ↑(Path.trans p (Path.symm p)).toContinuousMap x) }.toContinuousMap
              (t, x))
        x =
      ↑(Path.refl x₀).toContinuousMap x ∧
    ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              {
                  toContinuousMap :=
                    ContinuousMap.mk fun x =>
                      ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) },
                  map_zero_left :=
                    (_ :
                      ∀ (a : ↑I),
                        ↑p { val := reflTransSymmAux (0, a), property := (_ : reflTransSymmAux (0, a) ∈ I) } = x₀),
                  map_one_left :=
                    (_ :
                      ∀ (x : ↑I),
                        ContinuousMap.toFun
                            (ContinuousMap.mk fun x =>
                              ↑p { val := reflTransSymmAux x, property := (_ : reflTransSymmAux x ∈ I) })
                            (1, x) =
                          ↑(Path.trans p (Path.symm p)).toContinuousMap x) }.toContinuousMap
              (t, x))
        x =
      ↑(Path.trans p (Path.symm p)).toContinuousMap x
[PROOFSTEP]
simp only [ContinuousMap.coe_mk, coe_toContinuousMap, Path.refl_apply]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0 ∨ x = 1
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]
cases hx with
| inl hx| inr hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0 ∨ x = 1
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]
cases hx with
| inl hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
| inr hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0 ∨ x = 1
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]
cases hx with
| inl hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
| inr hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
[GOAL]
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]

| inl hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
[GOAL]
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]
rw [hx]
[GOAL]
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0
⊢ ↑p { val := reflTransSymmAux (t, 0), property := (_ : reflTransSymmAux (t, 0) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, 0), property := (_ : reflTransSymmAux (t, 0) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) 0
[PROOFSTEP]
simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
  sub_self, Path.source, Path.target, and_self]
[GOAL]
case inl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 0
⊢ ↑p { val := if 0 ≤ 2 then 0 else ↑t * 2, property := (_ : (fun x => x ∈ I) (if 0 ≤ 2 then 0 else ↑t * 2)) } = x₀
[PROOFSTEP]
norm_num
[GOAL]
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 1
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]

| inr hx =>
  rw [hx]
  simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
    sub_self, Path.source, Path.target, and_self]
  norm_num
[GOAL]
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 1
⊢ ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, x), property := (_ : reflTransSymmAux (t, x) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) x
[PROOFSTEP]
rw [hx]
[GOAL]
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 1
⊢ ↑p { val := reflTransSymmAux (t, 1), property := (_ : reflTransSymmAux (t, 1) ∈ I) } = x₀ ∧
    ↑p { val := reflTransSymmAux (t, 1), property := (_ : reflTransSymmAux (t, 1) ∈ I) } =
      ↑(Path.trans p (Path.symm p)) 1
[PROOFSTEP]
simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one, inv_nonneg, mul_zero, sub_zero,
  sub_self, Path.source, Path.target, and_self]
[GOAL]
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t x : ↑I
hx : x = 1
⊢ ↑p { val := if 1 ≤ 2⁻¹ then ↑t * 2 else 0, property := (_ : (fun x => x ∈ I) (if 1 ≤ 2⁻¹ then ↑t * 2 else 0)) } = x₀
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous transReflReparamAux
[PROOFSTEP]
refine' continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _ <;> [continuity; continuity;
  continuity; continuity; skip]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous transReflReparamAux
[PROOFSTEP]
refine' continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _
[GOAL]
case refine'_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x
[PROOFSTEP]
continuity
[GOAL]
case refine'_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 2
[PROOFSTEP]
continuity
[GOAL]
case refine'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 2 * ↑x
[PROOFSTEP]
continuity
[GOAL]
case refine'_4
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1
[PROOFSTEP]
continuity
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1
[PROOFSTEP]
skip
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 2
⊢ 2 * ↑x = 1
[PROOFSTEP]
simp [hx]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
⊢ transReflReparamAux t ∈ I
[PROOFSTEP]
unfold transReflReparamAux
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) ∈ I
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ∈ I
[PROOFSTEP]
constructor
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ∈ I
[PROOFSTEP]
constructor
[GOAL]
case pos.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ 2 * ↑t
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case pos.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case neg.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case neg.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ transReflReparamAux 0 = 0
[PROOFSTEP]
simp [transReflReparamAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ 2 < 0 → False
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ transReflReparamAux 1 = 1
[PROOFSTEP]
simp [transReflReparamAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ 1 ≤ 2⁻¹ → False
[PROOFSTEP]
norm_num
[GOAL]
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) }
[PROOFSTEP]
continuity
[GOAL]
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)
[PROOFSTEP]
ext
[GOAL]
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✝
[PROOFSTEP]
unfold transReflReparamAux
[GOAL]
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✝
[PROOFSTEP]
simp only [Path.trans_apply, not_le, coe_reparam, Function.comp_apply, one_div, Path.refl_apply]
[GOAL]
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)) }
[PROOFSTEP]
split_ifs
[GOAL]
case pos
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✝)) }
[PROOFSTEP]
rfl
[GOAL]
case neg
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✝)) }
[PROOFSTEP]
rfl
[GOAL]
case pos
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) }
[PROOFSTEP]
simp
[GOAL]
case neg
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) }
[PROOFSTEP]
simp
[GOAL]
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) }
[PROOFSTEP]
continuity
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Path.symm (Path.trans (Path.symm p) (Path.refl x₀)) = Path.trans (Path.refl x₀) p
[PROOFSTEP]
simp
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Path.symm (Path.symm p) = p
[PROOFSTEP]
simp
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous transAssocReparamAux
[PROOFSTEP]
refine'
    continuous_if_le _ _ (Continuous.continuousOn _)
      (continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _).continuousOn _ <;>
  [continuity; continuity; continuity; continuity; continuity; continuity; continuity; skip; skip]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous transAssocReparamAux
[PROOFSTEP]
refine'
  continuous_if_le _ _ (Continuous.continuousOn _)
    (continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _).continuousOn _
[GOAL]
case refine'_1
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x
[PROOFSTEP]
continuity
[GOAL]
case refine'_2
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 4
[PROOFSTEP]
continuity
[GOAL]
case refine'_3
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 2 * ↑x
[PROOFSTEP]
continuity
[GOAL]
case refine'_4
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x
[PROOFSTEP]
continuity
[GOAL]
case refine'_5
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 2
[PROOFSTEP]
continuity
[GOAL]
case refine'_6
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => ↑x + 1 / 4
[PROOFSTEP]
continuity
[GOAL]
case refine'_7
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ Continuous fun x => 1 / 2 * (↑x + 1)
[PROOFSTEP]
continuity
[GOAL]
case refine'_8
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 2 → ↑x + 1 / 4 = 1 / 2 * (↑x + 1)
[PROOFSTEP]
skip
[GOAL]
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 4 → 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)
[PROOFSTEP]
skip
[GOAL]
case refine'_8
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 2 → ↑x + 1 / 4 = 1 / 2 * (↑x + 1)
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_8
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 2
⊢ ↑x + 1 / 4 = 1 / 2 * (↑x + 1)
[PROOFSTEP]
simp [hx]
[GOAL]
case refine'_8
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 2
⊢ 2⁻¹ + 4⁻¹ = 2⁻¹ * (2⁻¹ + 1)
[PROOFSTEP]
norm_num
[GOAL]
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ (x : ↑I), ↑x = 1 / 4 → 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 4
⊢ 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)
[PROOFSTEP]
simp [hx]
[GOAL]
case refine'_9
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x : ↑I
hx : ↑x = 1 / 4
⊢ 2 * 4⁻¹ = if 4⁻¹ ≤ 2⁻¹ then 4⁻¹ + 4⁻¹ else 2⁻¹ * (4⁻¹ + 1)
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
⊢ transAssocReparamAux t ∈ I
[PROOFSTEP]
unfold transAssocReparamAux
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
⊢ (if ↑t ≤ 1 / 4 then 2 * ↑t else if ↑t ≤ 1 / 2 then ↑t + 1 / 4 else 1 / 2 * (↑t + 1)) ∈ I
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ∈ I
[PROOFSTEP]
constructor
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ∈ I
[PROOFSTEP]
constructor
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ∈ I
[PROOFSTEP]
constructor
[GOAL]
case pos.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 0 ≤ 2 * ↑t
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case pos.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case pos.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ ↑t + 1 / 4
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case pos.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case neg.left
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1 / 2 * (↑t + 1)
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
case neg.right
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ≤ 1
[PROOFSTEP]
linarith [unitInterval.le_one t, unitInterval.nonneg t]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ transAssocReparamAux 0 = 0
[PROOFSTEP]
simp [transAssocReparamAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ 4 < 0 → (if 0 ≤ 2 then 4⁻¹ else 2⁻¹) = 0
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ transAssocReparamAux 1 = 1
[PROOFSTEP]
simp [transAssocReparamAux]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ (if 1 ≤ 4⁻¹ then 2 else if 1 ≤ 2⁻¹ then 1 + 4⁻¹ else 2⁻¹ * (1 + 1)) = 1
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ Continuous fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }
[PROOFSTEP]
continuity
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ Path.trans (Path.trans p q) r =
    Path.reparam (Path.trans p (Path.trans q r))
      (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) })
      (_ : Continuous fun x => { val := transAssocReparamAux x, property := (_ : transAssocReparamAux x ∈ I) })
      (_ : (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }) 0 = 0)
      (_ : (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }) 1 = 1)
[PROOFSTEP]
ext x
[GOAL]
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
⊢ ↑(Path.trans (Path.trans p q) r) x =
    ↑(Path.reparam (Path.trans p (Path.trans q r))
          (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) })
          (_ : Continuous fun x => { val := transAssocReparamAux x, property := (_ : transAssocReparamAux x ∈ I) })
          (_ : (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }) 0 = 0)
          (_ : (fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }) 1 = 1))
      x
[PROOFSTEP]
simp only [transAssocReparamAux, Path.trans_apply, mul_inv_cancel_left₀, not_le, Function.comp_apply, Ne.def,
  not_false_iff, bit0_eq_zero, one_ne_zero, mul_ite, Subtype.coe_mk, Path.coe_reparam]
  -- TODO: why does split_ifs not reduce the ifs??????
[GOAL]
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
⊢ (if h : ↑x ≤ 1 / 2 then
      if h_1 : 2 * ↑x ≤ 1 / 2 then
        ↑p { val := 2 * (2 * ↑x), property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } ∈ I) }
      else
        ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) }
    else ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) }) =
    if h : (if ↑x ≤ 1 / 4 then 2 * ↑x else if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)) ≤ 1 / 2 then
      ↑p
        { val := if ↑x ≤ 1 / 4 then 2 * (2 * ↑x) else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1)),
          property :=
            (_ :
              (fun x => x ∈ I)
                (if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1)))) }
    else
      if h_1 :
          (if ↑x ≤ 1 / 4 then 2 * (2 * ↑x) else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) - 1 ≤
            1 / 2 then
        ↑q
          {
            val :=
              2 *
                ((if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                  else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                  1),
            property :=
              (_ :
                2 *
                    ↑{
                        val :=
                          (if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                            else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                            1,
                        property :=
                          (_ :
                            (fun x => x ∈ I)
                              ((if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                                else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                                1)) } ∈
                  I) }
      else
        ↑r
          {
            val :=
              2 *
                  ((if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                    else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                    1) -
                1,
            property :=
              (_ :
                2 *
                      ↑{
                          val :=
                            (if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                              else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                              1,
                          property :=
                            (_ :
                              (fun x => x ∈ I)
                                ((if ↑x ≤ 1 / 4 then 2 * (2 * ↑x)
                                  else if ↑x ≤ 1 / 2 then 2 * (↑x + 1 / 4) else 2 * (1 / 2 * (↑x + 1))) -
                                  1)) } -
                    1 ∈
                  I) }
[PROOFSTEP]
split_ifs with h₁ h₂ h₃ h₄ h₅
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ↑x ≤ 1 / 4
⊢ ↑p { val := 2 * (2 * ↑x), property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } ∈ I) } =
    ↑p { val := 2 * (2 * ↑x), property := (_ : (fun x => x ∈ I) (2 * (2 * ↑x))) }
[PROOFSTEP]
rfl
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ↑x + 1 / 4 ≤ 1 / 2
⊢ ↑p { val := 2 * (2 * ↑x), property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } ∈ I) } =
    ↑p { val := 2 * (↑x + 1 / 4), property := (_ : (fun x => x ∈ I) (2 * (↑x + 1 / 4))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ↑x + 1 / 4 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ¬↑x + 1 / 4 ≤ 1 / 2
h₅ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ ↑p { val := 2 * (2 * ↑x), property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } ∈ I) } =
    ↑q { val := 2 * (2 * (↑x + 1 / 4) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (↑x + 1 / 4) - 1))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ¬↑x + 1 / 4 ≤ 1 / 2
h₅ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ¬↑x + 1 / 4 ≤ 1 / 2
h₅ : ¬2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ ↑p { val := 2 * (2 * ↑x), property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } ∈ I) } =
    ↑r { val := 2 * (2 * (↑x + 1 / 4) - 1) - 1, property := (_ : (fun x => x ∈ I) (2 * (2 * (↑x + 1 / 4) - 1) - 1)) }
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : 2 * ↑x ≤ 1 / 2
h₃ : ¬↑x ≤ 1 / 4
h₄ : ¬↑x + 1 / 4 ≤ 1 / 2
h₅ : ¬2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑q { val := 2 * (2 * (2 * ↑x) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (2 * ↑x) - 1))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑r { val := 2 * (2 * (2 * ↑x) - 1) - 1, property := (_ : (fun x => x ∈ I) (2 * (2 * (2 * ↑x) - 1) - 1)) }
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : ↑x + 1 / 4 ≤ 1 / 2
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑p { val := 2 * (↑x + 1 / 4), property := (_ : (fun x => x ∈ I) (2 * (↑x + 1 / 4))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : ↑x + 1 / 4 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑q { val := 2 * (2 * (↑x + 1 / 4) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (↑x + 1 / 4) - 1))) }
[PROOFSTEP]
have h : 2 * (2 * (x : ℝ)) - 1 = 2 * (2 * (↑x + 1 / 4) - 1) := by linarith
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ 2 * (2 * ↑x) - 1 = 2 * (2 * (↑x + 1 / 4) - 1)
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
h : 2 * (2 * ↑x) - 1 = 2 * (2 * (↑x + 1 / 4) - 1)
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑q { val := 2 * (2 * (↑x + 1 / 4) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (↑x + 1 / 4) - 1))) }
[PROOFSTEP]
simp [h₂, h₁, h, dif_neg (show ¬False from id), dif_pos True.intro, if_false, if_true]
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : ¬2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ ↑q { val := 2 * (2 * ↑x) - 1, property := (_ : 2 * ↑{ val := 2 * ↑x, property := (_ : 2 * ↑x ∈ I) } - 1 ∈ I) } =
    ↑r { val := 2 * (2 * (↑x + 1 / 4) - 1) - 1, property := (_ : (fun x => x ∈ I) (2 * (2 * (↑x + 1 / 4) - 1) - 1)) }
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ↑x ≤ 1 / 2
h₂ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : ¬2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * ↑x ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑p { val := 2 * (2 * ↑x), property := (_ : (fun x => x ∈ I) (2 * (2 * ↑x))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * ↑x ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑q { val := 2 * (2 * (2 * ↑x) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (2 * ↑x) - 1))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑r { val := 2 * (2 * (2 * ↑x) - 1) - 1, property := (_ : (fun x => x ∈ I) (2 * (2 * (2 * ↑x) - 1) - 1)) }
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑p { val := 2 * (1 / 2 * (↑x + 1)), property := (_ : (fun x => x ∈ I) (2 * (1 / 2 * (↑x + 1)))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑q
      { val := 2 * (2 * (1 / 2 * (↑x + 1)) - 1), property := (_ : (fun x => x ∈ I) (2 * (2 * (1 / 2 * (↑x + 1)) - 1))) }
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ ↑r { val := 2 * ↑x - 1, property := (_ : 2 * ↑x - 1 ∈ I) } =
    ↑r
      { val := 2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1,
        property := (_ : (fun x => x ∈ I) (2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1)) }
[PROOFSTEP]
congr
[GOAL]
case neg.h.e_6.h.e_val.e_a.e_a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
h₁ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ ↑x = 2 * (1 / 2 * (↑x + 1)) - 1
[PROOFSTEP]
ring
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀✝ x₁✝ x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ Continuous fun t => { val := transAssocReparamAux t, property := (_ : transAssocReparamAux t ∈ I) }
[PROOFSTEP]
continuity
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x y : FundamentalGroupoid X
p : x ⟶ y
⊢ ∀ (a b : Path x y),
    a ≈ b →
      (fun l => Quotient.mk (Path.Homotopic.setoid y x) (Path.symm l)) a =
        (fun l => Quotient.mk (Path.Homotopic.setoid y x) (Path.symm l)) b
[PROOFSTEP]
rintro a b ⟨h⟩
[GOAL]
case intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x y : FundamentalGroupoid X
p : x ⟶ y
a b : Path x y
h : Path.Homotopy a b
⊢ (fun l => Quotient.mk (Path.Homotopic.setoid y x) (Path.symm l)) a =
    (fun l => Quotient.mk (Path.Homotopic.setoid y x) (Path.symm l)) b
[PROOFSTEP]
simp only
[GOAL]
case intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x y : FundamentalGroupoid X
p : x ⟶ y
a b : Path x y
h : Path.Homotopy a b
⊢ Quotient.mk (Path.Homotopic.setoid y x) (Path.symm a) = Quotient.mk (Path.Homotopic.setoid y x) (Path.symm b)
[PROOFSTEP]
rw [Quotient.eq]
[GOAL]
case intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
x y : FundamentalGroupoid X
p : x ⟶ y
a b : Path x y
h : Path.Homotopy a b
⊢ Path.symm a ≈ Path.symm b
[PROOFSTEP]
exact ⟨h.symm₂⟩
[GOAL]
X✝¹ : Type u
Y✝¹ : Type v
inst✝¹ : TopologicalSpace X✝¹
inst✝ : TopologicalSpace Y✝¹
x₀ x₁ : X✝¹
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
X Y : ↑((fun X => Bundled.mk (FundamentalGroupoid ↑X)) X✝)
p : X ⟶ Y
⊢ ↑f X ⟶ ↑f Y
[PROOFSTEP]
exact Path.Homotopic.Quotient.mapFn p f
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
x y z : ↑((fun X => Bundled.mk (FundamentalGroupoid ↑X)) X✝)
p : x ⟶ y
q : y ⟶ z
⊢ { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map (p ≫ q) =
    { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map p ≫
      { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map q
[PROOFSTEP]
refine' Quotient.inductionOn₂ p q fun a b => _
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
x y z : ↑((fun X => Bundled.mk (FundamentalGroupoid ↑X)) X✝)
p : x ⟶ y
q : y ⟶ z
a : Path x y
b : Path y z
⊢ { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map
      (Quotient.mk (Path.Homotopic.setoid x y) a ≫ Quotient.mk (Path.Homotopic.setoid y z) b) =
    { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map
        (Quotient.mk (Path.Homotopic.setoid x y) a) ≫
      { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }.map
        (Quotient.mk (Path.Homotopic.setoid y z) b)
[PROOFSTEP]
simp only [comp_eq, ← Path.Homotopic.map_lift, ← Path.Homotopic.comp_lift, Path.map_trans]
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
⊢ { obj := fun X => Bundled.mk (FundamentalGroupoid ↑X),
          map := fun {X Y} f =>
            CategoryTheory.Functor.mk { obj := ↑f, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.mapFn p f } }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => Bundled.mk (FundamentalGroupoid ↑X),
            map := fun {X Y} f =>
              CategoryTheory.Functor.mk { obj := ↑f, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.mapFn p f } }.obj
        X)
[PROOFSTEP]
simp only
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
⊢ CategoryTheory.Functor.mk { obj := ↑(𝟙 X), map := fun {X_1 Y} p => Path.Homotopic.Quotient.mapFn p (𝟙 X) } =
    𝟙 (Bundled.mk (FundamentalGroupoid ↑X))
[PROOFSTEP]
change _ = (⟨_, _, _⟩ : FundamentalGroupoid X ⥤ FundamentalGroupoid X)
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
⊢ CategoryTheory.Functor.mk { obj := ↑(𝟙 X), map := fun {X_1 Y} p => Path.Homotopic.Quotient.mapFn p (𝟙 X) } =
    CategoryTheory.Functor.mk { obj := fun X => X, map := fun {X_1 Y} f => f }
[PROOFSTEP]
congr
[GOAL]
case e_toPrefunctor.e_map
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
⊢ (fun {X_1 Y} p => Path.Homotopic.Quotient.mapFn p (𝟙 X)) = fun {X_1 Y} f => f
[PROOFSTEP]
ext x y p
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
⊢ Path.Homotopic.Quotient.mapFn p (𝟙 X) = p
[PROOFSTEP]
refine' Quotient.inductionOn p fun q => _
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
q : Path x y
⊢ Path.Homotopic.Quotient.mapFn (Quotient.mk (Path.Homotopic.setoid x y) q) (𝟙 X) =
    Quotient.mk (Path.Homotopic.setoid x y) q
[PROOFSTEP]
rw [← Path.Homotopic.map_lift]
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
q : Path x y
⊢ Quotient.mk (Path.Homotopic.setoid (↑(𝟙 X) x) (↑(𝟙 X) y)) (Path.map q (_ : Continuous ↑(𝟙 X))) =
    Quotient.mk (Path.Homotopic.setoid x y) q
[PROOFSTEP]
conv_rhs => rw [← q.map_id]
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
q : Path x y
| Quotient.mk (Path.Homotopic.setoid x y) q
[PROOFSTEP]
rw [← q.map_id]
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
q : Path x y
| Quotient.mk (Path.Homotopic.setoid x y) q
[PROOFSTEP]
rw [← q.map_id]
[GOAL]
X✝ : Type u
Y : Type v
inst✝¹ : TopologicalSpace X✝
inst✝ : TopologicalSpace Y
x₀ x₁ : X✝
X : TopCat
x y : FundamentalGroupoid ↑X
p : x ⟶ y
q : Path x y
| Quotient.mk (Path.Homotopic.setoid x y) q
[PROOFSTEP]
rw [← q.map_id]
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => Bundled.mk (FundamentalGroupoid ↑X),
          map := fun {X Y} f =>
            CategoryTheory.Functor.mk { obj := ↑f, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.mapFn p f } }.map
      (f ≫ g) =
    { obj := fun X => Bundled.mk (FundamentalGroupoid ↑X),
            map := fun {X Y} f =>
              CategoryTheory.Functor.mk { obj := ↑f, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.mapFn p f } }.map
        f ≫
      { obj := fun X => Bundled.mk (FundamentalGroupoid ↑X),
            map := fun {X Y} f =>
              CategoryTheory.Functor.mk { obj := ↑f, map := fun {X_1 Y_1} p => Path.Homotopic.Quotient.mapFn p f } }.map
        g
[PROOFSTEP]
simp only
[GOAL]
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ CategoryTheory.Functor.mk { obj := ↑(f ≫ g), map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p (f ≫ g) } =
    CategoryTheory.Functor.mk { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f } ≫
      CategoryTheory.Functor.mk { obj := ↑g, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p g }
[PROOFSTEP]
congr
[GOAL]
case e_toPrefunctor.e_map
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (fun {X Y} p => Path.Homotopic.Quotient.mapFn p (f ≫ g)) = fun {X Y} f_1 =>
    (CategoryTheory.Functor.mk { obj := ↑g, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p g }).map
      ((CategoryTheory.Functor.mk { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }).map f_1)
[PROOFSTEP]
ext x y p
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x y : FundamentalGroupoid ↑X✝
p : x ⟶ y
⊢ Path.Homotopic.Quotient.mapFn p (f ≫ g) =
    (CategoryTheory.Functor.mk { obj := ↑g, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p g }).map
      ((CategoryTheory.Functor.mk { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }).map p)
[PROOFSTEP]
refine' Quotient.inductionOn p fun q => _
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x y : FundamentalGroupoid ↑X✝
p : x ⟶ y
q : Path x y
⊢ Path.Homotopic.Quotient.mapFn (Quotient.mk (Path.Homotopic.setoid x y) q) (f ≫ g) =
    (CategoryTheory.Functor.mk { obj := ↑g, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p g }).map
      ((CategoryTheory.Functor.mk { obj := ↑f, map := fun {X Y} p => Path.Homotopic.Quotient.mapFn p f }).map
        (Quotient.mk (Path.Homotopic.setoid x y) q))
[PROOFSTEP]
simp only [Quotient.map_mk, Path.map_map, Quotient.eq']
[GOAL]
case e_toPrefunctor.e_map.h.h.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x y : FundamentalGroupoid ↑X✝
p : x ⟶ y
q : Path x y
⊢ Path.Homotopic.Quotient.mapFn (Quotient.mk (Path.Homotopic.setoid x y) q) (f ≫ g) =
    Path.Homotopic.Quotient.mapFn (Path.Homotopic.Quotient.mapFn (Quotient.mk (Path.Homotopic.setoid x y) q) f) g
[PROOFSTEP]
rfl
