-- 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
⊢ 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 ⇑γ₂

Tactic:
apply eq_of_subset_of_subset

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

case a
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range ⇑γ₁ ∪ range ⇑γ₂ ⊆
    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 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' := ⋯ }

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

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

Tactic:
rintro x ⟨⟨t, ht0, ht1⟩, hxt⟩

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

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

Tactic:
linarith

Result:
no goals

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 : γ₂ ⟨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' := ⋯ }

Tactic:
use ⟨1 / 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
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' := ⋯ }
      ⟨1 / 2, ⋯⟩ =
    x

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

Tactic:
use ⟨2 * t, ⟨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, ⋯⟩ = 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
⊢ 0 ≤ t / 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 :
  { 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

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

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

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
⊢ 1 / 2 ≤ 1

Tactic:
linarith

Result:
no goals

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

Tactic:
rintro x (⟨⟨t, ht0, ht1⟩, hxt⟩ | ⟨⟨t, ht0, ht1⟩, hxt⟩)

Result:
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' := ⋯ }

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' := ⋯ }

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

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
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

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

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