Using aesop_cat to prove paths are homotopic

Stream: Is there code for X?

[Sebastian Kumar]

I was formalizing some algebraic topology, and I ended up needing to prove a result along the lines of:

import Mathlib

example {X : Type*} [TopologicalSpace X] {a : X} (f : Path a a) :
    ((Path.refl a).trans (f.trans (Path.refl a))).Homotopic f := sorry

One could do this directly with Path.Homotopic.trans, Path.Homotopy.reflTrans, and such lemmas, but it is a bit annoying (and my actual example was much more complicated). I ended up coming up with the following solution using aesop_cat:

import Mathlib

namespace CategoryTheory

lemma my_lemma (obj : Type u) [Category obj] {X Y : obj} (f : X ⟶ Y) :
    𝟙 X ≫ (f ≫ 𝟙 Y) = f := by aesop_cat

end CategoryTheory

example {X : Type*} [TopologicalSpace X] {a : X} (f : Path a a) :
    ((Path.refl a).trans (f.trans (Path.refl a))).Homotopic f :=
  Quotient.exact (CategoryTheory.my_lemma (FundamentalGroupoid X) ⟦_⟧)

At first I was proud of this. But the use of an overly specific lemma is annoying and messy. How could I modify my code to avoid this? I tried a few things (e.g., using show, refine, ...) but I couldn't figure anything out.

[Kenny Lau]

your code contains nbsp for some reason

[Kenny Lau]

import Mathlib

variable {X : Type*} [TopologicalSpace X] {x y z : X}

open CategoryTheory

namespace FundamentalGroupoid

nonrec abbrev mkHom (f : Path x y) : mk x ⟶ mk y :=
  Quotient.mk _ f

@[simp] lemma mkHom_trans (f : Path x y) (g : Path y z) :
    mkHom (f.trans g) = (mkHom f) ≫ (mkHom g) :=
  rfl

@[simp] lemma mkHom_refl : mkHom (Path.refl x) = 𝟙 _ :=
  rfl

end FundamentalGroupoid

theorem foo {f g : Path x y} (ih : FundamentalGroupoid.mkHom f = FundamentalGroupoid.mkHom g) :
    f.Homotopic g :=
  Quotient.exact ih

example {X : Type*} [TopologicalSpace X] {a : X} (f : Path a a) :
    ((Path.refl a).trans (f.trans (Path.refl a))).Homotopic f :=
  foo (by aesop)

[Kenny Lau]

@Sebastian Kumar I believe the library is missing the above abbrev to make everything smoother

[Kenny Lau]

but that's a design question, I expect not everyone will agree with me