-- Mathlib/Topology/Path.lean
theorem trans_range {a b c : X} (γ₁ : Path a b) (γ₂ : Path b c) :
    range (γ₁.trans γ₂) = range γ₁ ∪ range γ₂

Proof state:
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 :
  { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t, ⋯⟩ =
    x
h : ¬t ≤ 1 / 2
⊢ 0 ≤ 2 * t - 1

Tactic:
linarith

Result:
no goals

Proof state:
case h
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 : γ₂ ⟨t, ⋯⟩ = x
h : ¬t = 0
⊢ { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨(t + 1) / 2, ⋯⟩ =
    x

Tactic:
replace h : t ≠ 0 := h

Result:
case h
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 : γ₂ ⟨t, ⋯⟩ = x
h : t ≠ 0
⊢ { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨(t + 1) / 2, ⋯⟩ =
    x

Proof state:
case h
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 : γ₁ ⟨t, ⋯⟩ = x
this : t / 2 ≤ 1 / 2
⊢ γ₁.extend t = x

Tactic:
rwa [γ₁.extend_extends]

Result:
no goals

Proof state:
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 : γ₂ ⟨t, ⋯⟩ = x
h : t = 0
⊢ 0 ≤ 1 / 2

Tactic:
linarith

Result:
no goals

Proof state:
case h
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 : γ₂ ⟨t, ⋯⟩ = x
h : t ≠ 0
ht0 : 0 < t
this : ¬(t + 1) / 2 ≤ 1 / 2
⊢ { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨(t + 1) / 2, ⋯⟩ =
    x

Tactic:
rw [coe_mk_mk, Function.comp_apply, Subtype.coe_mk, if_neg this]

Result:
case h
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 : γ₂ ⟨t, ⋯⟩ = x
h : t ≠ 0
ht0 : 0 < t
this : ¬(t + 1) / 2 ≤ 1 / 2
⊢ γ₂.extend (2 * ((t + 1) / 2) - 1) = x

Proof state:
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 : γ₁ ⟨t, ⋯⟩ = x
⊢ t / 2 ≤ 1

Tactic:
linarith

Result:
no goals

Proof state:
case neg.h
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 :
  { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t, ⋯⟩ =
    x
h : ¬t ≤ 1 / 2
⊢ x ∈ range ⇑γ₂

Tactic:
use ⟨2 * t - 1, ⟨by linarith, by linarith⟩⟩

Result:
case h
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 :
  { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t, ⋯⟩ =
    x
h : ¬t ≤ 1 / 2
⊢ γ₂ ⟨2 * t - 1, ⋯⟩ = x

Proof state:
case h
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 : γ₁ ⟨t, ⋯⟩ = x
⊢ { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t / 2, ⋯⟩ =
    x

Tactic:
have : t / 2 ≤ 1 / 2 := (div_le_div_iff_of_pos_right (zero_lt_two : (0 : ℝ) < 2)).mpr ht1

Result:
case h
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 : γ₁ ⟨t, ⋯⟩ = x
this : t / 2 ≤ 1 / 2
⊢ { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t / 2, ⋯⟩ =
    x

Proof state:
case h
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 : γ₂ ⟨t, ⋯⟩ = x
h : t = 0
⊢ γ₁.extend 1 = x

Tactic:
rw [γ₁.extend_one]

Result:
case h
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 : γ₂ ⟨t, ⋯⟩ = x
h : t = 0
⊢ b = x

Proof state:
case a.intro.mk.intro
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 :
  { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t, ⋯⟩ =
    x
⊢ x ∈ range ⇑γ₁ ∪ range ⇑γ₂

Tactic:
by_cases h : t ≤ 1 / 2

Result:
case pos
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 :
  { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t, ⋯⟩ =
    x
h : t ≤ 1 / 2
⊢ x ∈ range ⇑γ₁ ∪ range ⇑γ₂

case neg
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 :
  { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t, ⋯⟩ =
    x
h : ¬t ≤ 1 / 2
⊢ x ∈ range ⇑γ₁ ∪ range ⇑γ₂

Proof state:
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 :
  { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t, ⋯⟩ =
    x
h : ¬t ≤ 1 / 2
⊢ 2 * t - 1 ≤ 1

Tactic:
linarith

Result:
no goals

Proof state:
case h
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 : γ₂ ⟨t, ⋯⟩ = x
h : t = 0
⊢ b = x

Tactic:
rwa [← γ₂.extend_extends, h, γ₂.extend_zero] at hxt

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range ⇑(γ₁.trans γ₂) = range ⇑γ₁ ∪ range ⇑γ₂

Tactic:
rw [Path.trans]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range
      ⇑{ toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } =
    range ⇑γ₁ ∪ range ⇑γ₂

Proof state:
case h
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 :
  { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t, ⋯⟩ =
    x
h : ¬t ≤ 1 / 2
⊢ γ₂.extend (2 * t - 1) = x

Tactic:
rwa [coe_mk_mk, Function.comp_apply, if_neg h] at hxt

Result:
no goals

Proof state:
case h
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 :
  { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t, ⋯⟩ =
    x
h : ¬t ≤ 1 / 2
⊢ γ₂ ⟨2 * t - 1, ⋯⟩ = x

Tactic:
rw [← γ₂.extend_extends]

Result:
case h
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 :
  { toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      ⟨t, ⋯⟩ =
    x
h : ¬t ≤ 1 / 2
⊢ γ₂.extend (2 * t - 1) = x