awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
W X_1 Y_1 Z : FundamentalGroupoid X
f_1 : Path.Homotopic.Quotient W.as X_1.as
f : Path W.as X_1.as
g_1 : Path.Homotopic.Quotient X_1.as Y_1.as
g : Path X_1.as Y_1.as
h_1 : Path.Homotopic.Quotient Y_1.as Z.as
h : Path Y_1.as Z.as
⊢ (Path.Homotopic.Quotient.trans
          (Quot.mk (⇑(Path.Homotopic.setoid W.as X_1.as) : Path W.as X_1.as → Path W.as X_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) g)).trans
      (Quot.mk (⇑(Path.Homotopic.setoid Y_1.as Z.as) : Path Y_1.as Z.as → Path Y_1.as Z.as → Prop) h) =
    Path.Homotopic.Quotient.trans
      (Quot.mk (⇑(Path.Homotopic.setoid W.as X_1.as) : Path W.as X_1.as → Path W.as X_1.as → Prop) f)
      (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) g)
        (Quot.mk (⇑(Path.Homotopic.setoid Y_1.as Z.as) : Path Y_1.as Z.as → Path Y_1.as Z.as → Prop) h))

Tactic:
Quotient.sound ⟨Path.Homotopy.transAssoc f g h⟩

Premises used: Quotient.map₂, Path.Homotopic.Quotient, Path.Homotopy.transAssoc, 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
W X_1 Y_1 Z : FundamentalGroupoid X
f_1 : Path.Homotopic.Quotient W.as X_1.as
f : Path W.as X_1.as
g_1 : Path.Homotopic.Quotient X_1.as Y_1.as
g : Path X_1.as Y_1.as
h_1 : Path.Homotopic.Quotient Y_1.as Z.as
h : Path Y_1.as Z.as
⊢ (Path.Homotopic.Quotient.trans
          (Quot.mk (⇑(Path.Homotopic.setoid W.as X_1.as) : Path W.as X_1.as → Path W.as X_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) g)).trans
      (Quot.mk (⇑(Path.Homotopic.setoid Y_1.as Z.as) : Path Y_1.as Z.as → Path Y_1.as Z.as → Prop) h) =
    Path.Homotopic.Quotient.trans
      (Quot.mk (⇑(Path.Homotopic.setoid W.as X_1.as) : Path W.as X_1.as → Path W.as X_1.as → Prop) f)
      (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) g)
        (Quot.mk (⇑(Path.Homotopic.setoid Y_1.as Z.as) : Path Y_1.as Z.as → Path Y_1.as Z.as → Prop) h))

Tactic:
exact Quotient.sound ⟨Path.Homotopy.transAssoc f g h⟩
-- 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
a b : Path X_1.as Y_1.as
h : a.Homotopy b
⊢ Eq.{u_1 + 1} (α := Path.Homotopic.Quotient Y_1.as X_1.as)
    ((fun (f : Path X_1.as Y_1.as) ↦
        (⟦f.symm⟧ : Quotient (α := Path Y_1.as X_1.as) (Path.Homotopic.setoid Y_1.as X_1.as)))
      a)
    ((fun (f : Path X_1.as Y_1.as) ↦
        (⟦f.symm⟧ : Quotient (α := Path Y_1.as X_1.as) (Path.Homotopic.setoid Y_1.as X_1.as)))
      b)

Tactic:
Quotient.sound ⟨h.symm₂⟩

Premises used: Path.Homotopy.symm₂, Path.Homotopic.Quotient, Nonempty.intro, 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
a b : Path X_1.as Y_1.as
h : a.Homotopy b
⊢ Eq.{u_1 + 1} (α := Path.Homotopic.Quotient Y_1.as X_1.as)
    ((fun (f : Path X_1.as Y_1.as) ↦
        (⟦f.symm⟧ : Quotient (α := Path Y_1.as X_1.as) (Path.Homotopic.setoid Y_1.as X_1.as)))
      a)
    ((fun (f : Path X_1.as Y_1.as) ↦
        (⟦f.symm⟧ : Quotient (α := Path Y_1.as X_1.as) (Path.Homotopic.setoid Y_1.as X_1.as)))
      b)

Tactic:
exact Quotient.sound ⟨h.symm₂⟩
-- 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
⊢ (Quotient.lift (fun (f : Path X_1.as Y_1.as) ↦ ⟦f.symm⟧) ⋯
          (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)).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⟧

Tactic:
Quotient.sound ⟨(Path.Homotopy.reflSymmTrans f).symm⟩

Premises used: Quotient.map₂, Path.Homotopic.Quotient, Nonempty.intro, Path.Homotopic.Quotient.trans, Quotient.sound, Path.Homotopy.symm, Path.Homotopy.reflSymmTrans
-- 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
⊢ (Quotient.lift (fun (f : Path X_1.as Y_1.as) ↦ ⟦f.symm⟧) ⋯
          (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)).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⟧

Tactic:
exact Quotient.sound ⟨(Path.Homotopy.reflSymmTrans f).symm⟩
-- 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)
      (Quotient.lift (fun (f : Path X_1.as Y_1.as) ↦ ⟦f.symm⟧) ⋯
        (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 X_1.as⟧

Tactic:
Quotient.sound ⟨(Path.Homotopy.reflTransSymm f).symm⟩

Premises used: Path.Homotopy.reflTransSymm, Quotient.map₂, Path.Homotopic.Quotient, Nonempty.intro, Path.Homotopic.Quotient.trans, Quotient.sound, Path.Homotopy.symm
-- 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)
      (Quotient.lift (fun (f : Path X_1.as Y_1.as) ↦ ⟦f.symm⟧) ⋯
        (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 X_1.as⟧

Tactic:
exact Quotient.sound ⟨(Path.Homotopy.reflTransSymm f).symm⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : FundamentalGroupoid X
p : x ⟶ y
q : y ⟶ z
⊢ p ≫ q = Path.Homotopic.Quotient.trans p q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x : FundamentalGroupoid X
⊢ Eq (α := x ⟶ x) (𝟙 x) ⟦Path.refl x.as⟧

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
f : C(X, Y)
X_1 Y_1 Z : FundamentalGroupoid X
f_1 : X_1 ⟶ Y_1
p : Path X_1.as Y_1.as
g : Y_1 ⟶ Z
q : Path Y_1.as Z.as
⊢ Eq (α :=
    Quiver.Hom (V := FundamentalGroupoid Y) ({ as := (f : (a : X) → Y) X_1.as } : FundamentalGroupoid Y)
      ({ as := (f : (a : X) → Y) Z.as } : FundamentalGroupoid Y))
    (Path.Homotopic.Quotient.map
      (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) p ≫
        Quot.mk (⇑(Path.Homotopic.setoid Y_1.as Z.as) : Path Y_1.as Z.as → Path Y_1.as Z.as → Prop) q)
      f)
    (Path.Homotopic.Quotient.map
        (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) p) f ≫
      Path.Homotopic.Quotient.map
        (Quot.mk (⇑(Path.Homotopic.setoid Y_1.as Z.as) : Path Y_1.as Z.as → Path Y_1.as Z.as → Prop) q) f)

Tactic:
congr_arg Quotient.mk'' (p.map_trans q f.continuous)

Premises used: ContinuousMap.continuous, Quotient.map, Quotient.mk'', Quotient.map₂, Path.Homotopic.Quotient.map, Path.Homotopic.Quotient, congr_arg, Path.Homotopic.Quotient.trans, Path.map_trans, Quotient, Quot.map
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
f : C(X, Y)
X_1 Y_1 Z : FundamentalGroupoid X
f_1 : X_1 ⟶ Y_1
p : Path X_1.as Y_1.as
g : Y_1 ⟶ Z
q : Path Y_1.as Z.as
⊢ Eq (α :=
    Quiver.Hom (V := FundamentalGroupoid Y) ({ as := (f : (a : X) → Y) X_1.as } : FundamentalGroupoid Y)
      ({ as := (f : (a : X) → Y) Z.as } : FundamentalGroupoid Y))
    (Path.Homotopic.Quotient.map
      (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) p ≫
        Quot.mk (⇑(Path.Homotopic.setoid Y_1.as Z.as) : Path Y_1.as Z.as → Path Y_1.as Z.as → Prop) q)
      f)
    (Path.Homotopic.Quotient.map
        (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) p) f ≫
      Path.Homotopic.Quotient.map
        (Quot.mk (⇑(Path.Homotopic.setoid Y_1.as Z.as) : Path Y_1.as Z.as → Path Y_1.as Z.as → Prop) q) f)

Tactic:
exact congr_arg Quotient.mk'' (p.map_trans q f.continuous)

Premises used: ContinuousMap.continuous, Quotient.mk'', congr_arg, Path.map_trans
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
e_map :
  Eq.{u_1 + 1} (α :=
    {X_1 Y : FundamentalGroupoid X} →
      (X_1 ⟶ Y) →
        Quiver.Hom (V := FundamentalGroupoid X)
          ({ as := (ContinuousMap.id X : (a : X) → X) X_1.as } : FundamentalGroupoid X)
          ({ as := (ContinuousMap.id X : (a : X) → X) Y.as } : FundamentalGroupoid X))
    (fun {X_1 Y : FundamentalGroupoid X} (p : X_1 ⟶ Y) ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X))
    fun {X_1 Y : FundamentalGroupoid X} (f : X_1 ⟶ Y) ↦ f
⊢ Eq.{u_1 + 1} (α := FundamentalGroupoid X ⥤ FundamentalGroupoid X)
    { obj := fun (x : FundamentalGroupoid X) ↦ { as := (ContinuousMap.id X : (a : X) → X) x.as },
      map := fun {X_1 Y : FundamentalGroupoid X} (p : X_1 ⟶ Y) ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X),
      map_id := ⋯, map_comp := ⋯ }
    (𝟭 (FundamentalGroupoid X))

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
e_map :
  ∀ (x y : FundamentalGroupoid X) (x_1 : x ⟶ y) (p : Path x.as y.as),
    Path.Homotopic.Quotient.map
        (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p) (ContinuousMap.id X) =
      Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p
⊢ Eq.{u_1 + 1} (α :=
    {X_1 Y : FundamentalGroupoid X} →
      (X_1 ⟶ Y) →
        Quiver.Hom (V := FundamentalGroupoid X)
          ({ as := (ContinuousMap.id X : (a : X) → X) X_1.as } : FundamentalGroupoid X)
          ({ as := (ContinuousMap.id X : (a : X) → X) Y.as } : FundamentalGroupoid X))
    (fun {X_1 Y : FundamentalGroupoid X} (p : X_1 ⟶ Y) ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X))
    fun {X_1 Y : FundamentalGroupoid X} (f : X_1 ⟶ Y) ↦ f

Tactic:
ext x y ⟨p⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : FundamentalGroupoid X
x_1 : x ⟶ y
p : Path x.as y.as
⊢ Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p)
      (ContinuousMap.id X) =
    Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
Z : Type u_3
inst_2 : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
e_map :
  Eq (α :=
    {X_1 Y_1 : FundamentalGroupoid X} →
      (X_1 ⟶ Y_1) →
        Quiver.Hom (V := FundamentalGroupoid Z) ({ as := (g.comp f : (a : X) → Z) X_1.as } : FundamentalGroupoid Z)
          ({ as := (g.comp f : (a : X) → Z) Y_1.as } : FundamentalGroupoid Z))
    (fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p (g.comp f))
    fun {X_1 Y_1 : FundamentalGroupoid X} (f_1 : X_1 ⟶ Y_1) ↦
    CategoryTheory.Functor.map
      { obj := fun (x : FundamentalGroupoid Y) ↦ { as := (g : (a : Y) → Z) x.as },
        map := fun {X Y_2 : FundamentalGroupoid Y} (p : X ⟶ Y_2) ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
        map_comp := ⋯ }
      (CategoryTheory.Functor.map
        { obj := fun (x : FundamentalGroupoid X) ↦ { as := (f : (a : X) → Y) x.as },
          map := fun {X_2 Y_2 : FundamentalGroupoid X} (p : X_2 ⟶ Y_2) ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
          map_comp := ⋯ }
        f_1)
