-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : (↑I : Type)
pos :
  ∀ (h : (↑x : ℝ) ≤ 1 / 2) (h_1 : 2 * (↑x : ℝ) ≤ 1 / 2) (h_2 : (↑x : ℝ) ≤ 1 / 4),
    Eq (α := X) ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ))) ⋯) : X)
      ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ))) ⋯) : X)
pos₁ :
  ∀ (h : (↑x : ℝ) ≤ 1 / 2) (h_1 : 2 * (↑x : ℝ) ≤ 1 / 2) (h_2 : ¬(↑x : ℝ) ≤ 1 / 4) (h_3 : (↑x : ℝ) + 1 / 4 ≤ 1 / 2),
    Eq (α := X) ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ))) ⋯) : X)
      ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * ((↑x : ℝ) + 1 / 4)) ⋯) : X)
pos₂ :
  ∀ (h : (↑x : ℝ) ≤ 1 / 2) (h_1 : 2 * (↑x : ℝ) ≤ 1 / 2) (h_2 : ¬(↑x : ℝ) ≤ 1 / 4) (h_3 : ¬(↑x : ℝ) + 1 / 4 ≤ 1 / 2)
    (h_4 : 2 * ((↑x : ℝ) + 1 / 4) - 1 ≤ 1 / 2),
    Eq (α := X) ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ))) ⋯) : X)
      ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * ((↑x : ℝ) + 1 / 4) - 1)) ⋯) : X)
neg :
  ∀ (h : (↑x : ℝ) ≤ 1 / 2) (h_1 : 2 * (↑x : ℝ) ≤ 1 / 2) (h_2 : ¬(↑x : ℝ) ≤ 1 / 4) (h_3 : ¬(↑x : ℝ) + 1 / 4 ≤ 1 / 2)
    (h_4 : ¬2 * ((↑x : ℝ) + 1 / 4) - 1 ≤ 1 / 2),
    Eq (α := X) ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ))) ⋯) : X)
      ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * ((↑x : ℝ) + 1 / 4) - 1) - 1) ⋯) : X)
pos₃ :
  ∀ (h : (↑x : ℝ) ≤ 1 / 2) (h_1 : ¬2 * (↑x : ℝ) ≤ 1 / 2) (h_2 : (↑x : ℝ) ≤ 1 / 4)
    (h_3 : 2 * (2 * (↑x : ℝ)) - 1 ≤ 1 / 2),
    Eq (α := X) ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ)) - 1) ⋯) : X)
      ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (2 * (↑x : ℝ)) - 1)) ⋯) : X)
neg₁ :
  ∀ (h : (↑x : ℝ) ≤ 1 / 2) (h_1 : ¬2 * (↑x : ℝ) ≤ 1 / 2) (h_2 : (↑x : ℝ) ≤ 1 / 4)
    (h_3 : ¬2 * (2 * (↑x : ℝ)) - 1 ≤ 1 / 2),
    Eq (α := X) ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ)) - 1) ⋯) : X)
      ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (2 * (↑x : ℝ)) - 1) - 1) ⋯) : X)
pos₄ :
  ∀ (h : (↑x : ℝ) ≤ 1 / 2) (h_1 : ¬2 * (↑x : ℝ) ≤ 1 / 2) (h_2 : ¬(↑x : ℝ) ≤ 1 / 4) (h_3 : (↑x : ℝ) + 1 / 4 ≤ 1 / 2),
    Eq (α := X) ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ)) - 1) ⋯) : X)
      ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * ((↑x : ℝ) + 1 / 4)) ⋯) : X)
⊢ Eq.{u_1 + 1} (α := X)
    (if h : (↑x : ℝ) ≤ 1 / 2 then
      if h_1 : 2 * (↑x : ℝ) ≤ 1 / 2 then
        (p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ))) ⋯)
      else (q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ)) - 1) ⋯)
    else (r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯))
    (if h :
        (if (↑x : ℝ) ≤ 1 / 4 then 2 * (↑x : ℝ)
          else if (↑x : ℝ) ≤ 1 / 2 then (↑x : ℝ) + 1 / 4 else 1 / 2 * ((↑x : ℝ) + 1)) ≤
          1 / 2 then
      (p : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
          (2 *
            if (↑x : ℝ) ≤ 1 / 4 then 2 * (↑x : ℝ)
            else if (↑x : ℝ) ≤ 1 / 2 then (↑x : ℝ) + 1 / 4 else 1 / 2 * ((↑x : ℝ) + 1))
          ⋯)
    else
      if h_1 :
          (2 *
                if (↑x : ℝ) ≤ 1 / 4 then 2 * (↑x : ℝ)
                else if (↑x : ℝ) ≤ 1 / 2 then (↑x : ℝ) + 1 / 4 else 1 / 2 * ((↑x : ℝ) + 1)) -
              1 ≤
            1 / 2 then
        (q : (a : (↑I : Type)) → X)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
            (2 *
              ((2 *
                  if (↑x : ℝ) ≤ 1 / 4 then 2 * (↑x : ℝ)
                  else if (↑x : ℝ) ≤ 1 / 2 then (↑x : ℝ) + 1 / 4 else 1 / 2 * ((↑x : ℝ) + 1)) -
                1))
            ⋯)
      else
        (r : (a : (↑I : Type)) → X)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
            (2 *
                ((2 *
                    if (↑x : ℝ) ≤ 1 / 4 then 2 * (↑x : ℝ)
                    else if (↑x : ℝ) ≤ 1 / 2 then (↑x : ℝ) + 1 / 4 else 1 / 2 * ((↑x : ℝ) + 1)) -
                  1) -
              1)
            ⋯))
have pos₅ : ∀ (h : (↑x : ℝ) ≤ 1 / 2) (h_1 : ¬2 * (↑x : ℝ) ≤ 1 / 2) (h_2 : ¬(↑x : ℝ) ≤ 1 / 4) (h_3 : ¬(↑x : ℝ) + 1 / 4 ≤ 1 / 2)
  (h_4 : 2 * ((↑x : ℝ) + 1 / 4) - 1 ≤ 1 / 2),
  Eq (α := X) ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ)) - 1) sorry) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * ((↑x : ℝ) + 1 / 4) - 1)) sorry) : X)
Tactic: split_ifs