awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
zero :
  Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piOpens F U)
    (Pi.lift fun (i : ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (single i))) :
      F.obj (op (iSup U)) ⟶ piObj.{v', v, u} fun (i : ι) ↦ F.obj (op (U i)))
    (SheafConditionEqualizerProducts.res F U : F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piOpens F U)
⊢ Eq.{v + 1} (α :=
    Cone.pt (F :=
        parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
          (SheafConditionEqualizerProducts.rightRes F U))
        (SheafConditionEqualizerProducts.fork F U) ⟶
      (parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U)).obj
        WalkingParallelPair.zero)
    (𝟙
        (Cone.pt (F :=
          parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U))
          (SheafConditionEqualizerProducts.fork F U)) ≫
      NatTrans.app
        (Cone.π (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))))
        WalkingParallelPair.zero)
    (NatTrans.app (Cone.π (SheafConditionEqualizerProducts.fork F U)) WalkingParallelPair.zero)

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
⊢ Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piOpens F U)
    (Pi.lift fun (i : ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (single i))) :
      F.obj (op (iSup U)) ⟶ piObj.{v', v, u} fun (i : ι) ↦ F.obj (op (U i)))
    (SheafConditionEqualizerProducts.res F U : F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piOpens F U)

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
one :
  Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 (F.obj (op (iSup U))) ≫ Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))) :
      F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piInters F U)
    (SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U :
      F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piInters F U)
⊢ Eq.{v + 1} (α :=
    Cone.pt (F :=
        parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
          (SheafConditionEqualizerProducts.rightRes F U))
        (SheafConditionEqualizerProducts.fork F U) ⟶
      (parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U)).obj
        WalkingParallelPair.one)
    (𝟙
        (Cone.pt (F :=
          parallelPair (X := SheafConditionEqualizerProducts.piOpens F U) (SheafConditionEqualizerProducts.leftRes F U)
            (SheafConditionEqualizerProducts.rightRes F U))
          (SheafConditionEqualizerProducts.fork F U)) ≫
      NatTrans.app
        (Cone.π (Functor.obj (Equivalence.functor (coneEquiv F U)) (Functor.mapCone F (Cocone.op (cocone U)))))
        WalkingParallelPair.one)
    (NatTrans.app (Cone.π (SheafConditionEqualizerProducts.fork F U)) WalkingParallelPair.one)

Tactic:
dsimp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
one :
  ∀ (j : Discrete (ι × ι)),
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 (F.obj (op (iSup U))) ≫
          Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) =
      CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U)
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)
⊢ Eq (α := F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piInters F U)
    (𝟙 (F.obj (op (iSup U))) ≫ Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))) :
      F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piInters F U)
    (SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U :
      F.obj (op (iSup U)) ⟶ SheafConditionEqualizerProducts.piInters F U)

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
one :
  Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 (F.obj (op (iSup U))) ≫
          Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
          (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
          (Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
⊢ CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (𝟙 (F.obj (op (iSup U))) ≫ Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) =
    CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
      (SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U)
      (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j)

Tactic:
dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                SheafConditionEqualizerProducts.leftRes]

Premises used: TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse, TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes, TopCat.Presheaf.SheafConditionEqualizerProducts.res
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
one :
  Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair j.as.1 j.as.2))) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (F.map (Quiver.Hom.op (leSupr U j.as.1)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))) :
      Cone.pt.{v', v, v', u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ F.obj (op (U i)))
          (Fan.mk (F.obj (op (iSup U))) fun (i : ι) ↦ F.map (leSupr U i).op) ⟶
        F.obj (op (U j.as.1 ⊓ U j.as.2)))
⊢ Eq.{v + 1} (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (𝟙 (F.obj (op (iSup U))) ≫
          Pi.lift fun (b : ι × ι) ↦ F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair b.1 b.2))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piInters F U)
        (CategoryStruct.comp (Y := SheafConditionEqualizerProducts.piOpens F U)
          (Pi.lift fun (i : ι) ↦ F.map (leSupr U i).op)
          (Pi.lift fun (p : ι × ι) ↦
            Pi.π (fun (i : ι) ↦ F.obj (op (U i))) p.1 ≫ F.map (Quiver.Hom.op ((U p.1).infLELeft (U p.2)))))
        (limit.π (Discrete.functor fun (p : ι × ι) ↦ F.obj (op (U p.1 ⊓ U p.2))) j) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))

Tactic:
simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
one :
  Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair j.as.1 j.as.2))) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (F.map (Quiver.Hom.op (leSupr U j.as.1) ≫ Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
⊢ Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair j.as.1 j.as.2))) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (F.map (Quiver.Hom.op (leSupr U j.as.1)) ≫ F.map (Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))) :
      Cone.pt.{v', v, v', u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ F.obj (op (U i)))
          (Fan.mk (F.obj (op (iSup U))) fun (i : ι) ↦ F.map (leSupr U i).op) ⟶
        F.obj (op (U j.as.1 ⊓ U j.as.2)))

Tactic:
rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
ι : Type v'
U : ι → Opens (↑X : Type v')
Q : IsLimit (Functor.mapCone F (Cocone.op (cocone U)))
j : Discrete (ι × ι)
⊢ Eq (α := F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (F.map (Quiver.Hom.op (coconeιApp U (Pairwise.pair j.as.1 j.as.2))) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))
    (F.map (Quiver.Hom.op (leSupr U j.as.1) ≫ Quiver.Hom.op ((U j.as.1).infLELeft (U j.as.2))) :
      F.obj (op (iSup U)) ⟶ F.obj (op (U j.as.1 ⊓ U j.as.2)))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v', v, u} C
X : TopCat
F : Presheaf.{v', v, u} C X
⊢ F.IsSheaf ↔ F.IsSheafEqualizerProducts

Tactic:
(isSheaf_iff_isSheafPairwiseIntersections F).trans <|
    Iff.intro (fun h _ U => ⟨isLimitSheafConditionForkOfIsLimitMapCone F U (h U).some⟩) fun h _ U =>
      ⟨isLimitMapConeOfIsLimitSheafConditionFork F U (h U).some⟩

Premises used: TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections, TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitMapConeOfIsLimitSheafConditionFork, Nonempty.some, Nonempty.intro, Iff.intro, Iff.trans, TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitSheafConditionForkOfIsLimitMapCone
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀
    (X_1 :
      ObjectProperty.FullSubcategory (C := Over Y) fun (f : Over Y) ↦
        (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom),
    Functor.obj
        (𝟭
          (ObjectProperty.FullSubcategory (C := Over Y) fun (f : Over Y) ↦
            (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom))
        X_1 =
      Functor.obj (generateEquivalenceOpensLe_functor' U ⋙ generateEquivalenceOpensLe_inverse' U hY) X_1
⊢ ∀
    (X_1 :
      ObjectProperty.FullSubcategory (C := Over Y) fun (f : Over Y) ↦
        (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom),
    Functor.obj
        (𝟭
          (ObjectProperty.FullSubcategory (C := Over Y) fun (f : Over Y) ↦
            (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom))
        X_1 =
      Functor.obj (generateEquivalenceOpensLe_functor' U ⋙ generateEquivalenceOpensLe_inverse' U hY) X_1

Tactic:
cat_disch
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (X_1 : OpensLeCover U),
    (generateEquivalenceOpensLe_inverse' U hY ⋙ generateEquivalenceOpensLe_functor' U).obj X_1 =
      Functor.obj (𝟭 (OpensLeCover U)) X_1
⊢ ∀ (X_1 : OpensLeCover U),
    (generateEquivalenceOpensLe_inverse' U hY ⋙ generateEquivalenceOpensLe_functor' U).obj X_1 =
      Functor.obj (𝟭 (OpensLeCover U)) X_1

Tactic:
cat_disch
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
j :
  (ObjectProperty.FullSubcategory (C := Over Y) fun (f : Over Y) ↦
      (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
dsimp :
  F.map (eqToHom ⋯) ≫
      F.map
        (unop j).obj (P := fun (f : Over Y) ↦
              ∃ (Y_1 : Opens (↑X : Type w)) (h : f.left ⟶ Y_1) (g : Y_1 ⟶ Y),
                presieveOfCoveringAux U Y g ∧ h ≫ g = f.hom).hom.op =
    F.map (Quiver.Hom.op ((opensLeCoverCocone U).ι.app (Functor.obj (generateEquivalenceOpensLe_functor' U) (unop j))))
⊢ F.map (eqToHom ⋯) ≫ (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op).π.app j =
    (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op)).π.app j

Tactic:
dsimp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
j :
  (ObjectProperty.FullSubcategory (C := Over Y) fun (f : Over Y) ↦
      (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
rw :
  F.map
      (eqToHom ⋯ ≫
        (unop j).obj (P := fun (f : Over Y) ↦
              ∃ (Y_1 : Opens (↑X : Type w)) (h : f.left ⟶ Y_1) (g : Y_1 ⟶ Y),
                presieveOfCoveringAux U Y g ∧ h ≫ g = f.hom).hom.op) =
    F.map (Quiver.Hom.op ((opensLeCoverCocone U).ι.app (Functor.obj (generateEquivalenceOpensLe_functor' U) (unop j))))
⊢ F.map (eqToHom ⋯) ≫
      F.map
        (unop j).obj (P := fun (f : Over Y) ↦
              ∃ (Y_1 : Opens (↑X : Type w)) (h : f.left ⟶ Y_1) (g : Y_1 ⟶ Y),
                presieveOfCoveringAux U Y g ∧ h ≫ g = f.hom).hom.op =
    F.map (Quiver.Hom.op ((opensLeCoverCocone U).ι.app (Functor.obj (generateEquivalenceOpensLe_functor' U) (unop j))))

Tactic:
rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
j :
  (ObjectProperty.FullSubcategory (C := Over Y) fun (f : Over Y) ↦
      (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
      (eqToHom ⋯ ≫
        (unop j).obj (P := fun (f : Over Y) ↦
              ∃ (Y_1 : Opens (↑X : Type w)) (h : f.left ⟶ Y_1) (g : Y_1 ⟶ Y),
                presieveOfCoveringAux U Y g ∧ h ≫ g = f.hom).hom.op) =
    F.map (Quiver.Hom.op ((opensLeCoverCocone U).ι.app (Functor.obj (generateEquivalenceOpensLe_functor' U) (unop j))))

Tactic:
congr 1
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
j :
  (ObjectProperty.FullSubcategory (C := Over Y) fun (f : Over Y) ↦
      (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
dsimp :
  F.map (eqToHom ⋯) ≫
      F.map
        (Quiver.Hom.op ((opensLeCoverCocone U).ι.app (Functor.obj (generateEquivalenceOpensLe_functor' U) (unop j)))) =
    F.map
      (unop j).obj (P := fun (f : Over Y) ↦
            ∃ (Y_1 : Opens (↑X : Type w)) (h : f.left ⟶ Y_1) (g : Y_1 ⟶ Y),
              presieveOfCoveringAux U Y g ∧ h ≫ g = f.hom).hom.op
⊢ F.map (eqToHom ⋯) ≫
      (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op)).π.app
        j =
    (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op).π.app j

Tactic:
dsimp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
j :
  (ObjectProperty.FullSubcategory (C := Over Y) fun (f : Over Y) ↦
      (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
rw :
  F.map
      (eqToHom ⋯ ≫
        Quiver.Hom.op ((opensLeCoverCocone U).ι.app (Functor.obj (generateEquivalenceOpensLe_functor' U) (unop j)))) =
    F.map
      (unop j).obj (P := fun (f : Over Y) ↦
            ∃ (Y_1 : Opens (↑X : Type w)) (h : f.left ⟶ Y_1) (g : Y_1 ⟶ Y),
              presieveOfCoveringAux U Y g ∧ h ≫ g = f.hom).hom.op
⊢ F.map (eqToHom ⋯) ≫
      F.map
        (Quiver.Hom.op ((opensLeCoverCocone U).ι.app (Functor.obj (generateEquivalenceOpensLe_functor' U) (unop j)))) =
    F.map
      (unop j).obj (P := fun (f : Over Y) ↦
            ∃ (Y_1 : Opens (↑X : Type w)) (h : f.left ⟶ Y_1) (g : Y_1 ⟶ Y),
              presieveOfCoveringAux U Y g ∧ h ≫ g = f.hom).hom.op

Tactic:
rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
j :
  (ObjectProperty.FullSubcategory (C := Over Y) fun (f : Over Y) ↦
      (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map
      (eqToHom ⋯ ≫
        Quiver.Hom.op ((opensLeCoverCocone U).ι.app (Functor.obj (generateEquivalenceOpensLe_functor' U) (unop j)))) =
    F.map
      (unop j).obj (P := fun (f : Over Y) ↦
            ∃ (Y_1 : Opens (↑X : Type w)) (h : f.left ⟶ Y_1) (g : Y_1 ⟶ Y),
              presieveOfCoveringAux U Y g ∧ h ≫ g = f.hom).hom.op

Tactic:
congr 1
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
w :
  ConeMorphism.hom
      (CategoryStruct.comp (Y := Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op)
        { hom := F.map (eqToHom ⋯), w := ⋯ } { hom := F.map (eqToHom ⋯), w := ⋯ }) =
    ConeMorphism.hom
      (𝟙 (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op)))
⊢ CategoryStruct.comp (Y := Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op)
      { hom := F.map (eqToHom ⋯), w := ⋯ } { hom := F.map (eqToHom ⋯), w := ⋯ } =
    𝟙 (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op))

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
⊢ ConeMorphism.hom
      (CategoryStruct.comp (Y := Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op)
        { hom := F.map (eqToHom ⋯), w := ⋯ } { hom := F.map (eqToHom ⋯), w := ⋯ }) =
    ConeMorphism.hom
      (𝟙 (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op)))

Tactic:
simp [eqToHom_map]

Premises used: CategoryTheory.eqToHom_map
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
w :
  ConeMorphism.hom
      (CategoryStruct.comp (Y :=
        Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op))
        { hom := F.map (eqToHom ⋯), w := ⋯ } { hom := F.map (eqToHom ⋯), w := ⋯ }) =
    ConeMorphism.hom (𝟙 (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op))
⊢ CategoryStruct.comp (Y :=
      Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op))
      { hom := F.map (eqToHom ⋯), w := ⋯ } { hom := F.map (eqToHom ⋯), w := ⋯ } =
    𝟙 (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op)

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
hY : Y = iSup U
⊢ ConeMorphism.hom
      (CategoryStruct.comp (Y :=
        Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op))
        { hom := F.map (eqToHom ⋯), w := ⋯ } { hom := F.map (eqToHom ⋯), w := ⋯ }) =
    ConeMorphism.hom (𝟙 (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op))

Tactic:
simp [eqToHom_map]

Premises used: CategoryTheory.eqToHom_map
-- Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Presheaf.{w, v_1, u_1} C X
ι : Type u_2
U : ι → Opens (↑X : Type w)
Y : Opens (↑X : Type w)
R : Presieve Y
hR : Sieve.generate R ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) Y
h :
  IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op) =
    IsLimit (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux (coveringOfPresieve Y R) Y)).arrows.cocone.op)
⊢ IsLimit (Functor.mapCone F (opensLeCoverCocone (coveringOfPresieve Y R)).op) ≃
    IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op)

Tactic:
convert!
    isLimitOpensLeEquivGenerate₁ F (coveringOfPresieve Y R)
      (coveringOfPresieve.iSup_eq_of_mem_grothendieck Y R hR).symm using 1

Premises used: TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck, TopCat.Presheaf.coveringOfPresieve, TopCat.Presheaf.isLimitOpensLeEquivGenerate₁, Eq.symm