awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
U : C
π : U ⟶ W
hπ : (Sieve.coverByImage F W).arrows π
refine_2 :
  Membership.mem (γ := Set (Sieve.{v, u} (F.obj (Nonempty.some hπ).obj)))
    ((J : (a : C) → Set (Sieve a)) (F.obj (Nonempty.some hπ).obj))
    (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
⊢ Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p))) ∈
    (J : (a : C) → Set (Sieve a)) U

Tactic:
apply J.pullback_stable

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- 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 : IsDenseSubsite J₀ J F
X : C
data : OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this_1 : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ →
  ⦃p : W ⟶ F.obj X₀⦄ →
    (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p →
      Sieve.{v, u} W :=
  fun (W : C) (p : W ⟶ F.obj X₀)
      (hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p) ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun (U : C) (π : U ⟶ W) (hπ : (Sieve.coverByImage F W).arrows π) ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v, u} data.toOneHypercover.toPreZeroHypercover)).arrows p
U : C
π : U ⟶ W
hπ : (Sieve.coverByImage F W).arrows π
⊢ Membership.mem (γ := Set (Sieve.{v, u} (F.obj (Nonempty.some hπ).obj)))
    ((J : (a : C) → Set (Sieve a)) (F.obj (Nonempty.some hπ).obj))
    (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))

Tactic:
apply functorPushforward_imageSieve_mem

Premises used: CategoryTheory.Functor.functorPushforward_imageSieve_mem
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i : (data X).I₀
W₀ : C₀
a : W₀ ⟶ (data X).X i
ha : (↑S : Sieve X).arrows (F.map a ≫ (data X).f i)
⊢ liftAux hG₀ s i ≫ G.map (F.map a).op = s.ι { Y := F.obj W₀, f := F.map a ≫ (data X).f i, hf := ha }

Tactic:
hG₀.amalgamate_map _ _ _ ⟨W₀, a, ha⟩

Premises used: CategoryTheory.Presheaf.IsSheaf.amalgamate_map, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).toOneHypercover.I₀
j : (data X).toOneHypercover.I₁ (i₁, i₂).1 (i₁, i₂).2
dsimp : liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op
⊢ Eq (α :=
    s.pt ⟶
      ((data X).toOneHypercover.multicospanIndex G).right
        (Sigma.mk (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
          (data X).toOneHypercover.I₁ i.1 i.2) (i₁, i₂) j))
    ((fun (i : (data X).toOneHypercover.multicospanShape.L) ↦ liftAux hG₀ s i)
        ((data X).toOneHypercover.multicospanShape.fst
          (Sigma.mk (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
            (data X).toOneHypercover.I₁ i.1 i.2) (i₁, i₂) j)) ≫
      ((data X).toOneHypercover.multicospanIndex G).fst
        (Sigma.mk (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
          (data X).toOneHypercover.I₁ i.1 i.2) (i₁, i₂) j))
    ((fun (i : (data X).toOneHypercover.multicospanShape.L) ↦ liftAux hG₀ s i)
        ((data X).toOneHypercover.multicospanShape.snd
          (Sigma.mk (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
            (data X).toOneHypercover.I₁ i.1 i.2) (i₁, i₂) j)) ≫
      ((data X).toOneHypercover.multicospanIndex G).snd
        (Sigma.mk (β := fun (i : (data X).toOneHypercover.I₀ × (data X).toOneHypercover.I₀) ↦
          (data X).toOneHypercover.I₁ i.1 i.2) (i₁, i₂) j))

Tactic:
dsimp at i₁ i₂ j ⊢
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
⊢ liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op

Tactic:
Presheaf.IsSheaf.hom_ext
      hG₀ ⟨_, cover_lift F J₀ _
        (J.pullback_stable (F.map ((data X).p₁ j) ≫ (data X).f i₁) S.2)⟩ _ _ ?_

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Functor.map, Subtype.mk, CategoryTheory.Functor.PreOneHypercoverDenseData.p₁, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.PreOneHypercoverDenseData.f, CategoryTheory.Functor.cover_lift, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData, Subtype.property
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
refine :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
          Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j)) S)
          (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯)),
    (liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op) ≫ (F.op ⋙ G).map I.f.op =
      (liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op) ≫ (F.op ⋙ G).map I.f.op
⊢ liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op

Tactic:
refine Presheaf.IsSheaf.hom_ext
      hG₀ ⟨_, cover_lift F J₀ _
        (J.pullback_stable (F.map ((data X).p₁ j) ≫ (data X).f i₁) S.2)⟩ _ _ ?_

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Functor.map, Subtype.mk, CategoryTheory.Functor.PreOneHypercoverDenseData.p₁, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.PreOneHypercoverDenseData.f, CategoryTheory.Functor.cover_lift, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData, Subtype.property
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
dsimp :
  (liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op) ≫ G.map (F.map a).op =
    (liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op) ≫ G.map (F.map a).op
