awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
apply :
  ∀ (t : (↑I : Type)),
    Eq (α := (↑Y : Type u))
      ((g : (a : (↑X : Type u)) → (↑Y : Type u)) ((p' : (a : (↑I : Type)) → (↑X : Type u)) t : (↑X : Type u)) :
        (↑Y : Type u))
      ((H.uliftMap : (a : (↑(TopCat.of (ULift.{u, 0} (↑I : Type) × (↑X : Type u))) : Type u)) → (↑Y : Type u))
          ((Path.prod (Path.refl { down := 1 }) p' :
                (a : (↑I : Type)) → (↑(TopCat.of (ULift.{u, 0} (↑I : Type) × (↑X : Type u))) : Type u))
              t :
            (↑(TopCat.of (ULift.{u, 0} (↑I : Type) × (↑X : Type u))) : Type u)) :
        (↑Y : Type u))
⊢ (π.map (TopCat.ofHom g)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) ⟦p'⟧) ≫ hcast ⋯

Tactic:
apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')

Premises used: ContinuousMap.Homotopy.eq_path_of_eq_image
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t : (↑I : Type)
rw :
  Eq (α := (↑Y : Type u))
    ((g : (a : (↑X : Type u)) → (↑Y : Type u)) ((p' : (a : (↑I : Type)) → (↑X : Type u)) t : (↑X : Type u)) :
      (↑Y : Type u))
    ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u))
        ((ULift.down.{u, 0} ((Path.refl { down := 1 } : (a : (↑I : Type)) → ULift.{u, 0} (↑I : Type)) t),
            (p' : (a : (↑I : Type)) → (↑X : Type u)) t) :
          (↑I : Type) × (↑X : Type u)) :
      (↑Y : Type u))
⊢ Eq (α := (↑Y : Type u))
    ((g : (a : (↑X : Type u)) → (↑Y : Type u)) ((p' : (a : (↑I : Type)) → (↑X : Type u)) t : (↑X : Type u)) :
      (↑Y : Type u))
    ((H.uliftMap : (a : (↑(TopCat.of (ULift.{u, 0} (↑I : Type) × (↑X : Type u))) : Type u)) → (↑Y : Type u))
        ((Path.prod (Path.refl { down := 1 }) p' :
              (a : (↑I : Type)) → (↑(TopCat.of (ULift.{u, 0} (↑I : Type) × (↑X : Type u))) : Type u))
            t :
          (↑(TopCat.of (ULift.{u, 0} (↑I : Type) × (↑X : Type u))) : Type u)) :
      (↑Y : Type u))

Tactic:
rw [Path.prod_coe, ulift_apply H]

Premises used: ContinuousMap.Homotopy.ulift_apply, Path.prod_coe
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t : (↑I : Type)
⊢ Eq (α := (↑Y : Type u))
    ((g : (a : (↑X : Type u)) → (↑Y : Type u)) ((p' : (a : (↑I : Type)) → (↑X : Type u)) t : (↑X : Type u)) :
      (↑Y : Type u))
    ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u))
        ((ULift.down.{u, 0} ((Path.refl { down := 1 } : (a : (↑I : Type)) → ULift.{u, 0} (↑I : Type)) t),
            (p' : (a : (↑I : Type)) → (↑X : Type u)) t) :
          (↑I : Type) × (↑X : Type u)) :
      (↑Y : Type u))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x : (↑X : Type u)
dsimp :
  Eq (α :=
    Quotient (α :=
      Path (X := (↑Y : Type u)) ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
        ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)))
      (Path.Homotopic.setoid ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x)
          ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x) :
        Setoid
          (Path (X := (↑Y : Type u)) ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
            ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)))))
    (⟦H.evalAt x⟧ :
      Quotient (α :=
        Path (X := (↑Y : Type u)) ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
          ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)))
        (Path.Homotopic.setoid ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x)
            ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x) :
          Setoid
            (Path (X := (↑Y : Type u)) ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
              ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)))))
    (eqToHom ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) ≫
          eqToHom ⋯ :
      Quiver.Hom (V := (↑(π.obj Y) : Type u)) (fromTop ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x))
        (fromTop ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x)))
