awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ (p₁.map ⋯).cast ⋯ ⋯ = Path.trans (p.map ⋯) (F.evalAt x₂)

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)
⊢ (p₂.map ⋯).cast ⋯ ⋯ = (F.evalAt x₁).trans (p.map ⋯)

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)
H : f.Homotopy g
x y : X
p : { as := x : FundamentalGroupoid X } ⟶ { as := y }
rcases :
  ∀ (p : Path { as := x : FundamentalGroupoid X }.as { as := y }.as),
    (map f).map (Path.Homotopic.Quotient.mk p) ≫ ⟦H.evalAt { as := y : FundamentalGroupoid X }.as⟧ =
      ⟦H.evalAt { as := x }.as⟧ ≫ (map g).map (Path.Homotopic.Quotient.mk p)
⊢ (map f).map p ≫ ⟦H.evalAt { as := y : FundamentalGroupoid X }.as⟧ = ⟦H.evalAt { as := x }.as⟧ ≫ (map g).map p

Tactic:
rcases Path.Homotopic.Quotient.mk_surjective p with ⟨p, rfl⟩

Premises used: rfl, Path.Homotopic.Quotient.mk_surjective
-- 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)
H : f.Homotopy g
x y : X
p : Path { as := x : FundamentalGroupoid X }.as { as := y }.as
simp :
  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))))
⊢ (map f).map (Path.Homotopic.Quotient.mk p) ≫ ⟦H.evalAt { as := y : FundamentalGroupoid X }.as⟧ =
    ⟦H.evalAt { as := x }.as⟧ ≫ (map g).map (Path.Homotopic.Quotient.mk p)

Tactic:
simp only [map_map, map_obj_as, Path.Homotopic.Quotient.mk''_eq_mk, comp_eq,
      ← Path.Homotopic.Quotient.mk_map, ← Path.Homotopic.Quotient.mk_trans]

Premises used: FundamentalGroupoid.map_map, FundamentalGroupoid.comp_eq, Path.Homotopic.Quotient.mk_map, FundamentalGroupoid.map_obj_as, Path.Homotopic.Quotient.mk_trans, Path.Homotopic.Quotient.mk''_eq_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)
H : f.Homotopy g
x y : X
p : Path { as := x : FundamentalGroupoid X }.as { as := y }.as
rw :
  ((p.map (⋯ : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y))).trans (H.evalAt y)).Homotopic
    ((H.evalAt x).trans (p.map (⋯ : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑g : (a : X) → Y))))
⊢ 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))))

Tactic:
rw [Path.Homotopic.Quotient.eq]

Premises used: Path.Homotopic.Quotient.eq
-- 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)
H : f.Homotopy g
x y : X
p : Path { as := x : FundamentalGroupoid X }.as { as := y }.as
⊢ ((p.map (⋯ : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y))).trans (H.evalAt y)).Homotopic
    ((H.evalAt x).trans (p.map (⋯ : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑g : (a : X) → Y))))

Tactic:
.map_trans_evalAt _ _

Premises used: Path.Homotopic.map_trans_evalAt
-- 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)
H : f.Homotopy g
x y : X
p : Path { as := x : FundamentalGroupoid X }.as { as := y }.as
⊢ ((p.map (⋯ : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑f : (a : X) → Y))).trans (H.evalAt y)).Homotopic
    ((H.evalAt x).trans (p.map (⋯ : Continuous.{u_1, u_2} (X := X) (Y := Y) (⇑g : (a : X) → Y))))

Tactic:
exact .map_trans_evalAt _ _
-- 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)
H : f.Homotopy g
⊢ IsIso (homotopicMapsNatIso H)

Tactic:
NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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
ε : map hequiv.invFun ⋙ map hequiv.toFun ≅ 𝟭 (FundamentalGroupoid 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)

Tactic:
apply CategoryTheory.Equivalence.mk (map hequiv.toFun) (map hequiv.invFun)

Premises used: ContinuousMap.HomotopyEquiv.invFun, FundamentalGroupoid.map, ContinuousMap.HomotopyEquiv.toFun, CategoryTheory.Equivalence.mk
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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

Tactic:
simpa only [FundamentalGroupoid.map_id, FundamentalGroupoid.map_comp]
      using (asIso (homotopicMapsNatIso hequiv.left_inv.some)).symm

Premises used: FundamentalGroupoid.map_comp, FundamentalGroupoidFunctor.homotopicMapsNatIso, Nonempty.some, ContinuousMap.HomotopyEquiv.left_inv, FundamentalGroupoid.map_id, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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
⊢ map hequiv.invFun ⋙ map hequiv.toFun ≅ 𝟭 (FundamentalGroupoid Y)

Tactic:
simpa only [FundamentalGroupoid.map_id, FundamentalGroupoid.map_comp]
      using asIso (homotopicMapsNatIso hequiv.right_inv.some)

Premises used: FundamentalGroupoid.map_comp, ContinuousMap.HomotopyEquiv.right_inv, FundamentalGroupoidFunctor.homotopicMapsNatIso, Nonempty.some, FundamentalGroupoid.map_id, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Goal:
X : TopCat
x₀ x₁ : (↑X : Type u)
hx₀ : x₀ = x₁
⊢ hcast hx₀ = eqToHom ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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))
simp : Path.Homotopic.Quotient.map ⟦p⟧ f ≍ Path.Homotopic.Quotient.map ⟦q⟧ g
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ ≍ (π.map (TopCat.ofHom g)).map ⟦q⟧

Tactic:
simp only [map_eq]

Premises used: FundamentalGroupoid.map_eq
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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))
hp :
  ∀ (t : (↑I : Type)),
    Eq.{u + 1} (α := (↑Y : Type u))
      (((fun (q : Path x₀ x₁) ↦ q.map ⋯) p : (a : (↑I : Type)) → (↑Y : Type u)) t : (↑Y : Type u))
      (((fun (q : Path x₂ x₃) ↦ q.map ⋯) q : (a : (↑I : Type)) → (↑Y : Type u)) t : (↑Y : Type u))
⊢ Path.Homotopic.Quotient.map ⟦p⟧ f ≍ Path.Homotopic.Quotient.map ⟦q⟧ g

Tactic:
apply Path.Homotopic.hpath_hext

Premises used: Path.Homotopic.hpath_hext
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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))
⊢ ∀ (t : (↑I : Type)),
    Eq.{u + 1} (α := (↑Y : Type u))
      (((fun (q : Path x₀ x₁) ↦ q.map ⋯) p : (a : (↑I : Type)) → (↑Y : Type u)) t : (↑Y : Type u))
      (((fun (q : Path x₂ x₃) ↦ q.map ⋯) q : (a : (↑I : Type)) → (↑Y : Type u)) t : (↑Y : Type u))

Tactic:
hfg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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))
⊢ ∀ (t : (↑I : Type)),
    Eq.{u + 1} (α := (↑Y : Type u))
      (((fun (q : Path x₀ x₁) ↦ q.map ⋯) p : (a : (↑I : Type)) → (↑Y : Type u)) t : (↑Y : Type u))
      (((fun (q : Path x₂ x₃) ↦ q.map ⋯) q : (a : (↑I : Type)) → (↑Y : Type u)) t : (↑Y : Type u))

Tactic:
exact hfg
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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)) ((p : (a : (↑I : Type)) → (↑X₁ : Type u)) 0 : (↑X₁ : Type u)) :
      (↑Y : Type u))
    ((g : (a : (↑X₂ : Type u)) → (↑Y : Type u)) ((q : (a : (↑I : Type)) → (↑X₂ : Type u)) 0 : (↑X₂ : Type u)) :
      (↑Y : Type u))

Tactic:
hfg 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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
h₁ : x₂ = (q : (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))

Tactic:
convert! hfg 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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))
⊢ x₀ = (p : (a : (↑I : Type)) → (↑X₁ : Type u)) 0

Tactic:
simp only [Path.source]

Premises used: Path.source
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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))
⊢ x₂ = (q : (a : (↑I : Type)) → (↑X₂ : Type u)) 0

Tactic:
simp only [Path.source]

Premises used: Path.source
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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)) ((p : (a : (↑I : Type)) → (↑X₁ : Type u)) 1 : (↑X₁ : Type u)) :
      (↑Y : Type u))
    ((g : (a : (↑X₂ : Type u)) → (↑Y : Type u)) ((q : (a : (↑I : Type)) → (↑X₂ : Type u)) 1 : (↑X₂ : Type u)) :
      (↑Y : Type u))

Tactic:
hfg 1

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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
h₁ : x₃ = (q : (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))

Tactic:
convert! hfg 1

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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))
⊢ x₁ = (p : (a : (↑I : Type)) → (↑X₁ : Type u)) 1

Tactic:
simp only [Path.target]

Premises used: Path.target
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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))
⊢ x₃ = (q : (a : (↑I : Type)) → (↑X₂ : Type u)) 1

Tactic:
simp only [Path.target]

Premises used: Path.target
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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))
rw : (π.map (TopCat.ofHom f)).map ⟦p⟧ ≍ (π.map (TopCat.ofHom g)).map ⟦q⟧
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom g)).map ⟦q⟧ ≫ hcast ⋯

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)]

Premises used: FundamentalGroupoid.fundamentalGroupoidFunctor, CategoryTheory.Functor.map, Quotient.mk, _private.0.ContinuousMap.Homotopy.end_path, TopCat.ofHom, FundamentalGroupoid.ext, _private.0.ContinuousMap.Homotopy.start_path, CategoryTheory.conj_eqToHom_iff_heq
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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⟧

Tactic:
heq_path_of_eq_image hfg

Premises used: ContinuousMap.Homotopy.heq_path_of_eq_image
-- Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
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⟧

Tactic:
exact heq_path_of_eq_image hfg

Premises used: ContinuousMap.Homotopy.heq_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
i : ULift.{u, 0} (↑I : Type)
x : (↑X : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((H.uliftMap : (a : (↑(TopCat.of (ULift.{u, 0} (↑I : Type) × (↑X : Type u))) : Type u)) → (↑Y : Type u)) (i, x) :
      (↑Y : Type u))
    ((H : (a : (↑I : Type) × (↑X : Type u)) → (↑Y : Type u)) (i.down, x) : (↑Y : Type u))

Tactic:
rfl

Premises used: 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₁
p' : Path (fromTop x₀).as (fromTop x₁).as
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))
⊢ (π.map (TopCat.ofHom f)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) ⟦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))
    ((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))
⊢ 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:
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))
    ((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:
simp