-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem trans_refl_reparam (p : Path x₀ x₁) :
    p.trans (Path.refl x₁) =
      p.reparam (fun t => ⟨transReflReparamAux t, transReflReparamAux_mem_I t⟩) (by continuity)
        (Subtype.ext transReflReparamAux_zero) (Subtype.ext transReflReparamAux_one)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous fun t => ⟨transReflReparamAux t, ⋯⟩

Tactic:
continuity

Result:
no goals

Proof state:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (if h : ↑x✝ ≤ 2⁻¹ then p ⟨2 * ↑x✝, ⋯⟩ else x₁) = p ⟨if ↑x✝ ≤ 2⁻¹ then 2 * ↑x✝ else 1, ⋯⟩

Tactic:
split_ifs

Result:
case pos
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ↑x✝ ≤ 2⁻¹
h✝ : ↑x✝ ≤ 2⁻¹
⊢ p ⟨2 * ↑x✝, ⋯⟩ = p ⟨2 * ↑x✝, ⋯⟩

case neg
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ↑x✝ ≤ 2⁻¹
h✝ : ¬↑x✝ ≤ 2⁻¹
⊢ p ⟨2 * ↑x✝, ⋯⟩ = p ⟨2 * ↑x✝, ⋯⟩

case pos
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ¬↑x✝ ≤ 2⁻¹
h✝ : ↑x✝ ≤ 2⁻¹
⊢ x₁ = p ⟨1, ⋯⟩

case neg
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ¬↑x✝ ≤ 2⁻¹
h✝ : ¬↑x✝ ≤ 2⁻¹
⊢ x₁ = p ⟨1, ⋯⟩

Proof state:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (p.trans (Path.refl x₁)) x✝ = (p.reparam (fun t => ⟨if ↑t ≤ 1 / 2 then 2 * ↑t else 1, ⋯⟩) ⋯ ⋯ ⋯) x✝

Tactic:
simp only [Path.trans_apply, not_le, coe_reparam, Function.comp_apply, one_div, Path.refl_apply]

Result:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (if h : ↑x✝ ≤ 2⁻¹ then p ⟨2 * ↑x✝, ⋯⟩ else x₁) = p ⟨if ↑x✝ ≤ 2⁻¹ then 2 * ↑x✝ else 1, ⋯⟩

Proof state:
case neg
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ¬↑x✝ ≤ 2⁻¹
h✝ : ¬↑x✝ ≤ 2⁻¹
⊢ x₁ = p ⟨1, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
case pos
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ¬↑x✝ ≤ 2⁻¹
h✝ : ↑x✝ ≤ 2⁻¹
⊢ x₁ = p ⟨1, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (p.trans (Path.refl x₁)) x✝ = (p.reparam (fun t => ⟨transReflReparamAux t, ⋯⟩) ⋯ ⋯ ⋯) x✝

Tactic:
unfold transReflReparamAux

Result:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (p.trans (Path.refl x₁)) x✝ = (p.reparam (fun t => ⟨if ↑t ≤ 1 / 2 then 2 * ↑t else 1, ⋯⟩) ⋯ ⋯ ⋯) x✝

Proof state:
case neg
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ↑x✝ ≤ 2⁻¹
h✝ : ¬↑x✝ ≤ 2⁻¹
⊢ p ⟨2 * ↑x✝, ⋯⟩ = p ⟨2 * ↑x✝, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
case pos
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
h✝¹ : ↑x✝ ≤ 2⁻¹
h✝ : ↑x✝ ≤ 2⁻¹
⊢ p ⟨2 * ↑x✝, ⋯⟩ = p ⟨2 * ↑x✝, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ p.trans (Path.refl x₁) = p.reparam (fun t => ⟨transReflReparamAux t, ⋯⟩) ⋯ ⋯ ⋯

Tactic:
ext

Result:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x✝ : ↑I
⊢ (p.trans (Path.refl x₁)) x✝ = (p.reparam (fun t => ⟨transReflReparamAux t, ⋯⟩) ⋯ ⋯ ⋯) x✝