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

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

Tactic:
use ⟨t / 2, ⟨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 : γ₁ ⟨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

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, ⋯⟩ = 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) = 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
h : ¬t = 0
⊢ 0 ≤ (t + 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
⊢ { 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:
have : ¬(t + 1) / 2 ≤ 1 / 2 := by
  rw [not_le]
  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 : γ₂ ⟨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

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:
have ht0 := lt_of_le_of_ne ht0 h.symm

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
⊢ { 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 (2 * (t / 2)) = x

Tactic:
ring_nf

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
⊢ γ₁.extend t = 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 :
  { 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

Tactic:
linarith

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
ht0 : 0 < t
⊢ ¬(t + 1) / 2 ≤ 1 / 2

Tactic:
rw [not_le]

Result:
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
⊢ 1 / 2 < (t + 1) / 2

Proof state:
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 ⇑γ₂

Tactic:
right

Result:
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 ⇑γ₂

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
⊢ γ₂.extend t = x

Tactic:
rwa [γ₂.extend_extends]

Result:
no goals

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

Tactic:
by_cases h : t = 0

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

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

Proof state:
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 ⇑γ₂

Tactic:
left

Result:
case pos.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 ⇑γ₁