awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃
x : (↑I : Type)
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 : ℝ))) ⋯)
      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)
            ⋯))
⊢ 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)

Tactic:
simp only [transAssocReparamAux, Path.trans_apply, Function.comp_apply, Path.coe_reparam]

Premises used: Path.Homotopy.transAssocReparamAux, Path.trans_apply, Function.comp_apply, Path.coe_reparam
-- 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₃
x : (↑I : Type)
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)

Tactic:
grind
-- 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₃
x : (↑I : Type)
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)

Tactic:
grind
-- 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₃
x : (↑I : Type)
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)

Tactic:
grind
-- 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₃
x : (↑I : Type)
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)

Tactic:
grind
-- 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₃
x : (↑I : Type)
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)

Tactic:
grind
-- 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₃
x : (↑I : Type)
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)

Tactic:
grind
-- 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₃
x : (↑I : Type)
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)

Tactic:
grind
-- 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₃
x : (↑I : Type)
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) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * ((↑x : ℝ) + 1 / 4) - 1)) ⋯) : X)

Tactic:
grind
-- 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₃
x : (↑I : Type)
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) ⋯) : X)
    ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * ((↑x : ℝ) + 1 / 4) - 1) - 1) ⋯) : X)

Tactic:
grind
-- 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₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : (↑x : ℝ) ≤ 1 / 4
h_2 : 2 * (↑x : ℝ) ≤ 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 * (2 * (↑x : ℝ))) ⋯) : X)

Tactic:
grind
-- 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₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : (↑x : ℝ) ≤ 1 / 4
h_2 : ¬2 * (↑x : ℝ) ≤ 1 / 2
h_3 : 2 * (2 * (↑x : ℝ)) - 1 ≤ 1 / 2
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (2 * (↑x : ℝ)) - 1)) ⋯) : X)

Tactic:
grind
-- 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₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : (↑x : ℝ) ≤ 1 / 4
h_2 : ¬2 * (↑x : ℝ) ≤ 1 / 2
h_3 : ¬2 * (2 * (↑x : ℝ)) - 1 ≤ 1 / 2
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (2 * (↑x : ℝ)) - 1) - 1) ⋯) : X)

Tactic:
grind
-- 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₃
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
linarith₁₂ :
  -1 + (HMul.hMul (α := ℝ) 1 1 - 2 * (↑x : ℝ)) +
      2 * (HMul.hMul (α := ℝ) 1 1 * (1 * (↑x : ℝ) + HMul.hMul (α := ℝ) 1 1) - HMul.hMul (α := ℝ) 1 1) =
    0
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)

Tactic:
linarith
-- 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₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : ¬1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
h_3 : 2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1 ≤ 1 / 2
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : 2 / 2 = 1
linarith₅ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : GT.gt (α := ℝ) 2 0
linarith₇ : 2 / 2 = 1
linarith₈ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : 2 / 2 = 1
linarith₁₀ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : HMul.hMul (α := ℝ) 2 1 = 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
linarith₁₉ :
  HMul.hMul (α := ℝ) 1 1 - 2 * (↑x : ℝ) +
      (HMul.hMul (α := ℝ) 1 2 * (HMul.hMul (α := ℝ) 1 1 * (1 * (↑x : ℝ) + HMul.hMul (α := ℝ) 1 1)) -
          HMul.hMul (α := ℝ) 2 1 -
        HMul.hMul (α := ℝ) 1 1) =
    0
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((q : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1)) ⋯) : X)

Tactic:
linarith
-- 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₃
x : (↑I : Type)
h : ¬(↑x : ℝ) ≤ 1 / 2
h_1 : ¬(↑x : ℝ) ≤ 1 / 4
h_2 : ¬1 / 2 * ((↑x : ℝ) + 1) ≤ 1 / 2
h_3 : ¬2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1 ≤ 1 / 2
⊢ Eq (α := X) ((r : (a : (↑I : Type)) → X) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (↑x : ℝ) - 1) ⋯) : X)
    ((r : (a : (↑I : Type)) → X)
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (2 * (2 * (1 / 2 * ((↑x : ℝ) + 1)) - 1) - 1) ⋯) :
      X)

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

Tactic:
⟨Homotopy.reflTrans p⟩

