awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
x : (↑I : Type) × (↑I : Type)
h : ¬(↑x.2 : ℝ) ≤ 1 / 2
⊢ 2 - 2 * (↑x.2 : ℝ) ≤ 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous.{0, u_1} (Y := X) fun (x : (↑I : Type) × (↑I : Type)) ↦
    (p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (reflTransSymmAux x) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ ∀ (x : (↑I : Type)),
    Eq (α := X) ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (reflTransSymmAux (0, x)) ⋯) : X)
      ((toContinuousMap (Path.refl x₀) : (a : (↑I : Type)) → X) x : X)

Tactic:
simp [reflTransSymmAux]

Premises used: Path.Homotopy.reflTransSymmAux
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
simp :
  Eq (α := X)
    ((p : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
          (if (↑x : ℝ) ≤ 1 / 2 then HMul.hMul (α := ℝ) (↑1 : ℝ) 2 * (↑x : ℝ) else (↑1 : ℝ) * (2 - 2 * (↑x : ℝ))) ⋯) :
      X)
    (({
            toFun :=
              (fun (t : ℝ) ↦
                  if t ≤ 1 / 2 then (p.extend : (a : ℝ) → X) (2 * t) else (p.symm.extend : (a : ℝ) → X) (2 * t - 1)) ∘
                Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)
⊢ Eq (α := X) ((p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (reflTransSymmAux (1, x)) ⋯) : X)
    (((p.trans p.symm).toContinuousMap : (a : (↑I : Type)) → X) x : X)

Tactic:
simp only [reflTransSymmAux, Path.trans]

Premises used: Path.trans, Path.Homotopy.reflTransSymmAux
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
hx : (↑x : ℝ) ≤ 2⁻¹
⊢ Eq (α := X)
    ((p : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
          (if (↑x : ℝ) ≤ 1 / 2 then HMul.hMul (α := ℝ) (↑1 : ℝ) 2 * (↑x : ℝ) else (↑1 : ℝ) * (2 - 2 * (↑x : ℝ))) ⋯) :
      X)
    (({
            toFun :=
              (fun (t : ℝ) ↦
                  if t ≤ 1 / 2 then (p.extend : (a : ℝ) → X) (2 * t) else (p.symm.extend : (a : ℝ) → X) (2 * t - 1)) ∘
                Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)

Tactic:
simp [hx, ← extend_apply]

Premises used: Path.extend_apply
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
hx : 2⁻¹ < (↑x : ℝ)
⊢ Eq (α := X) ((p.extend : (a : ℝ) → X) (2 - 2 * (↑x : ℝ)) : X) ((p.extend : (a : ℝ) → X) (1 - (2 * (↑x : ℝ) - 1)) : X)

Tactic:
ring_nf
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
hx : 2⁻¹ < (↑x : ℝ)
⊢ Eq (α := X) ((p.extend : (a : ℝ) → X) (2 - 2 * (↑x : ℝ)) : X) ((p.extend : (a : ℝ) → X) (1 - (2 * (↑x : ℝ) - 1)) : X)

Tactic:
have : p.extend (2 - 2 * ↑x) = p.extend (1 - (2 * ↑x - 1)) := by ring_nf
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
hx : 2⁻¹ < (↑x : ℝ)
this :
  Eq (α := X) ((p.extend : (a : ℝ) → X) (2 - 2 * (↑x : ℝ)) : X) ((p.extend : (a : ℝ) → X) (1 - (2 * (↑x : ℝ) - 1)) : X)
⊢ Eq (α := X)
    ((p : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
          (if (↑x : ℝ) ≤ 1 / 2 then HMul.hMul (α := ℝ) (↑1 : ℝ) 2 * (↑x : ℝ) else (↑1 : ℝ) * (2 - 2 * (↑x : ℝ))) ⋯) :
      X)
    (({
            toFun :=
              (fun (t : ℝ) ↦
                  if t ≤ 1 / 2 then (p.extend : (a : ℝ) → X) (2 * t) else (p.symm.extend : (a : ℝ) → X) (2 * t - 1)) ∘
                Subtype.val (p := fun (x : ℝ) ↦ x ∈ I),
            continuous_toFun := ⋯ : C((↑I : Type), X) } :
          (a : (↑I : Type)) → X)
        x :
      X)

Tactic:
simpa [hx.not_ge, ← extend_apply]

Premises used: Path.extend_apply, LT.lt.not_ge
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
⊢ (↑x : ℝ) ≤ 2⁻¹ ∨ 2⁻¹ < (↑x : ℝ)

Tactic:
cases le_or_gt (x : ℝ) 2⁻¹ with
    | inl hx => simp [hx, ← extend_apply]
    | inr hx =>
      have : p.extend (2 - 2 * ↑x) = p.extend (1 - (2 * ↑x - 1)) := by ring_nf
      simpa [hx.not_ge, ← extend_apply]

Premises used: Path.extend_apply, le_or_gt, Inv.inv, OfNat.ofNat, Subtype.val
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
t : (↑I : Type)
⊢ ∀ (x : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) {0, 1} x →
      Eq (α := X)
        (({
                toFun := fun (x : (↑I : Type)) ↦
                  (p : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (reflTransSymmAux (t, x)) ⋯),
                continuous_toFun := ⋯ : C((↑I : Type), X) } :
              (a : (↑I : Type)) → X)
            x :
          X)
        ((toContinuousMap (Path.refl x₀) : (a : (↑I : Type)) → X) x : X)

Tactic:
norm_num [reflTransSymmAux]

Premises used: Path.Homotopy.reflTransSymmAux
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ Continuous (X := (↑I : Type)) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I))

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ Continuous (Y := ℝ) fun (x : (↑I : Type)) ↦ 1 / 2

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : (↑I : Type)) ↦ 2 * (↑x : ℝ)) {x : (↑I : Type) | (↑x : ℝ) ≤ 1 / 2}

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : (↑I : Type)) ↦ 1) {x : (↑I : Type) | 1 / 2 ≤ (↑x : ℝ)}

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ∀ (x : (↑I : Type)), (↑x : ℝ) = 1 / 2 → 2 * (↑x : ℝ) = 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
pos : (↑t : ℝ) ≤ 1 / 2 → 2 * (↑t : ℝ) ∈ I
neg : ¬(↑t : ℝ) ≤ 1 / 2 → 1 ∈ I
⊢ (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) ∈ I

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
pos : 0 ≤ 2 * (↑t : ℝ)
pos₁ : 2 * (↑t : ℝ) ≤ 1
⊢ 2 * (↑t : ℝ) ∈ I

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
neg : LE.le (α := ℝ) 0 1
neg₁ : LE.le (α := ℝ) 1 1
⊢ 1 ∈ I

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
linarith : 2 * (↑t : ℝ) < 0 → 2 / 2 = 1
linarith₁ : 2 * (↑t : ℝ) < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * (↑t : ℝ) < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * (↑t : ℝ) < 0 → 2 * (↑t : ℝ) - 0 + 2 * (0 - (↑t : ℝ)) = 0
linarith₄ : 2 * (↑t : ℝ) < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 2 * (↑t : ℝ)

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

Premises used: unitInterval.le_one, unitInterval.nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < 2 * (↑t : ℝ) → 2 / 2 = 1
linarith₁ : 1 < 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < 2 * (↑t : ℝ) → GT.gt (α := ℝ) 2 0
linarith₃ : 1 < 2 * (↑t : ℝ) → 2 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1 + (1 - 2 * (↑t : ℝ)) = 0
⊢ 2 * (↑t : ℝ) ≤ 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

Premises used: unitInterval.le_one, unitInterval.nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : LT.lt (α := ℝ) 1 0 → 2 / 2 = 1
linarith₁ : LT.lt (α := ℝ) 1 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : LT.lt (α := ℝ) 1 0 → GT.gt (α := ℝ) 2 0
linarith₃ : LT.lt (α := ℝ) 1 0 → -1 + HSub.hSub (α := ℝ) 1 0 = 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

Premises used: unitInterval.le_one, unitInterval.nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 2
linarith : LT.lt (α := ℝ) 1 1 → 2 / 2 = 1
linarith₁ : LT.lt (α := ℝ) 1 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : LT.lt (α := ℝ) 1 1 → GT.gt (α := ℝ) 2 0
linarith₃ : LT.lt (α := ℝ) 1 1 → HSub.hSub (α := ℝ) 1 1 = 0
⊢ LE.le (α := ℝ) 1 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

Premises used: unitInterval.le_one, unitInterval.nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ transReflReparamAux 0 = 0

Tactic:
norm_num [transReflReparamAux]

Premises used: Path.Homotopy.transReflReparamAux
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ transReflReparamAux 1 = 1

Tactic:
norm_num [transReflReparamAux]

Premises used: Path.Homotopy.transReflReparamAux
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ Continuous (Y := (↑I : Type)) fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transReflReparamAux t) ⋯

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
a :
  ∀ (x : (↑I : Type)),
    Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
      ((p.reparam (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transReflReparamAux t) ⋯)
              trans_refl_reparam._proof_1 ⋯ ⋯ :
            (a : (↑I : Type)) → X)
          x :
        X)