⊢ (liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op) ≫
      (F.op ⋙ G).map
        { Y := W₀, f := a, hf := ha :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
                  Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j)))
                    ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j)) S)
                  (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X)))
                  ⋯) }.f.op =
    (liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op) ≫ (F.op ⋙ G).map { Y := W₀, f := a, hf := ha }.f.op

Tactic:
dsimp
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
simp : liftAux hG₀ s i₁ ≫ G.map (F.map (a ≫ (data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map (a ≫ (data X).p₂ j)).op
⊢ (liftAux hG₀ s i₁ ≫ G.map (F.map ((data X).p₁ j)).op) ≫ G.map (F.map a).op =
    (liftAux hG₀ s i₂ ≫ G.map (F.map ((data X).p₂ j)).op) ≫ G.map (F.map a).op

Tactic:
simp only [assoc, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
⊢ (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)

Tactic:
simpa using ha
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
⊢ (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)

Tactic:
have ha₁ : S (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁) := by simpa using ha
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
rwa : (↑S : Sieve X).arrows (F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂)
rwa₁ rwa₂ rwa₃ rwa₄ : (↑S : Sieve X).arrows (F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁)
⊢ (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)

Tactic:
rwa [Functor.map_comp_assoc, ← (data X).w j]

Premises used: CategoryTheory.Functor.PreOneHypercoverDenseData.w, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
⊢ (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)

Tactic:
have ha₂ : S (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂) := by
      rwa [Functor.map_comp_assoc, ← (data X).w j]
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
rw :
  Eq (α := s.pt ⟶ G.obj (op (F.obj W₀)))
    (s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ } :
      s.pt ⟶ (S.index G).left { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ })
    (s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂, hf := ha₂ })
⊢ liftAux hG₀ s i₁ ≫ G.map (F.map (a ≫ (data X).p₁ j)).op = liftAux hG₀ s i₂ ≫ G.map (F.map (a ≫ (data X).p₂ j)).op

Tactic:
rw [liftAux_fac _ _ _ ha₁, liftAux_fac _ _ _ ha₂]

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux_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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
h : F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂
⊢ Eq (α := s.pt ⟶ G.obj (op (F.obj W₀)))
    (s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ } :
      s.pt ⟶ (S.index G).left { Y := F.obj W₀, f := F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁, hf := ha₁ })
    (s.ι { Y := F.obj W₀, f := F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂, hf := ha₂ })

Tactic:
congr 2
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i₁ i₂ : (data X).I₀
j : (data X).I₁ i₁ i₂
W₀ : C₀
a : W₀ ⟶ (data X).Y j
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v₀, u₀} ((data X).Y j)) ↦
            Membership.mem (γ := Set (Sieve.{v₀, u₀} ((data X).Y j))) ((J₀ : (a : C₀) → Set (Sieve a)) ((data X).Y j))
              S)
            (Sieve.functorPullback F (Sieve.pullback (F.map ((data X).p₁ j) ≫ (data X).f i₁) (↑S : Sieve X))) ⋯) :
        Sieve ((data X).Y j)).arrows
    a
ha₁ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁)
ha₂ : (↑S : Sieve X).arrows (F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂)
h : F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂
h₁ : F.map a ≫ F.map ((data X).p₁ j) ≫ (data X).f i₁ = F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂
h₂ h₃ : F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂ = F.map a ≫ F.map ((data X).p₂ j) ≫ (data X).f i₂
⊢ F.map (a ≫ (data X).p₁ j) ≫ (data X).f i₁ = F.map (a ≫ (data X).p₂ j) ≫ (data X).f i₂

Tactic:
rw [map_comp_assoc, map_comp_assoc, (data X).w j]

Premises used: CategoryTheory.Functor.PreOneHypercoverDenseData.w, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData
-- 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
inst_3 : IsDenseSubsite J₀ J F
data : (X : C) → OneHypercoverDenseData.{u_1, v₀, v, u₀, u} F J₀ J X
G : Functor.{v, v', u, u'} Cᵒᵖ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
i : (data X).I₀
⊢ lift hG₀ hG s ≫ G.map ((data X).f i).op = liftAux hG₀ s i

Tactic:
Multifork.IsLimit.fac _ _ _ _

Premises used: CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift, CategoryTheory.Limits.Multifork.IsLimit.fac, CategoryTheory.Limits.Multifork.ι