Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: 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
⊢ (if h : ↑x ≤ 1 / 2 then if h_1 : 2 * ↑x ≤ 1 / 2 then p ⟨2 * (2 * ↑x), ⋯⟩ else q ⟨2 * (2 * ↑x) - 1, ⋯⟩
    else r ⟨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 ⟨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 ⟨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 ⟨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, ⋯⟩

Tactic:
split_ifs

Goal state after:
case pos
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
h✝² : ↑x ≤ 1 / 2
h✝¹ : 2 * ↑x ≤ 1 / 2
h✝ : ↑x ≤ 1 / 4
⊢ p ⟨2 * (2 * ↑x), ⋯⟩ = p ⟨2 * (2 * ↑x), ⋯⟩

case pos
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
h✝³ : ↑x ≤ 1 / 2
h✝² : 2 * ↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : ↑x + 1 / 4 ≤ 1 / 2
⊢ p ⟨2 * (2 * ↑x), ⋯⟩ = p ⟨2 * (↑x + 1 / 4), ⋯⟩

case pos
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
h✝⁴ : ↑x ≤ 1 / 2
h✝³ : 2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ p ⟨2 * (2 * ↑x), ⋯⟩ = q ⟨2 * (2 * (↑x + 1 / 4) - 1), ⋯⟩

case neg
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
h✝⁴ : ↑x ≤ 1 / 2
h✝³ : 2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : ¬2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ p ⟨2 * (2 * ↑x), ⋯⟩ = r ⟨2 * (2 * (↑x + 1 / 4) - 1) - 1, ⋯⟩

case pos
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
h✝³ : ↑x ≤ 1 / 2
h✝² : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ q ⟨2 * (2 * ↑x) - 1, ⋯⟩ = q ⟨2 * (2 * (2 * ↑x) - 1), ⋯⟩

case neg
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
h✝³ : ↑x ≤ 1 / 2
h✝² : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ q ⟨2 * (2 * ↑x) - 1, ⋯⟩ = r ⟨2 * (2 * (2 * ↑x) - 1) - 1, ⋯⟩

case pos
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
h✝³ : ↑x ≤ 1 / 2
h✝² : ¬2 * ↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : ↑x + 1 / 4 ≤ 1 / 2
⊢ q ⟨2 * (2 * ↑x) - 1, ⋯⟩ = p ⟨2 * (↑x + 1 / 4), ⋯⟩

case pos
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
h✝⁴ : ↑x ≤ 1 / 2
h✝³ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : 2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ q ⟨2 * (2 * ↑x) - 1, ⋯⟩ = q ⟨2 * (2 * (↑x + 1 / 4) - 1), ⋯⟩

case neg
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
h✝⁴ : ↑x ≤ 1 / 2
h✝³ : ¬2 * ↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬↑x + 1 / 4 ≤ 1 / 2
h✝ : ¬2 * (↑x + 1 / 4) - 1 ≤ 1 / 2
⊢ q ⟨2 * (2 * ↑x) - 1, ⋯⟩ = r ⟨2 * (2 * (↑x + 1 / 4) - 1) - 1, ⋯⟩

case pos
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
h✝² : ¬↑x ≤ 1 / 2
h✝¹ : ↑x ≤ 1 / 4
h✝ : 2 * ↑x ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = p ⟨2 * (2 * ↑x), ⋯⟩

case pos
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
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : 2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (2 * ↑x) - 1), ⋯⟩

case neg
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
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ↑x ≤ 1 / 4
h✝¹ : ¬2 * ↑x ≤ 1 / 2
h✝ : ¬2 * (2 * ↑x) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (2 * ↑x) - 1) - 1, ⋯⟩

case pos
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
h✝² : ¬↑x ≤ 1 / 2
h✝¹ : ¬↑x ≤ 1 / 4
h✝ : 1 / 2 * (↑x + 1) ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = p ⟨2 * (1 / 2 * (↑x + 1)), ⋯⟩

case pos
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
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : 2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = q ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1), ⋯⟩

case neg
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
h✝³ : ¬↑x ≤ 1 / 2
h✝² : ¬↑x ≤ 1 / 4
h✝¹ : ¬1 / 2 * (↑x + 1) ≤ 1 / 2
h✝ : ¬2 * (1 / 2 * (↑x + 1)) - 1 ≤ 1 / 2
⊢ r ⟨2 * ↑x - 1, ⋯⟩ = r ⟨2 * (2 * (1 / 2 * (↑x + 1)) - 1) - 1, ⋯⟩