⊢ p.trans (Path.refl x₁) =
    p.reparam (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transReflReparamAux t) ⋯)
      trans_refl_reparam._proof_1 ⋯ ⋯

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
a :
  Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
    ((p.reparam
            (fun (t : (↑I : Type)) ↦
              Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) ⋯)
            trans_refl_reparam._proof_1 ⋯ ⋯ :
          (a : (↑I : Type)) → X)
        x :
      X)
⊢ Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
    ((p.reparam (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transReflReparamAux t) ⋯)
            trans_refl_reparam._proof_1 ⋯ ⋯ :
          (a : (↑I : Type)) → X)
        x :
      X)

Tactic:
unfold transReflReparamAux

Premises used: Path.Homotopy.transReflReparamAux
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
a :
  Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
    (Function.comp (β := (↑I : Type)) (⇑p : (a : (↑I : Type)) → X)
        (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) ⋯)
        x :
      X)
⊢ Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
    ((p.reparam
            (fun (t : (↑I : Type)) ↦
              Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) ⋯)
            trans_refl_reparam._proof_1 ⋯ ⋯ :
          (a : (↑I : Type)) → X)
        x :
      X)

Tactic:
simp only [coe_reparam]

Premises used: Path.coe_reparam
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
x : (↑I : Type)
⊢ Eq (α := X) ((p.trans (Path.refl x₁) : (a : (↑I : Type)) → X) x : X)
    (Function.comp (β := (↑I : Type)) (⇑p : (a : (↑I : Type)) → X)
        (fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (if (↑t : ℝ) ≤ 1 / 2 then 2 * (↑t : ℝ) else 1) ⋯)
        x :
      X)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ (p.symm.trans (Path.refl x₀)).symm = Path.trans (Path.refl x₀) p

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
⊢ p.symm.symm = p

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ Continuous (Y := ℝ) fun (x : (↑I : Type)) ↦ 1 / 4

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : (↑I : Type)) ↦ 2 * (↑x : ℝ)) {x : (↑I : Type) | (↑x : ℝ) ≤ 1 / 4}

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : (↑I : Type)) ↦ (↑x : ℝ) + 1 / 4) {x : (↑I : Type) | (↑x : ℝ) ≤ 1 / 2}

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : (↑I : Type)) ↦ 1 / 2 * ((↑x : ℝ) + 1)) {x : (↑I : Type) | 1 / 2 ≤ (↑x : ℝ)}

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ∀ (x : (↑I : Type)), (↑x : ℝ) = 1 / 2 → (↑x : ℝ) + 1 / 4 = 1 / 2 * ((↑x : ℝ) + 1)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ ∀ (x : (↑I : Type)),
    (↑x : ℝ) = 1 / 4 → 2 * (↑x : ℝ) = if (↑x : ℝ) ≤ 1 / 2 then (↑x : ℝ) + 1 / 4 else 1 / 2 * ((↑x : ℝ) + 1)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
pos : (↑t : ℝ) ≤ 1 / 4 → 2 * (↑t : ℝ) ∈ I
pos₁ : ¬(↑t : ℝ) ≤ 1 / 4 → (↑t : ℝ) ≤ 1 / 2 → (↑t : ℝ) + 1 / 4 ∈ I
neg : ¬(↑t : ℝ) ≤ 1 / 4 → ¬(↑t : ℝ) ≤ 1 / 2 → 1 / 2 * ((↑t : ℝ) + 1) ∈ I
⊢ (if (↑t : ℝ) ≤ 1 / 4 then 2 * (↑t : ℝ) else if (↑t : ℝ) ≤ 1 / 2 then (↑t : ℝ) + 1 / 4 else 1 / 2 * ((↑t : ℝ) + 1)) ∈ I

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
pos : 0 ≤ 2 * (↑t : ℝ)
pos₁ : 2 * (↑t : ℝ) ≤ 1
⊢ 2 * (↑t : ℝ) ∈ I

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
pos : 0 ≤ (↑t : ℝ) + 1 / 4
pos₁ : (↑t : ℝ) + 1 / 4 ≤ 1
⊢ (↑t : ℝ) + 1 / 4 ∈ I

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : ¬(↑t : ℝ) ≤ 1 / 2
neg : 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)
neg₁ : 1 / 2 * ((↑t : ℝ) + 1) ≤ 1
⊢ 1 / 2 * ((↑t : ℝ) + 1) ∈ I

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
linarith : 2 * (↑t : ℝ) < 0 → 4 / 4 = 1
linarith₁ : 2 * (↑t : ℝ) < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 2 * (↑t : ℝ) < 0 → GT.gt (α := ℝ) 4 0
linarith₃ : 2 * (↑t : ℝ) < 0 → 2 * (↑t : ℝ) - 0 + 2 * (0 - (↑t : ℝ)) = 0
linarith₄ : 2 * (↑t : ℝ) < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 2 * (↑t : ℝ)

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