⊢ Eq (α := CategoryTheory.Functor.{u_1, u_3, u_1, u_3} (FundamentalGroupoid X) (FundamentalGroupoid Z))
    { obj := fun (x : FundamentalGroupoid X) ↦ { as := (g.comp f : (a : X) → Z) x.as },
      map := fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p (g.comp f),
      map_id := ⋯, map_comp := ⋯ }
    (Functor.comp.{u_1, u_2, u_3, u_1, u_2, u_3} (D := FundamentalGroupoid Y)
      { obj := fun (x : FundamentalGroupoid X) ↦ { as := (f : (a : X) → Y) x.as },
        map := fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
        map_comp := ⋯ }
      { obj := fun (x : FundamentalGroupoid Y) ↦ { as := (g : (a : Y) → Z) x.as },
        map := fun {X Y_1 : FundamentalGroupoid Y} (p : X ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
        map_comp := ⋯ })

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
Z : Type u_3
inst_2 : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
e_map :
  ∀ (x y : FundamentalGroupoid X) (x_1 : x ⟶ y) (p : Path x.as y.as),
    Path.Homotopic.Quotient.map
        (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p) (g.comp f) =
      CategoryTheory.Functor.map
        { obj := fun (x : FundamentalGroupoid Y) ↦ { as := (g : (a : Y) → Z) x.as },
          map := fun {X Y_1 : FundamentalGroupoid Y} (p : X ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
          map_comp := ⋯ }
        (CategoryTheory.Functor.map
          { obj := fun (x : FundamentalGroupoid X) ↦ { as := (f : (a : X) → Y) x.as },
            map := fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
            map_comp := ⋯ }
          (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p))
⊢ Eq (α :=
    {X_1 Y_1 : FundamentalGroupoid X} →
      (X_1 ⟶ Y_1) →
        Quiver.Hom (V := FundamentalGroupoid Z) ({ as := (g.comp f : (a : X) → Z) X_1.as } : FundamentalGroupoid Z)
          ({ as := (g.comp f : (a : X) → Z) Y_1.as } : FundamentalGroupoid Z))
    (fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p (g.comp f))
    fun {X_1 Y_1 : FundamentalGroupoid X} (f_1 : X_1 ⟶ Y_1) ↦
    CategoryTheory.Functor.map
      { obj := fun (x : FundamentalGroupoid Y) ↦ { as := (g : (a : Y) → Z) x.as },
        map := fun {X Y_2 : FundamentalGroupoid Y} (p : X ⟶ Y_2) ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
        map_comp := ⋯ }
      (CategoryTheory.Functor.map
        { obj := fun (x : FundamentalGroupoid X) ↦ { as := (f : (a : X) → Y) x.as },
          map := fun {X_2 Y_2 : FundamentalGroupoid X} (p : X_2 ⟶ Y_2) ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
          map_comp := ⋯ }
        f_1)

Tactic:
ext x y ⟨p⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
Z : Type u_3
inst_2 : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
x y : FundamentalGroupoid X
x_1 : x ⟶ y
p : Path x.as y.as
⊢ Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p)
      (g.comp f) =
    CategoryTheory.Functor.map
      { obj := fun (x : FundamentalGroupoid Y) ↦ { as := (g : (a : Y) → Z) x.as },
        map := fun {X Y_1 : FundamentalGroupoid Y} (p : X ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
        map_comp := ⋯ }
      (CategoryTheory.Functor.map
        { obj := fun (x : FundamentalGroupoid X) ↦ { as := (f : (a : X) → Y) x.as },
          map := fun {X_1 Y_1 : FundamentalGroupoid X} (p : X_1 ⟶ Y_1) ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
          map_comp := ⋯ }
        (Quot.mk (⇑(Path.Homotopic.setoid x.as y.as) : Path x.as y.as → Path x.as y.as → Prop) p))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X Y : TopCat
x₀ x₁ : (↑X : Type u)
f : C((↑X : Type u), (↑Y : Type u))
p : Path.Homotopic.Quotient x₀ x₁
⊢ (π.map (TopCat.ofHom f)).map p = p.map f

Tactic:
rfl

Premises used: Quotient.map, Path.Homotopic.Quotient.map, Quot.map, rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
f g : Path x₀ x₁
⊢ fromPath (Path.Homotopic.Quotient.mk f) = fromPath (Path.Homotopic.Quotient.mk g) ↔ f.Homotopic g

Tactic:
⟨fun ih ↦ Quotient.exact ih, fun h ↦ Quotient.sound h⟩

Premises used: Iff.intro, Quotient.exact, Quotient.sound
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ x₁ : X
h : x₀ = x₁
subst : Eq (α := { as := x₀ : FundamentalGroupoid X } ⟶ { as := x₀ }) (eqToHom ⋯) ⟦Path.cast (Path.refl x₀) ⋯ ⋯⟧
⊢ Eq (α := { as := x₀ : FundamentalGroupoid X } ⟶ { as := x₁ }) (eqToHom ⋯) ⟦Path.cast (Path.refl x₁) h ⋯⟧

Tactic:
subst h
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x₀ : X
⊢ Eq (α := { as := x₀ : FundamentalGroupoid X } ⟶ { as := x₀ }) (eqToHom ⋯) ⟦Path.cast (Path.refl x₀) ⋯ ⋯⟧

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x y x' y' : X
p : Path x y
hx : x' = x
hy : y' = y
subst :
  ∀ {p : Path x' y'}, eqToHom ⋯ ≫ Path.Homotopic.Quotient.mk p ≫ eqToHom ⋯ = Path.Homotopic.Quotient.mk (p.cast ⋯ ⋯)
⊢ eqToHom ⋯ ≫ Path.Homotopic.Quotient.mk p ≫ eqToHom ⋯ = Path.Homotopic.Quotient.mk (p.cast hx hy)

Tactic:
subst hx hy
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x' y' : X
p : Path x' y'
⊢ eqToHom ⋯ ≫ Path.Homotopic.Quotient.mk p ≫ eqToHom ⋯ = Path.Homotopic.Quotient.mk (p.cast ⋯ ⋯)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
x : X
y : Y
h : (f : (a : X) → Y) x = y
p : Path x x
⊢ (mapOfEq f h : (a : FundamentalGroup X x) → FundamentalGroup Y y) (fromPath (Path.Homotopic.Quotient.mk p)) =
    fromPath (Path.Homotopic.Quotient.mk ((p.map ⋯).cast ⋯ ⋯))

Tactic:
FundamentalGroupoid.conj_eqToHom ..

Premises used: Eq.mpr, CategoryTheory.eqToHom, Quotient.map, Quotient.map₂, Path.Homotopic.Quotient.map, Path.Homotopic.Quotient, CategoryTheory.End, Path.Homotopic.Quotient.trans, Quotient, Quotient.mk', Quot.map, FundamentalGroupoid.conj_eqToHom, Path.Homotopic, FundamentalGroup, Path.Homotopic.Quotient.mk
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C((↑I : Type) × (↑I : Type), Y) :=
  F.comp (ContinuousMap.prodMap (ContinuousMap.id (↑I : Type)) (↑p : C((↑I : Type), X)))
p₁ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.trans (Path.refl 0) Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.id.trans (Path.refl 1)).prod (Path.trans (Path.refl 0) Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
⊢ (Path.trans (p.map ⋯) (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))

Tactic:
⟨((Fsq.map G).pathCast ?H0 ?H1).cast ?hp ?hq⟩

Premises used: Path.Homotopy.pathCast, Nonempty.intro, Path.Homotopy.cast, Path.Homotopic, Path.Homotopy.map
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C((↑I : Type) × (↑I : Type), Y) :=
  F.comp (ContinuousMap.prodMap (ContinuousMap.id (↑I : Type)) (↑p : C((↑I : Type), X)))
p₁ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.trans (Path.refl 0) Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.id.trans (Path.refl 1)).prod (Path.trans (Path.refl 0) Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
H0 : Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x₁ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (0, 0) : Y)
H1 : Eq.{u_2 + 1} (α := Y) ((g : (a : X) → Y) x₂ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (1, 1) : Y)
hp : (p₁.map ⋯).cast ⋯ ⋯ = Path.trans (p.map ⋯) (F.evalAt x₂)
hq : (p₂.map ⋯).cast ⋯ ⋯ = (F.evalAt x₁).trans (p.map ⋯)
⊢ (Path.trans (p.map ⋯) (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))

Tactic:
refine ⟨((Fsq.map G).pathCast ?H0 ?H1).cast ?hp ?hq⟩
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C((↑I : Type) × (↑I : Type), Y) :=
  F.comp (ContinuousMap.prodMap (ContinuousMap.id (↑I : Type)) (↑p : C((↑I : Type), X)))
p₁ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.trans (Path.refl 0) Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.id.trans (Path.refl 1)).prod (Path.trans (Path.refl 0) Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
⊢ Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x₁ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (0, 0) : Y)

Tactic:
aesop (add simp Path.trans_apply)

Premises used: Path.trans_apply
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C((↑I : Type) × (↑I : Type), Y) :=
  F.comp (ContinuousMap.prodMap (ContinuousMap.id (↑I : Type)) (↑p : C((↑I : Type), X)))
p₁ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.trans (Path.refl 0) Path.id).prod (Path.id.trans (Path.refl 1))
p₂ : Path (X := (↑I : Type) × (↑I : Type)) (0, 0) (1, 1) :=
  (Path.id.trans (Path.refl 1)).prod (Path.trans (Path.refl 0) Path.id)
Fsq : p₁.Homotopy p₂ :=
  prodHomotopy ((Homotopy.reflTrans Path.id).trans (Homotopy.transRefl Path.id).symm)
    ((Homotopy.transRefl Path.id).trans (Homotopy.reflTrans Path.id).symm)
⊢ Eq.{u_2 + 1} (α := Y) ((g : (a : X) → Y) x₂ : Y) ((G : (a : (↑I : Type) × (↑I : Type)) → Y) (1, 1) : Y)

Tactic:
aesop (add simp Path.trans_apply)

Premises used: Path.trans_apply