awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact Category.comp_id _

Premises used: CategoryTheory.Category.comp_id
-- 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.269827, 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.269827, 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₀
h : ∀ (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.269827, 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₀
h : ∀ (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.269827, 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₀
h : ∀ (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
⊢ f = g ↔
    ∃ (hs₀ : f.s₀ = g.s₀) (_ : ∀ (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), f.h₁ k = g.h₁ k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)) ≫ eqToHom ⋯

Tactic:
⟨fun h ↦ ?_, fun ⟨hs₀, hh₀, hs₁, hh₁⟩ ↦ Hom.ext' hs₀ hh₀ hs₁ hh₁⟩

Premises used: CategoryTheory.PreOneHypercover.Hom.ext', _private.0.CategoryTheory.PreOneHypercover.Hom.ext'_iff.match_1, Iff.intro, Eq
-- 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
refine :
  ∀ (h : f = g),
    ∃ (hs₀ : f.s₀ = g.s₀) (_ : ∀ (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), f.h₁ k = g.h₁ k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)) ≫ eqToHom ⋯
⊢ f = g ↔
    ∃ (hs₀ : f.s₀ = g.s₀) (_ : ∀ (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), f.h₁ k = g.h₁ k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)) ≫ eqToHom ⋯

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨hs₀, hh₀, hs₁, hh₁⟩ ↦ Hom.ext' hs₀ hh₀ hs₁ hh₁⟩
-- 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
h : f = g
subst :
  ∃ (hs₀ : f.s₀ = f.s₀) (_ : ∀ (i : E.I₀), f.h₀ i = f.h₀ i ≫ eqToHom ⋯) (hs₁ :
    ∀ (i j : E.I₀) (k : E.I₁ i j),
      f.s₁ k = (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (f.s₀ i) (f.s₀ j)) → F.I₁ (f.s₀ i) (f.s₀ j)) (f.s₁ k)),
    ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = f.h₁ k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (f.s₁ k)) ≫ eqToHom ⋯
⊢ ∃ (hs₀ : f.s₀ = g.s₀) (_ : ∀ (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), f.h₁ k = g.h₁ k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)) ≫ eqToHom ⋯

Tactic:
subst h
-- 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 : E.Hom F
⊢ ∃ (hs₀ : f.s₀ = f.s₀) (_ : ∀ (i : E.I₀), f.h₀ i = f.h₀ i ≫ eqToHom ⋯) (hs₁ :
    ∀ (i j : E.I₀) (k : E.I₁ i j),
      f.s₁ k = (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (f.s₀ i) (f.s₀ j)) → F.I₁ (f.s₀ i) (f.s₀ j)) (f.s₁ k)),
    ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = f.h₁ k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (f.s₁ k)) ≫ eqToHom ⋯

Tactic:
simp [congrIndexOneOfEq]

Premises used: 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 : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.274259, v, u} S
s₀ : Equiv.{w + 1, w' + 1} E.I₀ F.I₀
s₁ : ⦃i j : E.I₀⦄ → Equiv.{w + 1, w' + 1} (E.I₁ i j) (F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
i j : E.I₀
k : E.I₁ i j
⊢ Eq.{w' + 1} (α := F.I₀) ((s₀ : (a : E.I₀) → F.I₀) i : F.I₀)
    ((s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)) : F.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 : C
E_1 E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.274259, v, u} S
s₀ : Equiv.{w + 1, w' + 1} E.I₀ F.I₀
s₁ : ⦃i j : E.I₀⦄ → Equiv.{w + 1, w' + 1} (E.I₁ i j) (F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
i j : E.I₀
k : E.I₁ i j
⊢ Eq.{w' + 1} (α := F.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₀) j)) : F.I₀)

Tactic:
simp
-- 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
s₀ : Equiv.{w + 1, w' + 1} E.I₀ F.I₀
s₁ : ⦃i j : E.I₀⦄ → Equiv.{w + 1, w' + 1} (E.I₁ i j) (F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
i j : E.I₀
k : E.I₁ i j
⊢ Eq.{w' + 1} (α :=
    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₁ ((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))) →
            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))))
        ((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) :
      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₁ ((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))) →
            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))))
        ((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))) :
      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))))

Tactic:
simp [PreOneHypercover.congrIndexOneOfEq_naturality (u₁ := fun i j k ↦ s₁ k)]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEq_naturality, DFunLike.coe
-- 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 : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.277334, v, u} S
s₀ : Equiv.{w + 1, w' + 1} E.I₀ F.I₀
s₁ : ⦃i j : E.I₀⦄ → Equiv.{w + 1, w' + 1} (E.I₁ i j) (F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
i j : E.I₀
k_1 : E.I₁ 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)
k : E.I₁ i j
⊢ F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i))) (i₂ :=
      (s₀ : (a : E.I₀) → F.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)) =
    F.Y (i₁ := (s₀ : (a : E.I₀) → F.I₀) ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) 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₁ ((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))) →
            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))))
        ((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))))

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 : C
E_1 E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.277334, v, u} S
s₀ : Equiv.{w + 1, w' + 1} E.I₀ F.I₀
s₁ : ⦃i j : E.I₀⦄ → Equiv.{w + 1, w' + 1} (E.I₁ i j) (F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
i j : E.I₀
k_1 : E.I₁ 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)
k : E.I₁ i j
⊢ Eq (α :=
    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 : 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))
        ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
    ((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))
        ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))

Tactic:
apply E.congrIndexOneOfEq_equiv s₀ s₁ _

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEq_equiv
-- 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
s₀ : Equiv.{w + 1, w' + 1} E.I₀ F.I₀
s₁ : ⦃i j : E.I₀⦄ → Equiv.{w + 1, w' + 1} (E.I₁ i j) (F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
i j : E.I₀
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)
k : E.I₁ i j
⊢ i = (s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) i)

Tactic:
simp
-- 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
s₀ : Equiv.{w + 1, w' + 1} E.I₀ F.I₀
s₁ : ⦃i j : E.I₀⦄ → Equiv.{w + 1, w' + 1} (E.I₁ i j) (F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
i j : E.I₀
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)
k : E.I₁ i j
⊢ j = (s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)

Tactic:
simp
-- 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
s₀ : Equiv.{w + 1, w' + 1} E.I₀ F.I₀
s₁ : ⦃i j : E.I₀⦄ → Equiv.{w + 1, w' + 1} (E.I₁ i j) (F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
i j : E.I₀
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)
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
      eqToHom ⋯ ≫
        Iso.hom
            (h₁
              ((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)))) ≫
          Iso.inv
            (h₁
              ((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)))) =
    (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
simp
-- 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
s₀ : Equiv.{w + 1, w' + 1} E.I₀ F.I₀
s₁ : ⦃i j : E.I₀⦄ → Equiv.{w + 1, w' + 1} (E.I₁ i j) (F.I₁ ((s₀ : (a : E.I₀) → F.I₀) i) ((s₀ : (a : E.I₀) → F.I₀) j))
i j : E.I₀
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)
k : E.I₁ i j
⊢ Eq (α :=
    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 : 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))
        ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))
    ((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))
        ((s₀.symm : (a : F.I₀) → E.I₀) ((s₀ : (a : E.I₀) → F.I₀) j)))

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
i j : F.I₀
k : F.I₁ i j
⊢ i = (s₀ : (a : E.I₀) → F.I₀) (__Hom.s₀ i)

Tactic:
simp