awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : Z ⟶ X
rw : mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map g.op = mapPreimage K G F f ≫ mapPreimage K G F (G.map g)
rw₁ rw₂ :
  mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map g.op =
    mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map g.op
⊢ mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map g.op = mapPreimage K G F (G.map g ≫ f)

Tactic:
rw [mapPreimage_comp, mapPreimage_map]

Premises used: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasWeakSheafify.{v_1, v_4, u_1, u_4} J A
P₁ P₂ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
f : P₁ ⟶ P₂
Q : Sheaf.{v_2, v_4, u_2, u_4} K A
g : obj (sheafifyOfIsEquivalence J K G A) P₂ ⟶ Q
⊢ G.IsLocallyFull K

Tactic:
have := IsDenseSubsite.isLocallyFull J K G
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasWeakSheafify.{v_1, v_4, u_1, u_4} J A
P₁ P₂ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
f : P₁ ⟶ P₂
Q : Sheaf.{v_2, v_4, u_2, u_4} K A
g : obj (sheafifyOfIsEquivalence J K G A) P₂ ⟶ Q
this : G.IsLocallyFull K
⊢ G.IsCoverDense K

Tactic:
have := IsDenseSubsite.isCoverDense J K G
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasWeakSheafify.{v_1, v_4, u_1, u_4} J A
P₁ P₂ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
f : P₁ ⟶ P₂
Q : Sheaf.{v_2, v_4, u_2, u_4} K A
g : obj (sheafifyOfIsEquivalence J K G A) P₂ ⟶ Q
this_1 : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : Adjunction (C := Sheaf.{v_1, v_4, u_1, u_4} J A)
  (Equivalence.functor (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K))))
  (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) :=
  Equivalence.toAdjunction (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))
adj₂ : Adjunction (C := Functor.{v_1, v_4, u_1, u_4} Cᵒᵖ A) (presheafToSheaf J A) (sheafToPresheaf J A) :=
  sheafificationAdjunction J A