⊢ ⟦H.evalAt x⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x))) ≫ hcast ⋯

Tactic:
dsimp only [prodToProdTopI, uhpath01, hcast]

Premises used: unitInterval.uhpath01, ContinuousMap.Homotopy.hcast, ContinuousMap.Homotopy.prodToProdTopI
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x : (↑X : Type u)
⊢ Eq (α :=
    Quotient (α :=
      Path (X := (↑Y : Type u)) ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
        ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)))
      (Path.Homotopic.setoid ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x)
          ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x) :
        Setoid
          (Path (X := (↑Y : Type u)) ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
            ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)))))
    (⟦H.evalAt x⟧ :
      Quotient (α :=
        Path (X := (↑Y : Type u)) ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
          ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)))
        (Path.Homotopic.setoid ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x)
            ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x) :
          Setoid
            (Path (X := (↑Y : Type u)) ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
              ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u)))))
    (eqToHom ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) ≫
          eqToHom ⋯ :
      Quiver.Hom (V := (↑(π.obj Y) : Type u)) (fromTop ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x))
        (fromTop ((g : (a : (↑X : Type u)) → (↑Y : Type u)) x)))

Tactic:
(@conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _
    (FundamentalGroupoid.ext <| H.apply_one x).symm).mpr ?_

Premises used: Iff.mpr, Path.Homotopic.Quotient, Quotient, FundamentalGroupoid.ext, ContinuousMap.Homotopy.apply_one, CategoryTheory.conj_eqToHom_iff_heq, Eq.symm
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x : (↑X : Type u)
t : (↑I : Type)
⊢ Eq (α := (↑Y : Type u)) ((H.evalAt x : (a : (↑I : Type)) → (↑Y : Type u)) t : (↑Y : Type u))
    (((fun
                (q :
                  Path (X := ULift.{u, 0} (↑I : Type) × (↑X : Type u))
                    (as
                        (Functor.obj (C :=
                          (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                          (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                          ({ as := { down := 0 } }, { as := x })) :
                      ULift.{u, 0} (↑I : Type) × (↑X : Type u))
                    (as
                      (Functor.obj (C :=
                        (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                        (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                        ({ as := { down := 1 } }, { as := x })))) ↦
              q.map ⋯)
            (unitInterval.upath01.prod (Path.refl (fromTop x).as)) :
          (a : (↑I : Type)) → (↑Y : Type u))
        t :
      (↑Y : Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
rw :
  (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (prodToProdTopI (𝟙 (fromTop { down := 0 : ULift.{u, 0} (↑I : Type) })) p) ≫
            hcast ⋯) ≫
        ⟦H.evalAt x₁⟧ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (prodToProdTopI (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) })) p) ≫
            hcast ⋯ =
      H.diagonalPath' p
⊢ (π.map (TopCat.ofHom f)).map p ≫ ⟦H.evalAt x₁⟧ = H.diagonalPath' p ∧
    ⟦H.evalAt x₀⟧ ≫ (π.map (TopCat.ofHom g)).map p = H.diagonalPath' p

Tactic:
rw [H.apply_zero_path, H.apply_one_path, H.evalAt_eq]

Premises used: ContinuousMap.Homotopy.apply_zero_path, ContinuousMap.Homotopy.evalAt_eq, ContinuousMap.Homotopy.apply_one_path
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
erw :
  (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (prodToProdTopI (𝟙 (fromTop { down := 0 : ULift.{u, 0} (↑I : Type) })) p) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop (fromTop x₁).as))) ≫ hcast ⋯ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (prodToProdTopI (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) })) p) ≫
            hcast ⋯ =
      H.diagonalPath' p
⊢ (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (prodToProdTopI (𝟙 (fromTop { down := 0 : ULift.{u, 0} (↑I : Type) })) p) ≫
            hcast ⋯) ≫
        ⟦H.evalAt x₁⟧ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (prodToProdTopI (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) })) p) ≫
            hcast ⋯ =
      H.diagonalPath' p

