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.284030, v, u} S_1
S : C
E F : PreOneHypercover.{u_2, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)
h₁ :
  ⦃i j : E.I₀⦄ →
    (k : E.I₁ i j) →
      E.Y k ≅
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) i) (i₂ := (s₀ : (a : E.I₀) → F.I₀) j)
          ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
w₁₁ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₁ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₁ k ≫ (h₀ i).hom
w₁₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₂ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₂ k ≫ (h₀ j).hom
i j : F.I₀
k : F.I₁ i j
⊢ j = (s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)

Tactic:
simp
-- 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.284030, v, u} S_1
S : C
E F : PreOneHypercover.{u_2, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)
h₁ :
  ⦃i j : E.I₀⦄ →
    (k : E.I₁ i j) →
      E.Y k ≅
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) i) (i₂ := (s₀ : (a : E.I₀) → F.I₀) j)
          ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
w₁₁ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₁ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₁ k ≫ (h₀ i).hom
w₁₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₂ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₂ k ≫ (h₀ j).hom
i j : F.I₀
k : F.I₁ i j
⊢ F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i : E.I₀)) (i₂ :=
      (s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j : E.I₀))
      ((congrIndexOneOfEq ⋯ ⋯ :
          (a : F.I₁ i j) →
            F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i))
              ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j)))
        k) =
    F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) (i₂ := (s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))
      ((s₁ :
          (a : E.I₁ (__Hom.s₀ i) (__Hom.s₀ j)) →
            F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
        ((Equiv.symm s₁ :
            (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
              E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
          ((congrIndexOneOfEq ⋯ ⋯ :
              (a : F.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
            k)))

Tactic:
simp
-- 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.284030, v, u} S_1
S : C
E F : PreOneHypercover.{u_2, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)
h₁ :
  ⦃i j : E.I₀⦄ →
    (k : E.I₁ i j) →
      E.Y k ≅
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) i) (i₂ := (s₀ : (a : E.I₀) → F.I₀) j)
          ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
w₁₁ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₁ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₁ k ≫ (h₀ i).hom
w₁₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₂ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ Eq (α :=
    E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀))
      ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j : F.I₀)))
    ((congrIndexOneOfEq ⋯ ⋯ :
          (a : E.I₁ i j) →
            E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))
              ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
        k :
      E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀))
        ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j : F.I₀)))
    ((Equiv.symm s₁ :
          (a :
              F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)))
                ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))) →
            E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))
              ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
        ((congrIndexOneOfEq ⋯ ⋯ :
            (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) →
              F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)))
                ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j))))
          ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)) :
      E.I₁ ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀))
        ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j : F.I₀)))

Tactic:
apply PreOneHypercover.congrIndexOneOfEq_equiv

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEq_equiv
-- 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.284030, v, u} S_1
S : C
E F : PreOneHypercover.{u_2, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)
h₁ :
  ⦃i j : E.I₀⦄ →
    (k : E.I₁ i j) →
      E.Y k ≅
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) i) (i₂ := (s₀ : (a : E.I₀) → F.I₀) j)
          ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
w₁₁ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₁ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₁ k ≫ (h₀ i).hom
w₁₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₂ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₂ k ≫ (h₀ j).hom
x : E.I₀
⊢ PreZeroHypercover.Hom.s₀
      (Hom.toHom
        (CategoryStruct.comp (Y := F)
          (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
          { toHom := __Hom,
            s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
              (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
            h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ })
          (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
          { toHom := __Hom,
            s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
              (Equiv.symm s₁ :
                  (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                    E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                ((congrIndexOneOfEq ⋯ ⋯ :
                    (a : F.I₁ i j) →
                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                  k),
            h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
              (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                eqToHom ⋯ ≫
                  Iso.inv
                    (h₁
                      ((Equiv.symm s₁ :
                          (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                            E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                        ((congrIndexOneOfEq ⋯ ⋯ :
                            (a : F.I₁ i j) →
                              F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                          k))),
            w₁₁ := ⋯, w₁₂ := ⋯ })))
      x =
    (Hom.toHom (𝟙 E)).s₀ x

Tactic:
simp
-- 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.284030, v, u} S_1
S : C
E F : PreOneHypercover.{u_2, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)
h₁ :
  ⦃i j : E.I₀⦄ →
    (k : E.I₁ i j) →
      E.Y k ≅
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) i) (i₂ := (s₀ : (a : E.I₀) → F.I₀) j)
          ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
w₁₁ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₁ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₁ k ≫ (h₀ i).hom
w₁₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₂ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₂ k ≫ (h₀ j).hom
x : F.I₀
⊢ PreZeroHypercover.Hom.s₀
      (Hom.toHom
        (CategoryStruct.comp (Y := E)
          (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
          { toHom := __Hom,
            s₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
              (Equiv.symm s₁ :
                  (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                    E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                ((congrIndexOneOfEq ⋯ ⋯ :
                    (a : F.I₁ i j) →
                      F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                  k),
            h₁ := fun {i j : F.I₀} (k : F.I₁ i j) ↦
              (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
                eqToHom ⋯ ≫
                  Iso.inv
                    (h₁
                      ((Equiv.symm s₁ :
                          (a : F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j))) →
                            E.I₁ (__Hom.s₀ i) (__Hom.s₀ j))
                        ((congrIndexOneOfEq ⋯ ⋯ :
                            (a : F.I₁ i j) →
                              F.I₁ ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)) ((s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ j)))
                          k))),
            w₁₁ := ⋯, w₁₂ := ⋯ })
          (let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
          { toHom := __Hom,
            s₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦
              (s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k,
            h₁ := fun {i j : E.I₀} (k : E.I₁ i j) ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ })))
      x =
    (Hom.toHom (𝟙 F)).s₀ x

Tactic:
simp
-- 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.284030, v, u} S_1
S : C
E F : PreOneHypercover.{u_2, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)
h₁ :
  ⦃i j : E.I₀⦄ →
    (k : E.I₁ i j) →
      E.Y k ≅
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) i) (i₂ := (s₀ : (a : E.I₀) → F.I₀) j)
          ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
w₁₁ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₁ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₁ k ≫ (h₀ i).hom
w₁₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₂ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₂ k ≫ (h₀ j).hom
i j : F.I₀
k : F.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ =
    𝟙 (F.Y k) ≫
      CategoryStruct.comp (Y :=
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i : E.I₀)) (i₂ :=
          (s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j : E.I₀))
          ((congrIndexOneOfEq ⋯ ⋯ :
              (a : F.I₁ i j) →
                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i))
                  ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j)))
            k))
        (Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ k)) (eqToHom ⋯)

Tactic:
(Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- 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.284030, v, u} S_1
S : C
E F : PreOneHypercover.{u_2, v, u} S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X ((s₀ : (a : E.I₀) → F.I₀) i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)
h₁ :
  ⦃i j : E.I₀⦄ →
    (k : E.I₁ i j) →
      E.Y k ≅
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) i) (i₂ := (s₀ : (a : E.I₀) → F.I₀) j)
          ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f ((s₀ : (a : E.I₀) → F.I₀) i) = E.f i
w₁₁ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₁ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₁ k ≫ (h₀ i).hom
w₁₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (h₁ k).hom ≫ F.p₂ ((s₁ : (a : E.I₁ i j) → F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j)) k) =
      E.p₂ k ≫ (h₀ j).hom
i j : F.I₀
k : F.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ =
    𝟙 (F.Y k) ≫
      CategoryStruct.comp (Y :=
        F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i : E.I₀)) (i₂ :=
          (s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j : E.I₀))
          ((congrIndexOneOfEq ⋯ ⋯ :
              (a : F.I₁ i j) →
                F.I₁ ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) i))
                  ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) j)))
            k))
        (Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ k)) (eqToHom ⋯)

Tactic:
exact (Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ e.inv.s₀ (e.hom.s₀ i) = i

Tactic:
congr($(e.hom_inv_id).s₀ i)

Premises used: congrArg, CategoryTheory.Iso.hom_inv_id, id, CategoryTheory.PreOneHypercover.Hom.toHom, CategoryTheory.PreZeroHypercover.Hom.s₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
⊢ e.hom.s₀ (e.inv.s₀ i) = i

Tactic:
congr($(e.inv_hom_id).s₀ i)

Premises used: CategoryTheory.Iso.inv_hom_id, congrArg, id, CategoryTheory.PreOneHypercover.Hom.toHom, CategoryTheory.PreZeroHypercover.Hom.s₀
-- 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.330949, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ i = e.inv.s₀ (e.hom.s₀ i)

Tactic:
simp
-- 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.330949, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ j = e.inv.s₀ (e.hom.s₀ j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀

Tactic:
obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
hs₀ : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
⊢ ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯

Tactic:
obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
hs₀ : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
hh₀ : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯
⊢ ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : E.I₁ ((𝟙 E).s₀ i) ((𝟙 E).s₀ j)) → E.I₁ ((e.hom ≫ e.inv).s₀ i) ((e.hom ≫ e.inv).s₀ j))
        (Hom.s₁ (𝟙 E) k)

Tactic:
obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
hs₀ : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
hh₀ : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : E.I₁ ((𝟙 E).s₀ i) ((𝟙 E).s₀ j)) → E.I₁ ((e.hom ≫ e.inv).s₀ i) ((e.hom ≫ e.inv).s₀ j))
        (Hom.s₁ (𝟙 E) k)
⊢ ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).h₁ k = Hom.h₁ (𝟙 E) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 E) k)) ≫ eqToHom ⋯

Tactic:
obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
hs₀ : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
hh₀ : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : E.I₁ ((𝟙 E).s₀ i) ((𝟙 E).s₀ j)) → E.I₁ ((e.hom ≫ e.inv).s₀ i) ((e.hom ≫ e.inv).s₀ j))
        (Hom.s₁ (𝟙 E) k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).h₁ k = Hom.h₁ (𝟙 E) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 E) k)) ≫ eqToHom ⋯
⊢ e.inv.s₁ (e.hom.s₁ k) =
    (congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ (e.inv.s₀ (e.hom.s₀ i)) (e.inv.s₀ (e.hom.s₀ j))) k

Tactic:
simpa using hs₁ i j k
-- 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.333035, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ i = e.hom.s₀ (e.inv.s₀ i)

Tactic:
simp
-- 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.333035, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ j = e.hom.s₀ (e.inv.s₀ j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀

Tactic:
obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
hs₀ : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
⊢ ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯

Tactic:
obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
hs₀ : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
hh₀ : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯
⊢ ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) → F.I₁ ((e.inv ≫ e.hom).s₀ i) ((e.inv ≫ e.hom).s₀ j))
        (Hom.s₁ (𝟙 F) k)

Tactic:
obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
hs₀ : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
hh₀ : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) → F.I₁ ((e.inv ≫ e.hom).s₀ i) ((e.inv ≫ e.hom).s₀ j))
        (Hom.s₁ (𝟙 F) k)
⊢ ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).h₁ k = Hom.h₁ (𝟙 F) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 F) k)) ≫ eqToHom ⋯

Tactic:
obtain ⟨hs₀, hh₀, hs₁, hh₁⟩ := PreOneHypercover.Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp