Lean4
/-- The constructed `GlueData` of a `GlueData'`, where `GlueData'` is a variant of `GlueData` that only
requires conditions on `V (i, j)` when `i ≠ j`.
-/
def ofGlueData' (D : GlueData' C) : GlueData C where
J := D.J
U := D.U
V ij := if h : ij.1 = ij.2 then D.U ij.1 else D.V ij.1 ij.2 h
f i j := D.f' i j
f_id i := by simp only [↓reduceDIte, GlueData'.f']; infer_instance
t i
j :=
if h : i = j then eqToHom (by simp [h]) else eqToHom (dif_neg h) ≫ D.t i j h ≫ eqToHom (dif_neg (Ne.symm h)).symm
t_id i := by simp
t' := D.t''
t_fac i j
k := by
delta GlueData'.t''
obtain rfl | _ := eq_or_ne i j
· simp
obtain rfl | _ := eq_or_ne i k
· simp [*]
obtain rfl | _ := eq_or_ne j k
· simp [*]
· simp [*, reassoc_of% D.t_fac]
cocycle i j
k := by
delta GlueData'.t''
if hij : i = j then
subst hij
if hik : i = k then
subst hik
ext <;> simp
else simp [hik, Ne.symm hik, fst_eq_snd_of_mono_eq]
else
if hik : i = k then
subst hik
ext <;> simp [hij, Ne.symm hij, fst_eq_snd_of_mono_eq, pullback.condition_assoc]
else
if hjk : j = k then
subst hjk
ext <;> simp [hij, Ne.symm hij, fst_eq_snd_of_mono_eq]
else ext <;> simp [hij, Ne.symm hij, hik, Ne.symm hik, hjk, Ne.symm hjk, pullback.map_comp_assoc]