Tactic:
erw [H.evalAt_eq]

Premises used: ContinuousMap.Homotopy.evalAt_eq
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
dsimp :
  CategoryStruct.comp (Y := (π.map (TopCat.ofHom f)).obj (fromTop x₁))
        (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (𝟙 (fromTop { down := 0 }), p)) ≫
            hcast ⋯)
        (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (uhpath01, 𝟙 (fromTop x₁))) ≫
            hcast ⋯) =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (uhpath01, 𝟙 (fromTop x₀))) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) }), p)) ≫
            hcast ⋯ =
      H.diagonalPath' p
⊢ (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (prodToProdTopI (𝟙 (fromTop { down := 0 : ULift.{u, 0} (↑I : Type) })) p) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop (fromTop x₁).as))) ≫ hcast ⋯ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (prodToProdTopI (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) })) p) ≫
            hcast ⋯ =
      H.diagonalPath' p

Tactic:
dsimp only [prodToProdTopI]

Premises used: ContinuousMap.Homotopy.prodToProdTopI
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
left :
  CategoryStruct.comp (Y := (π.map (TopCat.ofHom f)).obj (fromTop x₁))
      (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (𝟙 (fromTop { down := 0 }), p)) ≫
          hcast ⋯)
      (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (uhpath01, 𝟙 (fromTop x₁))) ≫
          hcast ⋯) =
    H.diagonalPath' p
right :
  (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (uhpath01, 𝟙 (fromTop x₀))) ≫
          hcast ⋯) ≫
      hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) }), p)) ≫
          hcast ⋯ =
    H.diagonalPath' p
⊢ CategoryStruct.comp (Y := (π.map (TopCat.ofHom f)).obj (fromTop x₁))
        (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (𝟙 (fromTop { down := 0 }), p)) ≫
            hcast ⋯)
        (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (uhpath01, 𝟙 (fromTop x₁))) ≫
            hcast ⋯) =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (uhpath01, 𝟙 (fromTop x₀))) ≫
            hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) }), p)) ≫
            hcast ⋯ =
      H.diagonalPath' p

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
a :
  ((π.map (TopCat.ofHom H.uliftMap)).map
        (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
          (𝟙 (fromTop { down := 0 }), p)) ≫
      𝟙
        ((π.map (TopCat.ofHom H.uliftMap)).obj
          (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
            (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            ({ as := { down := 0 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
              { as := x₁ : FundamentalGroupoid (↑X : Type u) }))) :
    Quiver.Hom (V := (↑(π.obj (TopCat.of (↑Y : Type u))) : Type u))
      (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₀)))
      (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₁))))
| ((π.map (TopCat.ofHom H.uliftMap)).map
        (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
          (𝟙 (fromTop { down := 0 }), p)) ≫
      hcast ⋯ ≫ hcast ⋯ :
    Quiver.Hom (V := (↑(π.obj (TopCat.of (↑Y : Type u))) : Type u))
      (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₀)))
      (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₁))))

Tactic:
rw [eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_trans
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
left :
  hcast ⋯ ≫
      CategoryStruct.comp (Y := fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₁)))
          ((π.map (TopCat.ofHom H.uliftMap)).map
                (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                  (𝟙 (fromTop { down := 0 }), p)) ≫
              𝟙
                ((π.map (TopCat.ofHom H.uliftMap)).obj
                  (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                    (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                    ({ as := { down := 0 : ULift.{u, 0} (↑I : Type) } :
                        FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
                      { as := x₁ : FundamentalGroupoid (↑X : Type u) }))) :
            Quiver.Hom (V := (↑(π.obj (TopCat.of (↑Y : Type u))) : Type u))
              (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₀)))
              (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₁))))
          ((π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (uhpath01, 𝟙 (fromTop x₁))) :
            (π.map (TopCat.ofHom H.uliftMap)).obj
                (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                  (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                  ({ as := { down := 0 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
                    { as := x₁ : FundamentalGroupoid (↑X : Type u) })) ⟶
              (π.map (TopCat.ofHom H.uliftMap)).obj
                (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                  (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X) ({ as := { down := 1 } }, { as := x₁ }))) ≫
        hcast ⋯ =
    H.diagonalPath' p
⊢ CategoryStruct.comp (Y := (π.map (TopCat.ofHom f)).obj (fromTop x₁))
      (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (𝟙 (fromTop { down := 0 }), p)) ≫
          hcast ⋯)
      (hcast ⋯ ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (uhpath01, 𝟙 (fromTop x₁))) ≫
          hcast ⋯) =
    H.diagonalPath' p

Tactic:
slice_lhs 2 4 => rw [eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_trans
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
a :
  ((π.map (TopCat.ofHom H.uliftMap)).map
      (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X) (Prod.mkHom uhpath01 p)) :
    (π.map (TopCat.ofHom H.uliftMap)).obj
        { as := ({ down := 0 : ULift.{u, 0} (↑I : Type) }, x₀) :
          FundamentalGroupoid (ULift.{u, 0} (↑I : Type) × (↑X : Type u)) } ⟶
      (π.map (TopCat.ofHom H.uliftMap)).obj { as := ({ down := 1 }, x₁) })
| ((π.map (TopCat.ofHom H.uliftMap)).map
        (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
          (𝟙 (fromTop { down := 0 }), p)) ≫
      𝟙
          ((π.map (TopCat.ofHom H.uliftMap)).obj
            (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
              (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              ({ as := { down := 0 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
                { as := x₁ : FundamentalGroupoid (↑X : Type u) }))) ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
          (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            (uhpath01, 𝟙 (fromTop x₁))) :
    fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₀)) ⟶
      (π.map (TopCat.ofHom H.uliftMap)).obj
        (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
          (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
          ({ as := { down := 1 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
            { as := x₁ : FundamentalGroupoid (↑X : Type u) })))

Tactic:
simp [← CategoryTheory.Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x₀ x₁ : (↑X : Type u)
p : fromTop x₀ ⟶ fromTop x₁
left :
  hcast ⋯ ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            (Prod.mkHom uhpath01 p)) ≫
        hcast ⋯ =
    H.diagonalPath' p
⊢ hcast ⋯ ≫
      CategoryStruct.comp (Y := fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₁)))
          ((π.map (TopCat.ofHom H.uliftMap)).map
                (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                  (𝟙 (fromTop { down := 0 }), p)) ≫
              𝟙
                ((π.map (TopCat.ofHom H.uliftMap)).obj
                  (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                    (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                    ({ as := { down := 0 : ULift.{u, 0} (↑I : Type) } :
                        FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
                      { as := x₁ : FundamentalGroupoid (↑X : Type u) }))) :
            Quiver.Hom (V := (↑(π.obj (TopCat.of (↑Y : Type u))) : Type u))
              (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₀)))
              (fromTop ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (0, x₁))))
          ((π.map (TopCat.ofHom H.uliftMap)).map
              (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                (uhpath01, 𝟙 (fromTop x₁))) :
            (π.map (TopCat.ofHom H.uliftMap)).obj
                (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                  (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
                  ({ as := { down := 0 : ULift.{u, 0} (↑I : Type) } : FundamentalGroupoid (ULift.{u, 0} (↑I : Type)) },
                    { as := x₁ : FundamentalGroupoid (↑X : Type u) })) ⟶
              (π.map (TopCat.ofHom H.uliftMap)).obj
                (Functor.obj (C := (↑(π.obj (TopCat.of (ULift.{u, 0} (↑I : Type)))) : Type u) × (↑(π.obj X) : Type u))
                  (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X) ({ as := { down := 1 } }, { as := x₁ }))) ≫
        hcast ⋯ =
    H.diagonalPath' p

Tactic:
slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp