awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
x y : X
p : Path { as := x : FundamentalGroupoid X }.as { as := y }.as
⊢ Path.Homotopic.Quotient.mk
      ((p.map (⋯ : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y))).trans (H.evalAt y)) =
    Path.Homotopic.Quotient.mk
      ((H.evalAt x).trans (p.map (⋯ : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑g : (a : X) → Y))))
have rw : ((p.map (sorry : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y))).trans (H.evalAt y)).Homotopic
  ((H.evalAt x).trans (p.map (sorry : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑g : (a : X) → Y))))
Tactic: rw [Path.Homotopic.Quotient.eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X_1 : Type u_1
Y_1 : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
f g : C(X_1, Y_1)
X : Type u_3
Y : Type u_4
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
hequiv : X ≃ₕ Y
⊢ CategoryTheory.Equivalence.{u_3, u_4, u_3, u_4} (↑(π.obj (TopCat.of X)) : Type u_3)
    (↑(π.obj (TopCat.of Y)) : Type u_4)
have η : 𝟭 (FundamentalGroupoid X) ≅ map hequiv.toFun ⋙ map hequiv.invFun
Tactic: apply CategoryTheory.Equivalence.mk (map hequiv.toFun) (map hequiv.invFun)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X_1 : Type u_1
Y_1 : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
f g : C(X_1, Y_1)
X : Type u_3
Y : Type u_4
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
hequiv : X ≃ₕ Y
η : 𝟭 (FundamentalGroupoid X) ≅ map hequiv.toFun ⋙ map hequiv.invFun
⊢ CategoryTheory.Equivalence.{u_3, u_4, u_3, u_4} (↑(π.obj (TopCat.of X)) : Type u_3)
    (↑(π.obj (TopCat.of Y)) : Type u_4)
have ε : map hequiv.invFun ⋙ map hequiv.toFun ≅ 𝟭 (FundamentalGroupoid Y)
Tactic: apply CategoryTheory.Equivalence.mk (map hequiv.toFun) (map hequiv.invFun)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X₁ X₂ Y : TopCat
f : C((↑X₁ : Type u), (↑Y : Type u))
g : C((↑X₂ : Type u), (↑Y : Type u))
x₀ x₁ : (↑X₁ : Type u)
x₂ x₃ : (↑X₂ : Type u)
p : Path x₀ x₁
q : Path x₂ x₃
hfg :
  ∀ (t : (↑I : Type)),
    Eq (α := (↑Y : Type u))
      ((f : (a : (↑X₁ : Type u)) → (↑Y : Type u)) ((p : (a : (↑I : Type)) → (↑X₁ : Type u)) t : (↑X₁ : Type u)) :
        (↑Y : Type u))
      ((g : (a : (↑X₂ : Type u)) → (↑Y : Type u)) ((q : (a : (↑I : Type)) → (↑X₂ : Type u)) t : (↑X₂ : Type u)) :
        (↑Y : Type u))
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ ≍ (π.map (TopCat.ofHom g)).map ⟦q⟧
have simp : Path.Homotopic.Quotient.map ⟦p⟧ f ≍ Path.Homotopic.Quotient.map ⟦q⟧ g
Tactic: simp only [map_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X₁ X₂ Y : TopCat
f : C((↑X₁ : Type u), (↑Y : Type u))
g : C((↑X₂ : Type u), (↑Y : Type u))
x₀ x₁ : (↑X₁ : Type u)
x₂ x₃ : (↑X₂ : Type u)
p : Path x₀ x₁
q : Path x₂ x₃
hfg :
  ∀ (t : (↑I : Type)),
    Eq (α := (↑Y : Type u))
      ((f : (a : (↑X₁ : Type u)) → (↑Y : Type u)) ((p : (a : (↑I : Type)) → (↑X₁ : Type u)) t : (↑X₁ : Type u)) :
        (↑Y : Type u))
      ((g : (a : (↑X₂ : Type u)) → (↑Y : Type u)) ((q : (a : (↑I : Type)) → (↑X₂ : Type u)) t : (↑X₂ : Type u)) :
        (↑Y : Type u))
⊢ Path.Homotopic.Quotient.map ⟦p⟧ f ≍ Path.Homotopic.Quotient.map ⟦q⟧ g
have hp : ∀ (t : (↑I : Type)),
  Eq.{u + 1} (α := (↑Y : Type u))
    (((fun (q : Path x₀ x₁) ↦ q.map sorry) p : (a : (↑I : Type)) → (↑Y : Type u)) t : (↑Y : Type u))
    (((fun (q : Path x₂ x₃) ↦ q.map sorry) q : (a : (↑I : Type)) → (↑Y : Type u)) t : (↑Y : Type u))
Tactic: apply Path.Homotopic.hpath_hext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X₁ X₂ Y : TopCat
f : C((↑X₁ : Type u), (↑Y : Type u))
g : C((↑X₂ : Type u), (↑Y : Type u))
x₀ x₁ : (↑X₁ : Type u)
x₂ x₃ : (↑X₂ : Type u)
p : Path x₀ x₁
q : Path x₂ x₃
hfg :
  ∀ (t : (↑I : Type)),
    Eq (α := (↑Y : Type u))
      ((f : (a : (↑X₁ : Type u)) → (↑Y : Type u)) ((p : (a : (↑I : Type)) → (↑X₁ : Type u)) t : (↑X₁ : Type u)) :
        (↑Y : Type u))
      ((g : (a : (↑X₂ : Type u)) → (↑Y : Type u)) ((q : (a : (↑I : Type)) → (↑X₂ : Type u)) t : (↑X₂ : Type u)) :
        (↑Y : Type u))
⊢ Eq (α := (↑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))
have h : x₀ = (p : (a : (↑I : Type)) → (↑X₁ : Type u)) 0
Tactic: convert! hfg 0
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X₁ X₂ Y : TopCat
f : C((↑X₁ : Type u), (↑Y : Type u))
g : C((↑X₂ : Type u), (↑Y : Type u))
x₀ x₁ : (↑X₁ : Type u)
x₂ x₃ : (↑X₂ : Type u)
p : Path x₀ x₁
q : Path x₂ x₃
hfg :
  ∀ (t : (↑I : Type)),
    Eq (α := (↑Y : Type u))
      ((f : (a : (↑X₁ : Type u)) → (↑Y : Type u)) ((p : (a : (↑I : Type)) → (↑X₁ : Type u)) t : (↑X₁ : Type u)) :
        (↑Y : Type u))
      ((g : (a : (↑X₂ : Type u)) → (↑Y : Type u)) ((q : (a : (↑I : Type)) → (↑X₂ : Type u)) t : (↑X₂ : Type u)) :
        (↑Y : Type u))
h : x₀ = (p : (a : (↑I : Type)) → (↑X₁ : Type u)) 0
⊢ Eq (α := (↑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))
have h₁ : x₂ = (q : (a : (↑I : Type)) → (↑X₂ : Type u)) 0
Tactic: convert! hfg 0
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X₁ X₂ Y : TopCat
f : C((↑X₁ : Type u), (↑Y : Type u))
g : C((↑X₂ : Type u), (↑Y : Type u))
x₀ x₁ : (↑X₁ : Type u)
x₂ x₃ : (↑X₂ : Type u)
p : Path x₀ x₁
q : Path x₂ x₃
hfg :
  ∀ (t : (↑I : Type)),
    Eq (α := (↑Y : Type u))
      ((f : (a : (↑X₁ : Type u)) → (↑Y : Type u)) ((p : (a : (↑I : Type)) → (↑X₁ : Type u)) t : (↑X₁ : Type u)) :
        (↑Y : Type u))
      ((g : (a : (↑X₂ : Type u)) → (↑Y : Type u)) ((q : (a : (↑I : Type)) → (↑X₂ : Type u)) t : (↑X₂ : Type u)) :
        (↑Y : Type u))
⊢ Eq (α := (↑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))
have h : x₁ = (p : (a : (↑I : Type)) → (↑X₁ : Type u)) 1
Tactic: convert! hfg 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X₁ X₂ Y : TopCat
f : C((↑X₁ : Type u), (↑Y : Type u))
g : C((↑X₂ : Type u), (↑Y : Type u))
x₀ x₁ : (↑X₁ : Type u)
x₂ x₃ : (↑X₂ : Type u)
p : Path x₀ x₁
q : Path x₂ x₃
hfg :
  ∀ (t : (↑I : Type)),
    Eq (α := (↑Y : Type u))
      ((f : (a : (↑X₁ : Type u)) → (↑Y : Type u)) ((p : (a : (↑I : Type)) → (↑X₁ : Type u)) t : (↑X₁ : Type u)) :
        (↑Y : Type u))
      ((g : (a : (↑X₂ : Type u)) → (↑Y : Type u)) ((q : (a : (↑I : Type)) → (↑X₂ : Type u)) t : (↑X₂ : Type u)) :
        (↑Y : Type u))
h : x₁ = (p : (a : (↑I : Type)) → (↑X₁ : Type u)) 1
⊢ Eq (α := (↑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))
have h₁ : x₃ = (q : (a : (↑I : Type)) → (↑X₂ : Type u)) 1
Tactic: convert! hfg 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X₁ X₂ Y : TopCat
f : C((↑X₁ : Type u), (↑Y : Type u))
g : C((↑X₂ : Type u), (↑Y : Type u))
x₀ x₁ : (↑X₁ : Type u)
x₂ x₃ : (↑X₂ : Type u)
p : Path x₀ x₁
q : Path x₂ x₃
hfg :
  ∀ (t : (↑I : Type)),
    Eq (α := (↑Y : Type u))
      ((f : (a : (↑X₁ : Type u)) → (↑Y : Type u)) ((p : (a : (↑I : Type)) → (↑X₁ : Type u)) t : (↑X₁ : Type u)) :
        (↑Y : Type u))
      ((g : (a : (↑X₂ : Type u)) → (↑Y : Type u)) ((q : (a : (↑I : Type)) → (↑X₂ : Type u)) t : (↑X₂ : Type u)) :
        (↑Y : Type u))
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom g)).map ⟦q⟧ ≫ hcast ⋯
have rw : (π.map (TopCat.ofHom f)).map ⟦p⟧ ≍ (π.map (TopCat.ofHom g)).map ⟦q⟧
Tactic: rw [conj_eqToHom_iff_heq
    ((πₘ (TopCat.ofHom f)).map ⟦p⟧) ((πₘ (TopCat.ofHom g)).map ⟦q⟧)
    (FundamentalGroupoid.ext <| start_path hfg)
    (FundamentalGroupoid.ext <| end_path hfg)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
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
⊢ (π.map (TopCat.ofHom f)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) ⟦p'⟧) ≫ hcast ⋯
have apply : ∀ (t : (↑I : Type)),
  Eq (α := (↑Y : Type u))
    ((f : (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 := 0 }) 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: apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
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))
    ((f : (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 := 0 }) 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))
