Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: 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), ⋯⟩

pp: 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), ⋯⟩

pp: 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), ⋯⟩

pp: 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, ⋯⟩

pp: 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), ⋯⟩

pp: 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, ⋯⟩

pp: 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), ⋯⟩

pp: 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), ⋯⟩

pp: 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, ⋯⟩

pp: 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), ⋯⟩

pp: 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), ⋯⟩

pp: 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, ⋯⟩

pp: 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)), ⋯⟩

pp: 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), ⋯⟩

pp: 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, ⋯⟩

Tactic:
grind

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
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, ⋯⟩