awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.261170, v, u} S_1
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i_1 i' j_1 j' : E.I₀
hii' : i_1 = i'
hjj' : j_1 = j'
i j : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
k : E.I₁ i j
⊢ F.Y (u₁ i j ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k)) =
    F.Y (i₁ := u₀ i) (i₂ := u₀ j) ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i) (u₀ j)) (u₁ i j k))

Tactic:
simp [congrIndexOneOfEq]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEq
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i i' j j' : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
subst :
  (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ z i j ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) ≫ eqToHom ⋯ =
    z i j k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k))
⊢ (congrIndexOneOfEqIso hii' hjj' k).inv ≫
      z i' j' ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k) ≫ eqToHom ⋯ =
    z i j k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k))

Tactic:
subst hii' hjj'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i j : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ z i j ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) ≫ eqToHom ⋯ =
    z i j k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k))

Tactic:
simp [congrIndexOneOfEqIso, congrIndexOneOfEq]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso, CategoryTheory.PreOneHypercover.congrIndexOneOfEq
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.263665, v, u} S
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
i : E.I₀
⊢ F.X (g.s₀ i) = F.X (f.s₀ i)

Tactic:
simp [hs₀]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.263665, v, u} S
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ i = f.s₀ i

Tactic:
simp [hs₀]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.263665, v, u} S
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ j = f.s₀ j

Tactic:
simp [hs₀]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E_2 : PreOneHypercover.{w, v, u} S
F_1 : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.263665, v, u} S
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    f.s₁ k = (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (g.s₀ i) (g.s₀ j)) → F.I₁ (f.s₀ i) (f.s₀ j)) (g.s₁ k)
i j : E.I₀
k : E.I₁ i j
rw rw₁ : F.Y (f.s₁ k) = F.Y (f.s₁ k)
⊢ F.Y (i₁ := f.s₀ i) (i₂ := f.s₀ j)
      ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (g.s₀ i) (g.s₀ j)) → F.I₁ (f.s₀ i) (f.s₀ j)) (g.s₁ k)) =
    F.Y (f.s₁ k)

Tactic:
rw [PreOneHypercover.congrIndexOneOfEq_congrFun hs₀ hs₁]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEq_congrFun
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    f.s₁ k = (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (g.s₀ i) (g.s₀ j)) → F.I₁ (f.s₀ i) (f.s₀ j)) (g.s₁ k)
hh₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = g.h₁ k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)) ≫ eqToHom ⋯
obtain :
  ∀ (toHomf : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover)
    (fs₁ : {i j : E.I₀} → (k : 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)
    (hs₀ : { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₀ = g.s₀)
    (hh₀ :
      ∀ (i : E.I₀),
        { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₀ i = g.h₀ i ≫ eqToHom ⋯)
    (hs₁ :
      ∀ (i j : E.I₀) (k : E.I₁ i j),
        { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₁ k =
          (congrIndexOneOfEq ⋯ ⋯ :
              (a : F.I₁ (g.s₀ i) (g.s₀ j)) →
                F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ i)
                  ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ j))
            (g.s₁ k))
    (hh₁ :
      ∀ (i j : E.I₀) (k : E.I₁ i j),
        { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₁ k =
          g.h₁ k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)) ≫ eqToHom ⋯),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F } = g
⊢ f = g

