awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
linarith₄ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₅ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
linarith₇ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 4 / 4 = 1
linarith₈ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₉ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 4 0
⊢ 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
have linarith₁₀ : 1 / 2 * ((↑t : ℝ) + 1) < 0 →
  HMul.hMul (α := ℝ) 3 (-1) + (HMul.hMul (α := ℝ) 1 1 - 2 * (↑t : ℝ)) +
      2 * (HMul.hMul (α := ℝ) 1 1 * (1 * (↑t : ℝ) + HMul.hMul (α := ℝ) 1 1) - HMul.hMul (α := ℝ) 2 0) =
    0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
linarith₄ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 2 / 2 = 1
linarith₅ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
linarith₇ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → 4 / 4 = 1
linarith₈ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₉ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 4 0
linarith₁₀ :
  1 / 2 * ((↑t : ℝ) + 1) < 0 →
    HMul.hMul (α := ℝ) 3 (-1) + (HMul.hMul (α := ℝ) 1 1 - 2 * (↑t : ℝ)) +
        2 * (HMul.hMul (α := ℝ) 1 1 * (1 * (↑t : ℝ) + HMul.hMul (α := ℝ) 1 1) - HMul.hMul (α := ℝ) 2 0) =
      0
⊢ 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
have linarith₁₁ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 3 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
⊢ 1 / 2 * ((↑t : ℝ) + 1) ≤ 1
have linarith : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
⊢ 1 / 2 * ((↑t : ℝ) + 1) ≤ 1
have linarith₁ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
linarith₁ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 / 2 * ((↑t : ℝ) + 1) ≤ 1
have linarith₂ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
linarith₁ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 2 1 = 2
⊢ 1 / 2 * ((↑t : ℝ) + 1) ≤ 1
have linarith₃ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 2 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
linarith₁ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 2 0
linarith₄ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
linarith₅ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 2 0
⊢ 1 / 2 * ((↑t : ℝ) + 1) ≤ 1
have linarith₇ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 4 / 4 = 1
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
linarith₁ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 2 0
linarith₄ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
linarith₅ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 2 0
linarith₇ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 4 / 4 = 1
⊢ 1 / 2 * ((↑t : ℝ) + 1) ≤ 1
have linarith₈ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
linarith₁ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 2 0
linarith₄ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
linarith₅ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 2 0
linarith₇ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 4 / 4 = 1
linarith₈ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 4 = 4
⊢ 1 / 2 * ((↑t : ℝ) + 1) ≤ 1
have linarith₉ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 4 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic (goal)
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
linarith : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
linarith₁ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 2 0
linarith₄ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 2 / 2 = 1
linarith₅ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 2 0
linarith₇ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → 4 / 4 = 1
linarith₈ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → HMul.hMul (α := ℝ) 1 4 = 4
linarith₉ : 1 < 1 / 2 * ((↑t : ℝ) + 1) → GT.gt (α := ℝ) 4 0
⊢ 1 / 2 * ((↑t : ℝ) + 1) ≤ 1
have linarith₁₀ : 1 < 1 / 2 * ((↑t : ℝ) + 1) →
  HMul.hMul (α := ℝ) 2 1 - HMul.hMul (α := ℝ) 1 1 * (1 * (↑t : ℝ) + HMul.hMul (α := ℝ) 1 1) + ((↑t : ℝ) - 1) = 0
Tactic: linarith [unitInterval.le_one t, unitInterval.nonneg t]
-- 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₃
⊢ (p.trans q).trans r =
    (p.trans (q.trans r)).reparam
      (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transAssocReparamAux t) ⋯)
      trans_assoc_reparam._proof_1 ⋯ ⋯
have a : ∀ (x : (↑I : Type)),
  Eq (α := X) (((p.trans q).trans r : (a : (↑I : Type)) → X) x : X)
    (((p.trans (q.trans r)).reparam
            (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transAssocReparamAux t) sorry)
            trans_assoc_reparam._proof_1 sorry sorry :
          (a : (↑I : Type)) → X)
        x :
      X)
Tactic: ext x
-- 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)
⊢ Eq (α := X) (((p.trans q).trans r : (a : (↑I : Type)) → X) x : X)
    (((p.trans (q.trans r)).reparam
            (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transAssocReparamAux t) ⋯)
            trans_assoc_reparam._proof_1 ⋯ ⋯ :
          (a : (↑I : Type)) → X)
        x :
      X)
have a : 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 : ℝ))) sorry)
    else (q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ)) - 1) sorry)
  else (r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) sorry))
  (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))
        sorry)
  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))
          sorry)
    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)
          sorry))
Tactic: simp only [transAssocReparamAux, Path.trans_apply, Function.comp_apply, Path.coe_reparam]
-- 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)
⊢ 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),
  Eq (α := X) ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ))) sorry) : X)
    ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ))) sorry) : X)
Tactic: split_ifs
-- 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)
⊢ 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),
  Eq (α := X) ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ))) sorry) : X)
    ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * ((↑x : ℝ) + 1 / 4)) sorry) : X)
Tactic: split_ifs
-- 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)
⊢ 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) ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (↑x : ℝ))) 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
-- 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)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : 1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 / 2 * ((↑x : ℝ) + 1))) ⋯) : X)
have linarith : 2 / 2 = 1
Tactic: linarith
-- 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)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : 1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
linarith : 2 / 2 = 1
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 / 2 * ((↑x : ℝ) + 1))) ⋯) : X)
have linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : 1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 / 2 * ((↑x : ℝ) + 1))) ⋯) : X)
have linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- 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)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : 1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 / 2 * ((↑x : ℝ) + 1))) ⋯) : X)
have linarith₅ : GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : 1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 / 2 * ((↑x : ℝ) + 1))) ⋯) : X)
have linarith₆ : 4 / 4 = 1
Tactic: linarith
-- 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)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : 1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ : 4 / 4 = 1
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 / 2 * ((↑x : ℝ) + 1))) ⋯) : X)
have linarith₇ : HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- 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)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : 1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ : 4 / 4 = 1
linarith₇ : HMul.hMul (α := ℝ) 1 4 = 4
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 / 2 * ((↑x : ℝ) + 1))) ⋯) : X)
have linarith₈ : GT.gt (α := ℝ) 4 0
Tactic: linarith
-- 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)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : 1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 2 / 2 = 1
linarith₄ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : GT.gt (α := ℝ) 2 0
linarith₆ : 4 / 4 = 1
linarith₇ : HMul.hMul (α := ℝ) 1 4 = 4
linarith₈ : GT.gt (α := ℝ) 4 0
linarith₉ : 2 / 2 = 1
linarith₁₀ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : GT.gt (α := ℝ) 2 0
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (1 / 2 * ((↑x : ℝ) + 1))) ⋯) : X)
have linarith₁₂ : -1 + (HMul.hMul (α := ℝ) 1 1 - 2 * (↑x : ℝ)) +
    2 * (HMul.hMul (α := ℝ) 1 1 * (1 * (↑x : ℝ) + HMul.hMul (α := ℝ) 1 1) - HMul.hMul (α := ℝ) 1 1) =
  0
Tactic: linarith