⊢ Eq (α :=
    obj (presheafToSheaf J A) (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P₁) ⟶
      obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q)
    ((adj₁.homEquiv (obj (presheafToSheaf J A) (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P₁)) Q :
          (a :
              (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor.obj
                  ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)) ⟶
                Q) →
            (presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁) ⟶
              (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q)
        (map (sheafifyOfIsEquivalence J K G A) f ≫ g) :
      obj (presheafToSheaf J A) (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P₁) ⟶
        obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q)
    (map (presheafToSheaf J A) (G.op.whiskerLeft f) ≫
        (adj₁.homEquiv (obj (presheafToSheaf J A) (G.op ⋙ P₂)) Q :
            (a :
                (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor.obj
                    ((presheafToSheaf J A).obj (G.op ⋙ P₂)) ⟶
                  Q) →
              (presheafToSheaf J A).obj (G.op ⋙ P₂) ⟶
                (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q)
          g :
      obj (presheafToSheaf J A) (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P₁) ⟶
        obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q)

Tactic:
apply adj₁.homEquiv_naturality_left

Premises used: CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasWeakSheafify.{v_1, v_4, u_1, u_4} J A
P : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
Q₁ Q₂ : Sheaf.{v_2, v_4, u_2, u_4} K A
f : obj (sheafifyOfIsEquivalence J K G A) P ⟶ Q₁
g : Q₁ ⟶ Q₂
⊢ G.IsLocallyFull K

Tactic:
have := IsDenseSubsite.isLocallyFull J K G
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasWeakSheafify.{v_1, v_4, u_1, u_4} J A
P : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
Q₁ Q₂ : Sheaf.{v_2, v_4, u_2, u_4} K A
f : obj (sheafifyOfIsEquivalence J K G A) P ⟶ Q₁
g : Q₁ ⟶ Q₂
this : G.IsLocallyFull K
⊢ G.IsCoverDense K

Tactic:
have := IsDenseSubsite.isCoverDense J K G
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_3 : Category.{v_4, u_4} A
inst_4 : IsDenseSubsite J K G
F : Sheaf.{v_1, v_4, u_1, u_4} J A
inst_5 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_6 : HasWeakSheafify.{v_1, v_4, u_1, u_4} J A
P₁ P₂ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
Q : Sheaf.{v_2, v_4, u_2, u_4} K A
f : P₁ ⟶ P₂
g : P₂ ⟶ obj (sheafToPresheaf K A) Q
⊢ Eq (α := P₁ ⟶ Q.obj (P := Presheaf.IsSheaf K))
    ((sheafifyHomEquivOfIsEquivalence J K G : (a : (sheafifyOfIsEquivalence J K G A).obj P₁ ⟶ Q) → P₁ ⟶ Q.obj)
        ((Equiv.symm (sheafifyHomEquivOfIsEquivalence J K G) :
            (a : P₁ ⟶ (sheafToPresheaf K A).obj Q) → (sheafifyOfIsEquivalence J K G A).obj P₁ ⟶ Q)
          (f ≫ g)) :
      P₁ ⟶ Q.obj (P := Presheaf.IsSheaf K))
    ((sheafifyHomEquivOfIsEquivalence J K G : (a : (sheafifyOfIsEquivalence J K G A).obj P₁ ⟶ Q) → P₁ ⟶ Q.obj)
        (map (sheafifyOfIsEquivalence J K G A) f ≫
          (Equiv.symm (sheafifyHomEquivOfIsEquivalence J K G) :
              (a : P₂ ⟶ (sheafToPresheaf K A).obj Q) → (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q)
            g) :
      P₁ ⟶ Q.obj (P := Presheaf.IsSheaf K))

Tactic:
simp [sheafifyHomEquivOfIsEquivalence_naturality_left _ _ _ f]

Premises used: CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasWeakSheafify.{v_1, v_4, u_1, u_4} J A
⊢ HasWeakSheafify.{v_2, v_4, u_2, u_4} K A

Tactic:
⟨_, ⟨sheafifyAdjunctionOfIsEquivalence J K G A⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk, CategoryTheory.Functor.IsDenseSubsite.sheafifyAdjunctionOfIsEquivalence
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasSheafify.{v_1, v_4, u_1, u_4} J A
inst_6 : HasFiniteLimits.{v_4, u_4} A
⊢ PreservesFiniteLimits (C := Functor.{v_1, v_4, u_1, u_4} Cᵒᵖ A)
    (presheafToSheaf J A ⋙ inv (G.sheafPushforwardContinuous A J K))

Tactic:
apply comp_preservesFiniteLimits

Premises used: CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasSheafify.{v_1, v_4, u_1, u_4} J A
inst_6 : HasFiniteLimits.{v_4, u_4} A
⊢ PreservesFiniteLimits (C := Functor.{v_1, v_4, u_1, u_4} Cᵒᵖ A)
    (presheafToSheaf J A ⋙ inv (G.sheafPushforwardContinuous A J K))

Tactic:
have : PreservesFiniteLimits (presheafToSheaf J A ⋙
    (G.sheafPushforwardContinuous A J K).inv) := by
    apply comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasSheafify.{v_1, v_4, u_1, u_4} J A
inst_6 : HasFiniteLimits.{v_4, u_4} A
this :
  PreservesFiniteLimits (C := Functor.{v_1, v_4, u_1, u_4} Cᵒᵖ A)
    (presheafToSheaf J A ⋙ inv (G.sheafPushforwardContinuous A J K))
⊢ PreservesFiniteLimits (C := Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A) (sheafifyOfIsEquivalence J K G A)

Tactic:
apply comp_preservesFiniteLimits

Premises used: CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasSheafify.{v_1, v_4, u_1, u_4} J A
inst_6 : HasFiniteLimits.{v_4, u_4} A
this :
  PreservesFiniteLimits (C := Functor.{v_1, v_4, u_1, u_4} Cᵒᵖ A)
    (presheafToSheaf J A ⋙ inv (G.sheafPushforwardContinuous A J K))
⊢ PreservesFiniteLimits (C := Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A) (sheafifyOfIsEquivalence J K G A)

Tactic:
have : PreservesFiniteLimits (sheafifyOfIsEquivalence J K G A) := by
    apply comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasSheafify.{v_1, v_4, u_1, u_4} J A
inst_6 : HasFiniteLimits.{v_4, u_4} A
this_1 :
  PreservesFiniteLimits (C := Functor.{v_1, v_4, u_1, u_4} Cᵒᵖ A)
    (presheafToSheaf J A ⋙ inv (G.sheafPushforwardContinuous A J K))
this : PreservesFiniteLimits (C := Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A) (sheafifyOfIsEquivalence J K G A)
⊢ HasSheafify.{v_2, v_4, u_2, u_4} K A

Tactic:
HasSheafify.mk' _ _ (sheafifyAdjunctionOfIsEquivalence J K G A)

Premises used: CategoryTheory.HasSheafify.mk', CategoryTheory.Functor.IsDenseSubsite.sheafifyAdjunctionOfIsEquivalence
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasSheafify.{v_1, v_4, u_1, u_4} J A
inst_6 : HasFiniteLimits.{v_4, u_4} A
this_1 :
  PreservesFiniteLimits (C := Functor.{v_1, v_4, u_1, u_4} Cᵒᵖ A)
    (presheafToSheaf J A ⋙ inv (G.sheafPushforwardContinuous A J K))
this : PreservesFiniteLimits (C := Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A) (sheafifyOfIsEquivalence J K G A)
⊢ HasSheafify.{v_2, v_4, u_2, u_4} K A

Tactic:
exact HasSheafify.mk' _ _ (sheafifyAdjunctionOfIsEquivalence J K G A)

Premises used: CategoryTheory.HasSheafify.mk', CategoryTheory.Functor.IsDenseSubsite.sheafifyAdjunctionOfIsEquivalence
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
X : C
data : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F X
P Q : Functor.{v₀, v', u₀, u'} C₀ᵒᵖ A
f : P ⟶ Q
i₁ : data.multicospanShape.L
⊢ Eq (α :=
    (data.multicospanIndex P).multicospan.obj (WalkingMulticospan.left i₁) ⟶
      (data.multicospanIndex Q).multicospan.obj (WalkingMulticospan.left i₁))
    ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left i₁)) ≫
      match (motive :=
        (x : WalkingMulticospan data.multicospanShape) →
          (data.multicospanIndex P).multicospan.obj x ⟶ (data.multicospanIndex Q).multicospan.obj x)
        WalkingMulticospan.left i₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y (j.snd (β := fun (i : data.I₀ × data.I₀) ↦ data.I₁ i.1 i.2)))))
    ((match (motive :=
        (x : WalkingMulticospan data.multicospanShape) →
          (data.multicospanIndex P).multicospan.obj x ⟶ (data.multicospanIndex Q).multicospan.obj x)
        WalkingMulticospan.left i₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j =>
        f.app (op (data.Y (j.snd (β := fun (i : data.I₀ × data.I₀) ↦ data.I₁ i.1 i.2))))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left i₁)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
X : C
data : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F X
P Q : Functor.{v₀, v', u₀, u'} C₀ᵒᵖ A
f : P ⟶ Q
j₂ : data.multicospanShape.R
⊢ Eq (α :=
    (data.multicospanIndex P).multicospan.obj (WalkingMulticospan.left (data.multicospanShape.fst j₂)) ⟶
      (data.multicospanIndex Q).multicospan.obj (WalkingMulticospan.right j₂))
    ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.fst j₂) ≫
      match (motive :=
        (x : WalkingMulticospan data.multicospanShape) →
          (data.multicospanIndex P).multicospan.obj x ⟶ (data.multicospanIndex Q).multicospan.obj x)
        WalkingMulticospan.right j₂ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y (j.snd (β := fun (i : data.I₀ × data.I₀) ↦ data.I₁ i.1 i.2)))))
    ((match (motive :=
        (x : WalkingMulticospan data.multicospanShape) →
          (data.multicospanIndex P).multicospan.obj x ⟶ (data.multicospanIndex Q).multicospan.obj x)
        WalkingMulticospan.left (data.multicospanShape.fst j₂) with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j =>
        f.app (op (data.Y (j.snd (β := fun (i : data.I₀ × data.I₀) ↦ data.I₁ i.1 i.2))))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.fst j₂))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
X : C
data : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F X
P Q : Functor.{v₀, v', u₀, u'} C₀ᵒᵖ A
f : P ⟶ Q
j₂ : data.multicospanShape.R
⊢ Eq (α :=
    (data.multicospanIndex P).multicospan.obj (WalkingMulticospan.left (data.multicospanShape.snd j₂)) ⟶
      (data.multicospanIndex Q).multicospan.obj (WalkingMulticospan.right j₂))
    ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.snd j₂) ≫
      match (motive :=
        (x : WalkingMulticospan data.multicospanShape) →
          (data.multicospanIndex P).multicospan.obj x ⟶ (data.multicospanIndex Q).multicospan.obj x)
        WalkingMulticospan.right j₂ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y (j.snd (β := fun (i : data.I₀ × data.I₀) ↦ data.I₁ i.1 i.2)))))
    ((match (motive :=
        (x : WalkingMulticospan data.multicospanShape) →
          (data.multicospanIndex P).multicospan.obj x ⟶ (data.multicospanIndex Q).multicospan.obj x)
        WalkingMulticospan.left (data.multicospanShape.snd j₂) with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j =>
        f.app (op (data.Y (j.snd (β := fun (i : data.I₀ × data.I₀) ↦ data.I₁ i.1 i.2))))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.snd j₂))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
X : C
data : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F X
P Q : Functor.{v₀, v', u₀, u'} C₀ᵒᵖ A
f : P ⟶ Q
j₁ : data.multicospanShape.R
⊢ Eq (α :=
    (data.multicospanIndex P).multicospan.obj (WalkingMulticospan.right j₁) ⟶
      (data.multicospanIndex Q).multicospan.obj (WalkingMulticospan.right j₁))
    ((data.multicospanIndex P).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right j₁)) ≫
      match (motive :=
        (x : WalkingMulticospan data.multicospanShape) →
          (data.multicospanIndex P).multicospan.obj x ⟶ (data.multicospanIndex Q).multicospan.obj x)
        WalkingMulticospan.right j₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j => f.app (op (data.Y (j.snd (β := fun (i : data.I₀ × data.I₀) ↦ data.I₁ i.1 i.2)))))
    ((match (motive :=
        (x : WalkingMulticospan data.multicospanShape) →
          (data.multicospanIndex P).multicospan.obj x ⟶ (data.multicospanIndex Q).multicospan.obj x)
        WalkingMulticospan.right j₁ with
      | WalkingMulticospan.left i => f.app (op (data.X i))
      | WalkingMulticospan.right j =>
        f.app (op (data.Y (j.snd (β := fun (i : data.I₀ × data.I₀) ↦ data.I₁ i.1 i.2))))) ≫
      (data.multicospanIndex Q).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right j₁)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
X : C
data : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F X
i₁ i₂ : data.I₀
W₀ : C₀
p₁ : W₀ ⟶ data.X i₁
p₂ : W₀ ⟶ data.X i₂
Z Z' : C₀
g : Z ⟶ W₀
j : data.I₁ i₁ i₂
h : Z ⟶ data.Y j
fac₁ : g ≫ p₁ = h ≫ data.p₁ j
fac₂ : g ≫ p₂ = h ≫ data.p₂ j
φ : Z' ⟶ Z
⊢ (φ ≫ g) ≫ p₁ = (φ ≫ h) ≫ data.p₁ j

Tactic:
simpa using φ ≫= fac₁
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
X : C
data : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F X
i₁ i₂ : data.I₀
W₀ : C₀
p₁ : W₀ ⟶ data.X i₁
p₂ : W₀ ⟶ data.X i₂
Z Z' : C₀
g : Z ⟶ W₀
j : data.I₁ i₁ i₂
h : Z ⟶ data.Y j
fac₁ : g ≫ p₁ = h ≫ data.p₁ j
fac₂ : g ≫ p₂ = h ≫ data.p₂ j
φ : Z' ⟶ Z
⊢ (φ ≫ g) ≫ p₂ = (φ ≫ h) ≫ data.p₂ j

Tactic:
simpa using φ ≫= fac₂
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_2 : Category.{v', u'} A
X : C
data : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F X
i₁ i₂ : data.I₀
W₀ : C₀
p₁ : W₀ ⟶ data.X i₁
p₂ : W₀ ⟶ data.X i₂
Z Z' : C₀
g : Z ⟶ W₀
j : data.I₁ i₁ i₂
h : Z ⟶ data.Y j
fac₁ : g ≫ p₁ = h ≫ data.p₁ j
fac₂ : g ≫ p₂ = h ≫ data.p₂ j
φ : Z' ⟶ Z
⊢ ∃ (j : data.I₁ i₁ i₂) (h : Z' ⟶ data.Y j), (φ ≫ g) ≫ p₁ = h ≫ data.p₁ j ∧ (φ ≫ g) ≫ p₂ = h ≫ data.p₂ j

Tactic:
exact ⟨j, φ ≫ h, by simpa using φ ≫= fac₁, by simpa using φ ≫= fac₂⟩
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Goal:
C₀ : Type u₀
C : Type u
inst : Category.{v₀, u₀} C₀
inst_1 : Category.{v, u} C
F : Functor.{v₀, v, u₀, u} C₀ C
J₀ : GrothendieckTopology.{v₀, u₀} C₀
J : GrothendieckTopology.{v, u} C
inst_2 : F.IsOneHypercoverDense J₀ J
inst_3 : F.IsLocallyFull J
inst_4 : F.IsLocallyFaithful J
h :
  ∀ {X₀ : C₀} {S₀ : Sieve.{v₀, u₀} X₀},
    Membership.mem (γ := Set (Sieve.{v, u} (F.obj X₀))) (J.sieves (F.obj X₀)) (Sieve.functorPushforward F S₀) ↔
      S₀ ∈ J₀.sieves X₀
X : C
⊢ Sieve.coverByImage F X ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
J.superset_covering ?_ (F.oneHypercoverDenseData J₀ J X).mem₀

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Functor.oneHypercoverDenseData, CategoryTheory.Functor.OneHypercoverDenseData.mem₀