Tactic:
obtain ⟨toHomf, fs₁, fh₁⟩ := f
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
toHomf : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → (k : 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 : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover
gs₁ : {i j : E.I₀} → (k : 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₁₁_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (gs₁ k) = E.p₁ k ≫ toHomg.h₀ i
w₁₂_1 : ∀ {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₁₂ : E.Hom F }.s₀ =
    { toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₀
hh₀ :
  ∀ (i : E.I₀),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₀ i =
      { toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a :
              F.I₁ ({ toHom := toHomg, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ i)
                ({ toHom := toHomg, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ j)) →
            F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ i)
              ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ j))
        ({ toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₁ k =
      { toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.h₁ k ≫
        Iso.inv
            (congrIndexOneOfEqIso ⋯ ⋯
              ({ toHom := toHomg, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.s₁ k)) ≫
          eqToHom ⋯
⊢ toHomf = toHomg

Tactic:
PreZeroHypercover.Hom.ext' hs₀ hh₀

Premises used: CategoryTheory.PreZeroHypercover.Hom.ext'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
toHomf : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → (k : 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₀} → (k : 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₁₁_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (gs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂_1 : ∀ {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₁₂ : E.Hom F }.s₀ =
    { toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₀
hh₀ :
  ∀ (i : E.I₀),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₀ i =
      { toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a :
              F.I₁ ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ i)
                ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ j)) →
            F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ i)
              ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ j))
        ({ toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₁ k =
      { toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.h₁ k ≫
        Iso.inv
            (congrIndexOneOfEqIso ⋯ ⋯
              ({ toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.s₁ k)) ≫
          eqToHom ⋯
h : ∀ (i j : E.I₀) (k : E.I₁ i j), fs₁ k = gs₁ k
⊢ @fs₁ = @gs₁

Tactic:
ext i j k
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
toHomf : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → (k : 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₀} → (k : 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₁₁_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (gs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂_1 : ∀ {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₁₂ : E.Hom F }.s₀ =
    { toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₀
hh₀ :
  ∀ (i : E.I₀),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₀ i =
      { toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a :
              F.I₁ ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ i)
                ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ j)) →
            F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ i)
              ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ j))
        ({ toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₁ k =
      { toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.h₁ k ≫
        Iso.inv
            (congrIndexOneOfEqIso ⋯ ⋯
              ({ toHom := toHomf, s₁ := @gs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.s₁ k)) ≫
          eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ fs₁ k = gs₁ k

Tactic:
simpa using hs₁ i j k
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
toHomf : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → (k : 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
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₀ =
    { toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₀
hh₀ :
  ∀ (i : E.I₀),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₀ i =
      { toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a :
              F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ i)
                ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ j)) →
            F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ i)
              ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ j))
        ({ toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.h₁ k =
      { toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.h₁ k ≫
        Iso.inv
            (congrIndexOneOfEqIso ⋯ ⋯
              ({ toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 : E.Hom F }.s₁ k)) ≫
          eqToHom ⋯
simp_all :
  ∀
    (hh₁ :
      ∀ (i j : E.I₀) (k : E.I₁ i j),
        fh₁ k =
          gh₁ k ≫
            𝟙
              (F.Y (i₁ := toHomf.s₀ i) (i₂ := toHomf.s₀ j)
                ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)) → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j))
                  (fs₁ k)))),
    @fh₁ = @gh₁
⊢ { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F } =
    { toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }

Tactic:
simp_all only [eqToHom_refl, Category.comp_id, implies_true, congrIndexOneOfEqIso_refl,
    Iso.refl_inv, mk.injEq, heq_eq_eq, true_and]

Premises used: heq_eq_eq, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_refl, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Iso.refl_inv, CategoryTheory.PreOneHypercover.Hom.mk.injEq, implies_true, true_and
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
toHomf : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → (k : 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
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₀ =
    { toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₀
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a :
              F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ i)
                ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ j)) →
            F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ i)
              ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ j))
        ({ toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    fh₁ k =
      gh₁ k ≫
        𝟙
          (F.Y (i₁ := toHomf.s₀ i) (i₂ := toHomf.s₀ j)
            ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)) → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j))
              (fs₁ k)))
h : ∀ (i j : E.I₀) (k : E.I₁ i j), fh₁ k = gh₁ k
⊢ @fh₁ = @gh₁

Tactic:
ext i j k
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
toHomf : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → (k : 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
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₀ =
    { toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₀
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a :
              F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ i)
                ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ j)) →
            F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ i)
              ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ j))
        ({ toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    fh₁ k =
      gh₁ k ≫
        𝟙
          (F.Y (i₁ := toHomf.s₀ i) (i₂ := toHomf.s₀ j)
            ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)) → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j))
              (fs₁ k)))
i j : E.I₀
k : E.I₁ i j
h :
  gh₁ k ≫
      𝟙
        (F.Y (i₁ := toHomf.s₀ i) (i₂ := toHomf.s₀ j)
          ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)) → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j))
            (fs₁ k))) =
    gh₁ k
⊢ fh₁ k = gh₁ k

Tactic:
rw [hh₁ i j k]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{u_2, v, u} S
F : PreOneHypercover.{u_3, v, u} S
toHomf : PreZeroHypercover.Hom.{u_3, u_2, v, u} E.toPreZeroHypercover F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → (k : 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
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂_1 : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₀ =
    { toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₀
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := @fs₁, h₁ := @fh₁, w₁₁ := @w₁₁, w₁₂ := @w₁₂ : E.Hom F }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a :
              F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ i)
                ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }.s₀ j)) →
            F.I₁ ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ i)
              ({ toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁, w₁₂ := w₁₂ }.s₀ j))
        ({ toHom := toHomf, s₁ := @fs₁, h₁ := @gh₁, w₁₁ := @w₁₁_1, w₁₂ := @w₁₂_1 }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    fh₁ k =
      gh₁ k ≫
        𝟙
          (F.Y (i₁ := toHomf.s₀ i) (i₂ := toHomf.s₀ j)
            ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)) → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j))
              (fs₁ k)))
i j : E.I₀
k : E.I₁ i j
⊢ gh₁ k ≫
      𝟙
        (F.Y (i₁ := toHomf.s₀ i) (i₂ := toHomf.s₀ j)
          ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)) → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j))
            (fs₁ k))) =
    gh₁ k

Tactic:
Category.comp_id _

Premises used: CategoryTheory.Category.comp_id