pullback lemma

Stream: mathlib4

[Klaus Gy]

this is my first try with Lean. there is this theorem

theorem of_horiz_isIso [IsIso fst] [IsIso g] (sq : CommSq fst snd f g) : IsPullback fst snd f g :=
  of_isLimit' sq
    (by
      refine
        PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by simp)
          (fun s => ?_) (by aesop_cat)
      simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition])

but i needed a stronger version with g being only mono. replacing IsIso g with Mono gand leaving the proof untouched seemed to typecheck just fine, does that mean I improved the theorem?

[Aaron Liu]

Maybe

[Adam Topaz]

Yes, that's right. The only thing about g that's used as far as I can tell is cancel_mono g which (of course) works for [Mono g].

[Klaus Gy]

cool, if i want to contribute to mathlib one day, should i in a case like this duplicate the theorem or just change it to the stronger form?

[Joël Riou]

The name of the more general lemma would have to be different, so that I think the best would be to have two lemmas, with of_horiz_isIso just applying the more general lemma.

[Klaus Gy]

i have it now like this:

theorem of_horiz_isIso_mono [IsIso fst] [Mono g] (sq : CommSq fst snd f g) :
    IsPullback fst snd f g :=
  of_isLimit' sq
    (by
      refine
        PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by simp)
          (fun s => ?_) (by aesop_cat)
      simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition])

theorem of_horiz_isIso [IsIso fst] [IsIso g] (sq : CommSq fst snd f g) : IsPullback fst snd f g :=
  of_horiz_isIso_mono sq