Premises used: Path.Homotopy.reflTrans, Nonempty.intro, Path.Homotopic
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ (p.trans (Path.refl x₁)).Homotopic p

Tactic:
⟨Homotopy.transRefl p⟩

Premises used: Path.Homotopy.transRefl, Nonempty.intro, Path.Homotopic
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ (p.trans p.symm).Homotopic (Path.refl x₀)

Tactic:
⟨(Homotopy.reflTransSymm p).symm⟩

Premises used: Path.Homotopy.reflTransSymm, Nonempty.intro, Path.Homotopic, Path.Homotopy.symm
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
p : Path x₀ x₁
⊢ (p.symm.trans p).Homotopic (Path.refl x₁)

Tactic:
⟨(Homotopy.reflSymmTrans p).symm⟩

Premises used: Nonempty.intro, Path.Homotopic, Path.Homotopy.symm, Path.Homotopy.reflSymmTrans
-- 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₃
⊢ ((p.trans q).trans r).Homotopic (p.trans (q.trans r))

Tactic:
⟨Homotopy.transAssoc p q r⟩

Premises used: Path.Homotopy.transAssoc, Nonempty.intro, Path.Homotopic
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Path x₀ x₁
⊢ trans (refl x₀) (mk γ) = mk γ

Tactic:
simpa [← mk_trans, ← mk_refl, eq] using Homotopic.refl_trans γ

Premises used: Path.Homotopic.refl_trans, Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.mk_refl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
mk : ∀ (γ : Path x₀ x₁), trans (refl x₀) (Quotient.mk γ) = Quotient.mk γ
⊢ trans (refl x₀) γ = γ

Tactic:
induction γ using Quotient.ind with | mk γ =>
  simpa [← mk_trans, ← mk_refl, eq] using Homotopic.refl_trans γ

Premises used: Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.ind, Path.Homotopic.Quotient.mk_refl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Path x₀ x₁
⊢ (mk γ).trans (refl x₁) = mk γ

Tactic:
simpa [← mk_trans, ← mk_refl, eq] using Homotopic.trans_refl γ

Premises used: Path.Homotopic.Quotient.eq, Path.Homotopic.trans_refl, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.mk_refl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
mk : ∀ (γ : Path x₀ x₁), (Quotient.mk γ).trans (refl x₁) = Quotient.mk γ
⊢ γ.trans (refl x₁) = γ

Tactic:
induction γ using Quotient.ind with | mk γ =>
  simpa [← mk_trans, ← mk_refl, eq] using Homotopic.trans_refl γ

Premises used: Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.ind, Path.Homotopic.Quotient.mk_refl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Path x₀ x₁
⊢ (mk γ).trans (mk γ).symm = refl x₀

Tactic:
simpa [← mk_trans, ← mk_symm, ← mk_refl, eq] using Homotopic.trans_symm γ

Premises used: Path.Homotopic.trans_symm, Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.mk_symm, Path.Homotopic.Quotient.mk_refl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
mk : ∀ (γ : Path x₀ x₁), (Quotient.mk γ).trans (Quotient.mk γ).symm = refl x₀
⊢ γ.trans γ.symm = refl x₀

Tactic:
induction γ using Quotient.ind with | mk γ =>
  simpa [← mk_trans, ← mk_symm, ← mk_refl, eq] using Homotopic.trans_symm γ

Premises used: Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.mk_symm, Path.Homotopic.Quotient.ind, Path.Homotopic.Quotient.mk_refl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Path x₀ x₁
⊢ (mk γ).symm.trans (mk γ) = refl x₁

Tactic:
simpa [← mk_trans, ← mk_symm, ← mk_refl, eq] using Homotopic.symm_trans γ

Premises used: Path.Homotopic.Quotient.eq, Path.Homotopic.symm_trans, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.mk_symm, Path.Homotopic.Quotient.mk_refl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
γ : Homotopic.Quotient x₀ x₁
mk : ∀ (γ : Path x₀ x₁), (Quotient.mk γ).symm.trans (Quotient.mk γ) = refl x₁
⊢ γ.symm.trans γ = refl x₁

Tactic:
induction γ using Quotient.ind with | mk γ =>
  simpa [← mk_trans, ← mk_symm, ← mk_refl, eq] using Homotopic.symm_trans γ

Premises used: Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.mk_symm, Path.Homotopic.Quotient.ind, Path.Homotopic.Quotient.mk_refl, Path.Homotopic.Quotient.mk
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₀ : Path x₀ x₁
γ₁ : Path x₁ x₂
γ₂ : Path x₂ x₃
⊢ ((mk γ₀).trans (mk γ₁)).trans (mk γ₂) = (mk γ₀).trans ((mk γ₁).trans (mk γ₂))

Tactic:
simpa [← mk_trans, eq] using Homotopic.trans_assoc γ₀ γ₁ γ₂

Premises used: Path.Homotopic.trans_assoc, Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_trans
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₂ : Homotopic.Quotient x₂ x₃
γ₀ : Path x₀ x₁
γ₁ : Path x₁ x₂
mk :
  ∀ (γ₂ : Path x₂ x₃),
    ((Quotient.mk γ₀).trans (Quotient.mk γ₁)).trans (Quotient.mk γ₂) =
      (Quotient.mk γ₀).trans ((Quotient.mk γ₁).trans (Quotient.mk γ₂))
⊢ ((Quotient.mk γ₀).trans (Quotient.mk γ₁)).trans γ₂ = (Quotient.mk γ₀).trans ((Quotient.mk γ₁).trans γ₂)

Tactic:
induction γ₂ using Quotient.ind with | mk γ₂ =>
  simpa [← mk_trans, eq] using Homotopic.trans_assoc γ₀ γ₁ γ₂

Premises used: Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.ind, Path.Homotopic.Quotient.mk
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₁ : Homotopic.Quotient x₁ x₂
γ₂ : Homotopic.Quotient x₂ x₃
γ₀ : Path x₀ x₁
mk :
  ∀ (γ₁ : Path x₁ x₂),
    ((Quotient.mk γ₀).trans (Quotient.mk γ₁)).trans γ₂ = (Quotient.mk γ₀).trans ((Quotient.mk γ₁).trans γ₂)
⊢ ((Quotient.mk γ₀).trans γ₁).trans γ₂ = (Quotient.mk γ₀).trans (γ₁.trans γ₂)

Tactic:
induction γ₁ using Quotient.ind with | mk γ₁ =>
  induction γ₂ using Quotient.ind with | mk γ₂ =>
  simpa [← mk_trans, eq] using Homotopic.trans_assoc γ₀ γ₁ γ₂

Premises used: Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.ind, Path.Homotopic.Quotient.mk
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₀ : Homotopic.Quotient x₀ x₁
γ₁ : Homotopic.Quotient x₁ x₂
γ₂ : Homotopic.Quotient x₂ x₃
mk : ∀ (γ₀ : Path x₀ x₁), ((Quotient.mk γ₀).trans γ₁).trans γ₂ = (Quotient.mk γ₀).trans (γ₁.trans γ₂)
⊢ (γ₀.trans γ₁).trans γ₂ = γ₀.trans (γ₁.trans γ₂)

Tactic:
induction γ₀ using Quotient.ind with | mk γ₀ =>
  induction γ₁ using Quotient.ind with | mk γ₁ =>
  induction γ₂ using Quotient.ind with | mk γ₂ =>
  simpa [← mk_trans, eq] using Homotopic.trans_assoc γ₀ γ₁ γ₂

Premises used: Path.Homotopic.Quotient.eq, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.ind, Path.Homotopic.Quotient.mk
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_3
⊢ IsEmpty.{u_3 + 1} (FundamentalGroupoid X) ↔ IsEmpty X

Tactic:
equiv _ |>.isEmpty_congr

Premises used: Equiv.isEmpty_congr, FundamentalGroupoid.equiv
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x₀ x₁ : X_1
X : Type u_3
inst_2 : IsEmpty X
⊢ IsEmpty.{u_3 + 1} (FundamentalGroupoid X)

Tactic:
equiv _ |>.isEmpty

Premises used: FundamentalGroupoid.equiv, Equiv.isEmpty
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_3
⊢ Nonempty.{u_3 + 1} (FundamentalGroupoid X) ↔ Nonempty X

Tactic:
equiv _ |>.nonempty_congr

Premises used: FundamentalGroupoid.equiv, Equiv.nonempty_congr
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x₀ x₁ : X_1
X : Type u_3
inst_2 : Nonempty X
⊢ Nonempty.{u_3 + 1} (FundamentalGroupoid X)

Tactic:
equiv _ |>.nonempty

Premises used: FundamentalGroupoid.equiv, Equiv.nonempty
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_3
⊢ Subsingleton.{u_3 + 1} (FundamentalGroupoid X) ↔ Subsingleton X

Tactic:
equiv _ |>.subsingleton_congr

Premises used: Equiv.subsingleton_congr, FundamentalGroupoid.equiv
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x₀ x₁ : X_1
X : Type u_3
inst_2 : Subsingleton X
⊢ Subsingleton.{u_3 + 1} (FundamentalGroupoid X)

Tactic:
equiv _ |>.subsingleton

Premises used: FundamentalGroupoid.equiv, Equiv.subsingleton
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
X_1 Y_1 : FundamentalGroupoid X
f_1 : Path.Homotopic.Quotient X_1.as Y_1.as
f : Path X_1.as Y_1.as
⊢ Path.Homotopic.Quotient.trans ⟦Path.refl X_1.as⟧
      (Quot.mk (⇑(Path.Homotopic.setoid X_1.as Y_1.as) : Path X_1.as Y_1.as → Path X_1.as Y_1.as → Prop) f) =
    Quot.mk (⇑(Path.Homotopic.setoid X_1.as Y_1.as) : Path X_1.as Y_1.as → Path X_1.as Y_1.as → Prop) f

Tactic:
Quotient.sound ⟨Path.Homotopy.reflTrans f⟩

Premises used: Quotient.map₂, Path.Homotopy.reflTrans, Path.Homotopic.Quotient, Nonempty.intro, Path.Homotopic.Quotient.trans, Quotient.sound
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
X_1 Y_1 : FundamentalGroupoid X
f_1 : Path.Homotopic.Quotient X_1.as Y_1.as
f : Path X_1.as Y_1.as
⊢ Path.Homotopic.Quotient.trans ⟦Path.refl X_1.as⟧
      (Quot.mk (⇑(Path.Homotopic.setoid X_1.as Y_1.as) : Path X_1.as Y_1.as → Path X_1.as Y_1.as → Prop) f) =
    Quot.mk (⇑(Path.Homotopic.setoid X_1.as Y_1.as) : Path X_1.as Y_1.as → Path X_1.as Y_1.as → Prop) f

Tactic:
exact Quotient.sound ⟨Path.Homotopy.reflTrans f⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
X_1 Y_1 : FundamentalGroupoid X
f_1 : Path.Homotopic.Quotient X_1.as Y_1.as
f : Path X_1.as Y_1.as
⊢ Path.Homotopic.Quotient.trans
      (Quot.mk (⇑(Path.Homotopic.setoid X_1.as Y_1.as) : Path X_1.as Y_1.as → Path X_1.as Y_1.as → Prop) f)
      ⟦Path.refl Y_1.as⟧ =
    Quot.mk (⇑(Path.Homotopic.setoid X_1.as Y_1.as) : Path X_1.as Y_1.as → Path X_1.as Y_1.as → Prop) f

Tactic:
Quotient.sound ⟨Path.Homotopy.transRefl f⟩

Premises used: Path.Homotopy.transRefl, Quotient.map₂, Path.Homotopic.Quotient, Nonempty.intro, Path.Homotopic.Quotient.trans, Quotient.sound
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
X_1 Y_1 : FundamentalGroupoid X
f_1 : Path.Homotopic.Quotient X_1.as Y_1.as
f : Path X_1.as Y_1.as
⊢ Path.Homotopic.Quotient.trans
      (Quot.mk (⇑(Path.Homotopic.setoid X_1.as Y_1.as) : Path X_1.as Y_1.as → Path X_1.as Y_1.as → Prop) f)
      ⟦Path.refl Y_1.as⟧ =
    Quot.mk (⇑(Path.Homotopic.setoid X_1.as Y_1.as) : Path X_1.as Y_1.as → Path X_1.as Y_1.as → Prop) f

Tactic:
exact Quotient.sound ⟨Path.Homotopy.transRefl f⟩