X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252948
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) } =
    range ↑γ₁ ∪ range ↑γ₂
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252948
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range ↑(trans γ₁ γ₂) = range ↑γ₁ ∪ range ↑γ₂
rw [Path.trans]
case a
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252948
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) } ⊆
    range ↑γ₁ ∪ range ↑γ₂

case a
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252948
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range ↑γ₁ ∪ range ↑γ₂ ⊆
    range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252948
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) } =
    range ↑γ₁ ∪ range ↑γ₂
apply eq_of_subset_of_subset
case a.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
⊢ x ∈ range ↑γ₁ ∪ range ↑γ₂
case a
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252948
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) } ⊆
    range ↑γ₁ ∪ range ↑γ₂
rintro x ⟨⟨t, ht0, ht1⟩, hxt⟩
case pos
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : t ≤ 1 / 2
⊢ x ∈ range ↑γ₁ ∪ range ↑γ₂

case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : ¬t ≤ 1 / 2
⊢ x ∈ range ↑γ₁ ∪ range ↑γ₂
case a.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
⊢ x ∈ range ↑γ₁ ∪ range ↑γ₂
by_cases h : t ≤ 1 / 2
case pos.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : t ≤ 1 / 2
⊢ x ∈ range ↑γ₁
case pos
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : t ≤ 1 / 2
⊢ x ∈ range ↑γ₁ ∪ range ↑γ₂
left
case pos.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : t ≤ 1 / 2
⊢ ↑γ₁ { val := 2 * t, property := (_ : 0 ≤ 2 * t ∧ 2 * t ≤ 1) } = x
case pos.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : t ≤ 1 / 2
⊢ x ∈ range ↑γ₁
use ⟨2 * t, ⟨by linarith, by linarith⟩⟩
case pos.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : t ≤ 1 / 2
⊢ extend γ₁ (2 * t) = x
case pos.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : t ≤ 1 / 2
⊢ ↑γ₁ { val := 2 * t, property := (_ : 0 ≤ 2 * t ∧ 2 * t ≤ 1) } = x
rw [← γ₁.extend_extends]
no goals
case pos.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : t ≤ 1 / 2
⊢ extend γ₁ (2 * t) = x
rwa [coe_mk_mk, Function.comp_apply, if_pos h] at hxt
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : t ≤ 1 / 2
⊢ 0 ≤ 2 * t
linarith
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : t ≤ 1 / 2
⊢ 2 * t ≤ 1
linarith
case neg.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : ¬t ≤ 1 / 2
⊢ x ∈ range ↑γ₂
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : ¬t ≤ 1 / 2
⊢ x ∈ range ↑γ₁ ∪ range ↑γ₂
right
case neg.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : ¬t ≤ 1 / 2
⊢ ↑γ₂ { val := 2 * t - 1, property := (_ : 0 ≤ 2 * t - 1 ∧ 2 * t - 1 ≤ 1) } = x
case neg.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : ¬t ≤ 1 / 2
⊢ x ∈ range ↑γ₂
use ⟨2 * t - 1, ⟨by linarith, by linarith⟩⟩
case neg.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : ¬t ≤ 1 / 2
⊢ extend γ₂ (2 * t - 1) = x
case neg.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : ¬t ≤ 1 / 2
⊢ ↑γ₂ { val := 2 * t - 1, property := (_ : 0 ≤ 2 * t - 1 ∧ 2 * t - 1 ≤ 1) } = x
rw [← γ₂.extend_extends]
no goals
case neg.h
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : ¬t ≤ 1 / 2
⊢ extend γ₂ (2 * t - 1) = x
rwa [coe_mk_mk, Function.comp_apply, if_neg h] at hxt
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : ¬t ≤ 1 / 2
⊢ 0 ≤ 2 * t - 1
linarith
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt :
  ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } =
    x
h : ¬t ≤ 1 / 2
⊢ 2 * t - 1 ≤ 1
linarith
case a.inl.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
⊢ x ∈
    range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }

case a.inr.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
⊢ x ∈
    range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
case a
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type ?u.252948
γ : Path x y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range ↑γ₁ ∪ range ↑γ₂ ⊆
    range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
rintro x (⟨⟨t, ht0, ht1⟩, hxt⟩ | ⟨⟨t, ht0, ht1⟩, hxt⟩)
case a.inl.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t / 2, property := (_ : 0 ≤ t / 2 ∧ t / 2 ≤ 1) } =
    x
case a.inl.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
⊢ x ∈
    range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
use ⟨t / 2, ⟨by linarith, by linarith⟩⟩
case a.inl.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
this : t / 2 ≤ 1 / 2
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t / 2, property := (_ : 0 ≤ t / 2 ∧ t / 2 ≤ 1) } =
    x
case a.inl.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t / 2, property := (_ : 0 ≤ t / 2 ∧ t / 2 ≤ 1) } =
    x
have : t / 2 ≤ 1 / 2 := (div_le_div_right (zero_lt_two : (0 : ℝ) < 2)).mpr ht1
case a.inl.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
this : t / 2 ≤ 1 / 2
⊢ extend γ₁ (2 * (t / 2)) = x
case a.inl.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
this : t / 2 ≤ 1 / 2
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := t / 2, property := (_ : 0 ≤ t / 2 ∧ t / 2 ≤ 1) } =
    x
rw [coe_mk_mk, Function.comp_apply, if_pos this, Subtype.coe_mk]
case a.inl.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
this : t / 2 ≤ 1 / 2
⊢ extend γ₁ t = x
case a.inl.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
this : t / 2 ≤ 1 / 2
⊢ extend γ₁ (2 * (t / 2)) = x
ring_nf
no goals
case a.inl.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
this : t / 2 ≤ 1 / 2
⊢ extend γ₁ t = x
rwa [γ₁.extend_extends]
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
⊢ 0 ≤ t / 2
linarith
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₁ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
⊢ t / 2 ≤ 1
linarith
case pos
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t = 0
⊢ x ∈
    range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }

case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : ¬t = 0
⊢ x ∈
    range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
case a.inr.intro.mk.intro
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
⊢ x ∈
    range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
by_cases h : t = 0
case pos
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t = 0
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := 1 / 2, property := (_ : 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1) } =
    x
case pos
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t = 0
⊢ x ∈
    range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
use ⟨1 / 2, ⟨by linarith, by linarith⟩⟩
case pos
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t = 0
⊢ extend γ₁ 1 = x
case pos
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t = 0
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := 1 / 2, property := (_ : 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1) } =
    x
rw [coe_mk_mk, Function.comp_apply, if_pos le_rfl, Subtype.coe_mk,
  mul_one_div_cancel (two_ne_zero' ℝ)]
case pos
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t = 0
⊢ b = x
case pos
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t = 0
⊢ extend γ₁ 1 = x
rw [γ₁.extend_one]
no goals
case pos
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t = 0
⊢ b = x
rwa [← γ₂.extend_extends, h, γ₂.extend_zero] at hxt
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t = 0
⊢ 0 ≤ 1 / 2
linarith
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t = 0
⊢ 1 / 2 ≤ 1
linarith
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : ¬t = 0
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := (t + 1) / 2, property := (_ : 0 ≤ (t + 1) / 2 ∧ (t + 1) / 2 ≤ 1) } =
    x
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : ¬t = 0
⊢ x ∈
    range
      ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
use ⟨(t + 1) / 2, ⟨by linarith, by linarith⟩⟩
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := (t + 1) / 2, property := (_ : 0 ≤ (t + 1) / 2 ∧ (t + 1) / 2 ≤ 1) } =
    x
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : ¬t = 0
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := (t + 1) / 2, property := (_ : 0 ≤ (t + 1) / 2 ∧ (t + 1) / 2 ≤ 1) } =
    x
replace h : t ≠ 0 := h
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := (t + 1) / 2, property := (_ : 0 ≤ (t + 1) / 2 ∧ (t + 1) / 2 ≤ 1) } =
    x
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := (t + 1) / 2, property := (_ : 0 ≤ (t + 1) / 2 ∧ (t + 1) / 2 ≤ 1) } =
    x
have ht0 := lt_of_le_of_ne ht0 h.symm
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
this : ¬(t + 1) / 2 ≤ 1 / 2
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := (t + 1) / 2, property := (_ : 0 ≤ (t + 1) / 2 ∧ (t + 1) / 2 ≤ 1) } =
    x
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := (t + 1) / 2, property := (_ : 0 ≤ (t + 1) / 2 ∧ (t + 1) / 2 ≤ 1) } =
    x
have : ¬(t + 1) / 2 ≤ 1 / 2 := by
  rw [not_le]
  linarith
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
this : ¬(t + 1) / 2 ≤ 1 / 2
⊢ extend γ₂ (2 * ((t + 1) / 2) - 1) = x
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
this : ¬(t + 1) / 2 ≤ 1 / 2
⊢ ↑{
          toContinuousMap :=
            ContinuousMap.mk ((fun t => if t ≤ 1 / 2 then extend γ₁ (2 * t) else extend γ₂ (2 * t - 1)) ∘ Subtype.val),
          source' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 0 = a),
          target' :=
            (_ : ((fun x => if x ≤ 1 / 2 then extend γ₁ (2 * x) else extend γ₂ (2 * x - 1)) ∘ Subtype.val) 1 = c) }
      { val := (t + 1) / 2, property := (_ : 0 ≤ (t + 1) / 2 ∧ (t + 1) / 2 ≤ 1) } =
    x
rw [coe_mk_mk, Function.comp_apply, Subtype.coe_mk, if_neg this]
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
this : ¬(t + 1) / 2 ≤ 1 / 2
⊢ extend γ₂ t = x
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
this : ¬(t + 1) / 2 ≤ 1 / 2
⊢ extend γ₂ (2 * ((t + 1) / 2) - 1) = x
ring_nf
no goals
case neg
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
this : ¬(t + 1) / 2 ≤ 1 / 2
⊢ extend γ₂ t = x
rwa [γ₂.extend_extends]
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : ¬t = 0
⊢ 0 ≤ (t + 1) / 2
linarith
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0 : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : ¬t = 0
⊢ (t + 1) / 2 ≤ 1
linarith
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
⊢ 1 / 2 < (t + 1) / 2
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
⊢ ¬(t + 1) / 2 ≤ 1 / 2
rw [not_le]
no goals
X✝ : Type ?u.252930
Y : Type ?u.252933
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x✝ y z : X✝
ι : Type ?u.252948
γ : Path x✝ y
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
x : X
t : ℝ
ht0✝ : 0 ≤ t
ht1 : t ≤ 1
hxt : ↑γ₂ { val := t, property := (_ : 0 ≤ t ∧ t ≤ 1) } = x
h : t ≠ 0
ht0 : 0 < t
⊢ 1 / 2 < (t + 1) / 2
linarith