Premises used: unitInterval.le_one, unitInterval.nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : (↑t : ℝ) ≤ 1 / 4
linarith : 1 < 2 * (↑t : ℝ) → 4 / 4 = 1
linarith₁ : 1 < 2 * (↑t : ℝ) → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 < 2 * (↑t : ℝ) → GT.gt (α := ℝ) 4 0
linarith₃ : 1 < 2 * (↑t : ℝ) → -1 + (4 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - 2 * (↑t : ℝ)) = 0
linarith₄ : 1 < 2 * (↑t : ℝ) → GT.gt (α := ℝ) 2 0
⊢ 2 * (↑t : ℝ) ≤ 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

Premises used: unitInterval.le_one, unitInterval.nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : (↑t : ℝ) + 1 / 4 < 0 → 4 / 4 = 1
linarith₁ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 4 0
linarith₃ : (↑t : ℝ) + 1 / 4 < 0 → 2 / 2 = 1
linarith₄ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 2 0
linarith₆ : (↑t : ℝ) + 1 / 4 < 0 → 4 / 4 = 1
linarith₇ : (↑t : ℝ) + 1 / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₈ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 4 0
linarith₉ :
  (↑t : ℝ) + 1 / 4 < 0 →
    HMul.hMul (α := ℝ) 2 (-1) + (HMul.hMul (α := ℝ) 1 1 - 4 * (↑t : ℝ)) +
        (4 * (↑t : ℝ) + HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 4 0) =
      0
linarith₁₀ : (↑t : ℝ) + 1 / 4 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ (↑t : ℝ) + 1 / 4

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

Premises used: unitInterval.le_one, unitInterval.nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
t : (↑I : Type)
h : ¬(↑t : ℝ) ≤ 1 / 4
h_1 : (↑t : ℝ) ≤ 1 / 2
linarith : 1 < (↑t : ℝ) + 1 / 4 → 4 / 4 = 1
linarith₁ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 4 0
linarith₃ : 1 < (↑t : ℝ) + 1 / 4 → 2 / 2 = 1
linarith₄ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 2 0
linarith₆ : 1 < (↑t : ℝ) + 1 / 4 → 4 / 4 = 1
linarith₇ : 1 < (↑t : ℝ) + 1 / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₈ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 4 0
linarith₉ :
  1 < (↑t : ℝ) + 1 / 4 →
    -1 + 2 * (2 * (↑t : ℝ) - HMul.hMul (α := ℝ) 1 1) +
        (HMul.hMul (α := ℝ) 4 1 - (4 * (↑t : ℝ) + HMul.hMul (α := ℝ) 1 1)) =
      0
linarith₁₀ : 1 < (↑t : ℝ) + 1 / 4 → GT.gt (α := ℝ) 2 0
⊢ (↑t : ℝ) + 1 / 4 ≤ 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

Premises used: unitInterval.le_one, unitInterval.nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
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
linarith₁₁ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 3 0
linarith₁₂ : 1 / 2 * ((↑t : ℝ) + 1) < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 1 / 2 * ((↑t : ℝ) + 1)

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

Premises used: unitInterval.le_one, unitInterval.nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
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
linarith₁₀ :
  1 < 1 / 2 * ((↑t : ℝ) + 1) →
    HMul.hMul (α := ℝ) 2 1 - HMul.hMul (α := ℝ) 1 1 * (1 * (↑t : ℝ) + HMul.hMul (α := ℝ) 1 1) + ((↑t : ℝ) - 1) = 0
⊢ 1 / 2 * ((↑t : ℝ) + 1) ≤ 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

Premises used: unitInterval.le_one, unitInterval.nonneg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ transAssocReparamAux 0 = 0

Tactic:
norm_num [transAssocReparamAux]

Premises used: Path.Homotopy.transAssocReparamAux
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
⊢ transAssocReparamAux 1 = 1

Tactic:
norm_num [transAssocReparamAux]

Premises used: Path.Homotopy.transAssocReparamAux
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀_1 x₁_1 x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ Continuous (Y := (↑I : Type)) fun (t : (↑I : Type)) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (transAssocReparamAux t) ⋯

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
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₃
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) ⋯)
              trans_assoc_reparam._proof_1 ⋯ ⋯ :
            (a : (↑I : Type)) → X)
          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 ⋯ ⋯

Tactic:
ext x