have rw : Eq (α := (↑Y : Type u))
  ((f : (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 := 0 } : (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: rw [Path.prod_coe, ulift_apply H]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
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
⊢ (π.map (TopCat.ofHom g)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) ⟦p'⟧) ≫ hcast ⋯
have 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))
Tactic: apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
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.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))
have 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))
Tactic: rw [Path.prod_coe, ulift_apply H]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
Goal:
X Y : TopCat
f g : C((↑X : Type u), (↑Y : Type u))
H : f.Homotopy g
x : (↑X : Type u)
⊢ ⟦H.evalAt x⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x))) ≫ hcast ⋯
have 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 sorry ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) ≫
        eqToHom sorry :
    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: dsimp only [prodToProdTopI, uhpath01, hcast]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
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₁
⊢ (π.map (TopCat.ofHom f)).map p ≫ ⟦H.evalAt x₁⟧ = H.diagonalPath' p ∧
    ⟦H.evalAt x₀⟧ ≫ (π.map (TopCat.ofHom g)).map p = H.diagonalPath' p
have rw : (hcast sorry ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (prodToProdTopI (𝟙 (fromTop { down := 0 : ULift.{u, 0} (↑I : Type) })) p) ≫
          hcast sorry) ≫
      ⟦H.evalAt x₁⟧ =
    H.diagonalPath' p ∧
  (hcast sorry ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast sorry) ≫
      hcast sorry ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (prodToProdTopI (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) })) p) ≫
          hcast sorry =
    H.diagonalPath' p
Tactic: rw [H.apply_zero_path, H.apply_one_path, H.evalAt_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
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₁
⊢ (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
have erw : (hcast sorry ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (prodToProdTopI (𝟙 (fromTop { down := 0 : ULift.{u, 0} (↑I : Type) })) p) ≫
          hcast sorry) ≫
      hcast sorry ≫
        (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop (fromTop x₁).as))) ≫ hcast sorry =
    H.diagonalPath' p ∧
  (hcast sorry ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast sorry) ≫
      hcast sorry ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (prodToProdTopI (𝟙 (fromTop { down := 1 : ULift.{u, 0} (↑I : Type) })) p) ≫
          hcast sorry =
    H.diagonalPath' p
Tactic: erw [H.evalAt_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
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₁
⊢ (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
have dsimp : CategoryStruct.comp (Y := (π.map (TopCat.ofHom f)).obj (fromTop x₁))
      (hcast sorry ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (𝟙 (fromTop { down := 0 }), p)) ≫
          hcast sorry)
      (hcast sorry ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (uhpath01, 𝟙 (fromTop x₁))) ≫
          hcast sorry) =
    H.diagonalPath' p ∧
  (hcast sorry ≫
        (π.map (TopCat.ofHom H.uliftMap)).map
            (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
              (uhpath01, 𝟙 (fromTop x₀))) ≫
          hcast sorry) ≫
      hcast sorry ≫
        (π.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 sorry =
    H.diagonalPath' p
Tactic: dsimp only [prodToProdTopI]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
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₁
⊢ 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
have left : CategoryStruct.comp (Y := (π.map (TopCat.ofHom f)).obj (fromTop x₁))
    (hcast sorry ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            (𝟙 (fromTop { down := 0 }), p)) ≫
        hcast sorry)
    (hcast sorry ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            (uhpath01, 𝟙 (fromTop x₁))) ≫
        hcast sorry) =
  H.diagonalPath' p
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps (goal)
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
⊢ 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
have right : (hcast sorry ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          (CategoryTheory.Functor.map (prodToProdTop (TopCat.of (ULift.{u, 0} (↑I : Type))) X)
            (uhpath01, 𝟙 (fromTop x₀))) ≫
        hcast sorry) ≫
    hcast sorry ≫
      (π.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 sorry =
  H.diagonalPath' p
Tactic: constructor