Lean4
/-- (Implementation detail) the constructed `GlueData.t'` from a `GlueData'`. -/
def t'' (D : GlueData' C) (i j k : D.J) : pullback (D.f' i j) (D.f' i k) ⟶ pullback (D.f' j k) (D.f' j i) :=
if hij : i = j then
(pullbackSymmetry _ _).hom ≫
pullback.map _ _ _ _ (eqToHom (by aesop)) (eqToHom (by aesop)) (eqToHom (by aesop)) (by aesop) (by aesop)
else
if hik : i = k then
have : IsIso (pullback.snd (D.f' j k) (D.f' j i)) := by subst hik; infer_instance
pullback.fst _ _ ≫
eqToHom (dif_neg hij) ≫ D.t _ _ _ ≫ eqToHom (dif_neg (Ne.symm hij)).symm ≫ inv (pullback.snd _ _)
else
if hjk : j = k then
have : IsIso (pullback.snd (D.f' j k) (D.f' j i)) :=
by
apply (config := { allowSynthFailures := true }) pullback_snd_iso_of_left_iso
simp only [hjk, GlueData'.f', ↓reduceDIte]
infer_instance
pullback.fst _ _ ≫
eqToHom (dif_neg hij) ≫ D.t _ _ _ ≫ eqToHom (dif_neg (Ne.symm hij)).symm ≫ inv (pullback.snd _ _)
else
haveI := Ne.symm hij
pullback.map _ _ _ _ (eqToHom (by aesop)) (eqToHom (by rw [dif_neg hik])) (eqToHom (by simp))
(by delta f'; aesop) (by delta f'; aesop) ≫
D.t' i j k hij hik hjk ≫
pullback.map _ _ _ _ (eqToHom (by aesop)) (eqToHom (by aesop)) (eqToHom (by simp)) (by delta f'; aesop)
(by delta f'; aesop)
