Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
toHomf : E.Hom F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
fh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
toHomg : E.Hom F.toPreZeroHypercover
gs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomg.s₀ i) (toHomg.s₀ j)
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (gs₁ k)
w₁₁✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (gs₁ k) = E.p₁ k ≫ toHomg.h₀ i
w₁₂✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (gs₁ k) = E.p₂ k ≫ toHomg.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₀ =
    { toHom := toHomg, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₀
hh₀ :
  ∀ (i : E.I₀),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.h₀ i =
      { toHom := toHomg, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯) ({ toHom := toHomg, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.h₁ k =
      { toHom := toHomg, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.h₁ k ≫
        (congrIndexOneOfEqIso ⋯ ⋯ ({ toHom := toHomg, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)).inv ≫
          eqToHom ⋯
⊢ { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ } =
    { toHom := toHomg, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }

Tactic:
obtain rfl : toHomf = toHomg := PreZeroHypercover.Hom.ext' hs₀ hh₀

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
toHomf : E.Hom F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
fh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
gs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (gs₁ k)
w₁₁✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (gs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (gs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₀ =
    { toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₀
hh₀ :
  ∀ (i : E.I₀),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.h₀ i =
      { toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯) ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.h₁ k =
      { toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.h₁ k ≫
        (congrIndexOneOfEqIso ⋯ ⋯ ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)).inv ≫
          eqToHom ⋯
⊢ { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ } =
    { toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }