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 : PreZeroHypercover.{u_2, v, u} S
inst_1 : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
h : Sieve.arrows ⊤ f
⊢ 𝟙 (pullback (E.f i) (E.f j)) ≫ pullback.snd (E.f i) (E.f j) =
    CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (eqToHom ⋯ ≫ E.toPreOneHypercover.toPullback PUnit.unit)
      (pullback.snd (E.f i) (E.f j))

Tactic:
simp [PreOneHypercover.toPullback]

Premises used: CategoryTheory.PreOneHypercover.toPullback
-- 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
J : Precoverage.{v, u} C
S : C
E : ZeroHypercover.{u_2, v, u} J S
inst_2 : E.HasPullbacks
⊢ ∀ (i₁ i₂ : E.toPreOneHypercover.I₀),
    Membership.mem (γ := Set (Sieve.{v, u} (pullback (E.toPreOneHypercover.f i₁) (E.toPreOneHypercover.f i₂))))
      ((J.toGrothendieck : (a : C) → Set (Sieve a)) (pullback (E.toPreOneHypercover.f i₁) (E.toPreOneHypercover.f i₂)))
      (E.toPreOneHypercover.sieve₁' i₁ 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
X : C
E : PreZeroHypercover.{w, v, u} X
inst_2 : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover.{w, v, u} (pullback (E.f i) (E.f j))
i j : E.I₀
k : (F i j).I₀
⊢ ((F i j).f k ≫ pullback.fst (E.f i) (E.f j)) ≫ E.f i = ((F i j).f k ≫ pullback.snd (E.f i) (E.f j)) ≫ E.f j

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
X : C
E : PreZeroHypercover.{w, v, u} X
inst_1 : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover.{w, v, u} (pullback (E.f i) (E.f j))
i j : E.I₀
e_f : (fun (j_1 : (E.refineOneHypercover F).I₁ i j) ↦ (E.refineOneHypercover F).toPullback j_1) = (F i j).f
⊢ (Sieve.ofArrows (E.refineOneHypercover F).Y fun (j_1 : (E.refineOneHypercover F).I₁ i j) ↦
      (E.refineOneHypercover F).toPullback j_1) =
    sieve₀.{w, v, u} (F i j)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
X : C
E : PreZeroHypercover.{w, v, u} X
inst_1 : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover.{w, v, u} (pullback (E.f i) (E.f j))
i j : E.I₀
e_f :
  ∀ (x : (E.refineOneHypercover F).I₁ i j),
    CategoryStruct.comp (Y := pullback ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j))
        ((E.refineOneHypercover F).toPullback x)
        (pullback.fst ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)) =
      (F i j).f x ≫ pullback.fst ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)
e_f₁ :
  ∀ (x : (E.refineOneHypercover F).I₁ i j),
    CategoryStruct.comp (Y := pullback ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j))
        ((E.refineOneHypercover F).toPullback x)
        (pullback.snd ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)) =
      (F i j).f x ≫ pullback.snd ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)
⊢ (fun (j_1 : (E.refineOneHypercover F).I₁ i j) ↦ (E.refineOneHypercover F).toPullback j_1) = (F i j).f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
X : C
E : PreZeroHypercover.{w, v, u} X
inst_1 : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover.{w, v, u} (pullback (E.f i) (E.f j))
i j : E.I₀
x : (E.refineOneHypercover F).I₁ i j
⊢ CategoryStruct.comp (Y := pullback ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j))
      ((E.refineOneHypercover F).toPullback x)
      (pullback.fst ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)) =
    (F i j).f x ≫ pullback.fst ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)

Tactic:
simp [PreOneHypercover.toPullback]

Premises used: CategoryTheory.PreOneHypercover.toPullback
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
X : C
E : PreZeroHypercover.{w, v, u} X
inst_1 : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover.{w, v, u} (pullback (E.f i) (E.f j))
i j : E.I₀
x : (E.refineOneHypercover F).I₁ i j
⊢ CategoryStruct.comp (Y := pullback ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j))
      ((E.refineOneHypercover F).toPullback x)
      (pullback.snd ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)) =
    (F i j).f x ≫ pullback.snd ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)

Tactic:
simp [PreOneHypercover.toPullback]

Premises used: CategoryTheory.PreOneHypercover.toPullback
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
F : Functor.{v_1, u_3, u_1, u_3 + 1} Cᵒᵖ (Type u_3)
rw :
  Function.Bijective (E.saturate.multifork F).toSections ↔
    Function.Bijective (β := (E.saturate.multicospanIndex F).sections)
      ((⇑(E.sectionsSaturateEquiv F).symm :
          (a : Subtype (Presieve.Arrows.Compatible F E.f)) → (E.saturate.multicospanIndex F).sections) ∘
        Presieve.Arrows.toCompatible F E.f)
⊢ Nonempty (IsLimit (E.saturate.multifork F)) ↔ Presieve.IsSheafFor F E.presieve₀

Tactic:
rw [Multifork.isLimit_types_iff, Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← Function.Bijective.of_comp_iff' (E.sectionsSaturateEquiv F).symm.bijective]

Premises used: Equiv.bijective, CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv, Function.Bijective.of_comp_iff', Equiv.symm, CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible, CategoryTheory.Limits.Multifork.isLimit_types_iff
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
F : Functor.{v_1, u_3, u_1, u_3 + 1} Cᵒᵖ (Type u_3)
⊢ Function.Bijective (E.saturate.multifork F).toSections ↔
    Function.Bijective (β := (E.saturate.multicospanIndex F).sections)
      ((⇑(E.sectionsSaturateEquiv F).symm :
          (a : Subtype (Presieve.Arrows.Compatible F E.f)) → (E.saturate.multicospanIndex F).sections) ∘
        Presieve.Arrows.toCompatible F E.f)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
S_1 : C
E_1 : PreZeroHypercover.{?u.11235, v_1, u_1} S_1
inst_2 : E_1.HasPullbacks
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_3 : E.HasPullbacks
⊢ ∀ (i : E.toPreOneHypercover.I₀),
    pullback.diagonal (E.f i) ≫ E.toPreOneHypercover.p₁ PUnit.unit = (PreOneHypercover.Hom.id E.toPreOneHypercover).h₀ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
S_1 : C
E_1 : PreZeroHypercover.{?u.11235, v_1, u_1} S_1
inst_2 : E_1.HasPullbacks
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_3 : E.HasPullbacks
⊢ ∀ (i : E.toPreOneHypercover.I₀),
    pullback.diagonal (E.f i) ≫ E.toPreOneHypercover.p₂ PUnit.unit = (PreOneHypercover.Hom.id E.toPreOneHypercover).h₀ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst_1 : E.HasPullbacks
⊢ ∀ (i : E.toPreOneHypercover.I₀),
    Hom.h₀
        (PreOneHypercover.Hom.toHom (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks))
        i =
      (PreOneHypercover.Hom.id E.toPreOneHypercover).h₀ i ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst_1 : E.HasPullbacks
⊢ ∀ (i j : E.toPreOneHypercover.I₀) (k : E.toPreOneHypercover.I₁ i j),
    Eq (α :=
      E.toPreOneHypercover.I₁
        (Hom.s₀
          (PreOneHypercover.Hom.toHom
            (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks))
          i)
        (Hom.s₀
          (PreOneHypercover.Hom.toHom
            (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks))
          j))
      (PreOneHypercover.Hom.s₁ (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks) k)
      ((PreOneHypercover.congrIndexOneOfEq ⋯ ⋯ :
          (a :
              E.toPreOneHypercover.I₁ ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₀ i)
                ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₀ j)) →
            E.toPreOneHypercover.I₁
              ((PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks).s₀ i)
              ((PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks).s₀ j))
        ((PreOneHypercover.Hom.id E.toPreOneHypercover).s₁ k))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst_1 : E.HasPullbacks
⊢ PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks =
    PreOneHypercover.Hom.id E.toPreOneHypercover

Tactic:
refine PreOneHypercover.Hom.ext' rfl (by simp) (by simp) (by simp)

Premises used: CategoryTheory.PreOneHypercover.Hom.ext', rfl
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
S_1 : C
E_1 : PreZeroHypercover.{?u.16302, v_1, u_1} S_1
inst_2 : E_1.HasPullbacks
S : C
E : PreZeroHypercover S
inst_3 : E.HasPullbacks
i : E.saturate.I₀
⊢ pullback.diagonal (E.f i) ≫
      E.saturate.p₁
        { obj := pullback (E.f i) (E.f i), fst := pullback.fst (E.f i) (E.f i), snd := pullback.snd (E.f i) (E.f i),
          w := ⋯ :
          E.Relation
            ((PreOneHypercover.Hom.comp (F := E.toPreOneHypercover) E.fromSaturateOfHasPullbacks
                  E.toSaturateOfHasPullbacks).s₀
              i)
            ((PreOneHypercover.Hom.id E.saturate).s₀ i) } =
    (PreOneHypercover.Hom.comp (F := E.toPreOneHypercover) E.fromSaturateOfHasPullbacks E.toSaturateOfHasPullbacks).h₀ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
S_1 : C
E_1 : PreZeroHypercover.{?u.16302, v_1, u_1} S_1
inst_2 : E_1.HasPullbacks
S : C
E : PreZeroHypercover S
inst_3 : E.HasPullbacks
i : E.saturate.I₀
⊢ pullback.diagonal (E.f i) ≫
      E.saturate.p₂
        { obj := pullback (E.f i) (E.f i), fst := pullback.fst (E.f i) (E.f i), snd := pullback.snd (E.f i) (E.f i),
          w := ⋯ :
          E.Relation
            ((PreOneHypercover.Hom.comp (F := E.toPreOneHypercover) E.fromSaturateOfHasPullbacks
                  E.toSaturateOfHasPullbacks).s₀
              i)
            ((PreOneHypercover.Hom.id E.saturate).s₀ i) } =
    (PreOneHypercover.Hom.id E.saturate).h₀ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
S_1 : C
E_1 : PreZeroHypercover.{?u.18915, v_1, u_1} S_1
inst_2 : E_1.HasPullbacks
S_2 : C
E_2 : PreZeroHypercover.{?u.19098, v_1, u_1} S_2
inst_3 : E_2.HasPullbacks
S : C
E : PreZeroHypercover S
inst_4 : E.HasPullbacks
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
rw :
  PreOneHypercover.Homotopy (PreOneHypercover.Hom.id E.toPreOneHypercover)
    (PreOneHypercover.Hom.id E.toPreOneHypercover)
⊢ PreOneHypercover.Homotopy (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks)
    (PreOneHypercover.Hom.id E.toPreOneHypercover)

Tactic:
rw [toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks]

Premises used: CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : Category.{v_2, u_2} A
S_1 : C
E_1 : PreZeroHypercover.{?u.18915, v_1, u_1} S_1
inst_2 : E_1.HasPullbacks
S_2 : C
E_2 : PreZeroHypercover.{?u.19098, v_1, u_1} S_2
inst_3 : E_2.HasPullbacks
S : C
E : PreZeroHypercover S
inst_4 : E.HasPullbacks
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ A
⊢ PreOneHypercover.Homotopy (PreOneHypercover.Hom.id E.toPreOneHypercover)
    (PreOneHypercover.Hom.id E.toPreOneHypercover)

Tactic:
exact E.toPreOneHypercoverHomotopy

Premises used: CategoryTheory.PreZeroHypercover.toPreOneHypercoverHomotopy
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
⊢ Eq (α :=
    (fun (X : Type u_2) ↦ X)
      ((E.toPreOneHypercover.multicospanIndex F).right
        (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2)
          (i, j) PUnit.unit)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((E.toPreOneHypercover.multicospanIndex F).fst
              (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦
                E.toPreOneHypercover.I₁ i.1 i.2) (i, j) PUnit.unit)) :
          (a :
              (fun (X : Type u_2) ↦ X)
                ((E.toPreOneHypercover.multicospanIndex F).left
                  (E.toPreOneHypercover.multicospanShape.fst ⟨(i, j), PUnit.unit⟩))) →
            (fun (X : Type u_2) ↦ X) ((E.toPreOneHypercover.multicospanIndex F).right ⟨(i, j), PUnit.unit⟩))
        (s.val
          (E.toPreOneHypercover.multicospanShape.fst
            (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦
              E.toPreOneHypercover.I₁ i.1 i.2) (i, j) PUnit.unit))) :
      (fun (X : Type u_2) ↦ X)
        ((E.toPreOneHypercover.multicospanIndex F).right
          (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2)
            (i, j) PUnit.unit)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((E.toPreOneHypercover.multicospanIndex F).snd
              (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦
                E.toPreOneHypercover.I₁ i.1 i.2) (i, j) PUnit.unit)) :
          (a :
              (fun (X : Type u_2) ↦ X)
                ((E.toPreOneHypercover.multicospanIndex F).left
                  (E.toPreOneHypercover.multicospanShape.snd ⟨(i, j), PUnit.unit⟩))) →
            (fun (X : Type u_2) ↦ X) ((E.toPreOneHypercover.multicospanIndex F).right ⟨(i, j), PUnit.unit⟩))
        (s.val
          (E.toPreOneHypercover.multicospanShape.snd
            (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦
              E.toPreOneHypercover.I₁ i.1 i.2) (i, j) PUnit.unit))) :
      (fun (X : Type u_2) ↦ X)
        ((E.toPreOneHypercover.multicospanIndex F).right
          (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2)
            (i, j) PUnit.unit)))

Tactic:
have heq := s.property ⟨(i, j), ⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  Eq (α := F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.fst (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X i))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val i) :
      F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.snd (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X j))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val j) :
      F.obj (op (pullback (E.f i) (E.f j))))
rw :
  Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                  (pullback.fst (E.f i) (E.f j))).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gj.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gi.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gj.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))

Tactic:
rw [← pullback.lift_fst _ _ hgij]

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  Eq (α := F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.fst (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X i))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val i) :
      F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.snd (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X j))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val j) :
      F.obj (op (pullback (E.f i) (E.f j))))
rw :
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                (pullback.snd (E.f i) (E.f j))).op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
      (s.val j) :
    (fun (X : Type u_2) ↦ X) (F.obj (op W)))
| ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gj.op) :
        (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
      (s.val j) :
    (fun (X : Type u_2) ↦ X) (F.obj (op W)))

Tactic:
rw [← pullback.lift_snd _ _ hgij]

Premises used: CategoryTheory.Limits.pullback.lift_snd
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  Eq (α := F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.fst (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X i))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val i) :
      F.obj (op (pullback (E.f i) (E.f j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.snd (E.f i) (E.f j)))) :
          (a : F.obj (op (E.X j))) → F.obj (op (pullback (E.f i) (E.f j))))
        (s.val j) :
      F.obj (op (pullback (E.f i) (E.f j))))
conv_rhs :
  Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                  (pullback.fst (E.f i) (E.f j))).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                  (pullback.snd (E.f i) (E.f j))).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CategoryStruct.comp (Y := pullback (E.f i) (E.f j)) (pullback.lift gi gj hgij)
                  (pullback.fst (E.f i) (E.f j))).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gj.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))

Tactic:
conv_rhs => rw [← pullback.lift_snd _ _ hgij]

Premises used: CategoryTheory.Limits.pullback.lift_snd