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 : 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
refine :
  PreZeroHypercover.sieve₀.{w, v, u} (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.toPreZeroHypercover ≤
    Sieve.coverByImage F X
⊢ Sieve.coverByImage F X ∈ (J : (a : C) → Set (Sieve a)) X

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

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Functor.oneHypercoverDenseData, CategoryTheory.Functor.OneHypercoverDenseData.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
inst_2 : F.IsOneHypercoverDense J₀ J
inst_3 : F.IsLocallyFull J
inst_4 : F.IsLocallyFaithful J
h_1 :
  ∀ {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 Y w : C
a : Y ⟶ w
w_1 : w ⟶ X
h :
  Presieve.ofArrows (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.X
    (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.f w_1
mk :
  ∀ (i : (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.I₀)
    (a : Y ⟶ (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.X i),
    (Sieve.coverByImage F X).arrows (a ≫ (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.f i)
⊢ (Sieve.coverByImage F X).arrows (a ≫ w_1)

Tactic:
cases h
-- 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 Y : C
i : (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.I₀
a : Y ⟶ (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.X i
⊢ (Sieve.coverByImage F X).arrows (a ≫ (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.f i)

Tactic:
⟨{ fac := rfl, ..}⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.PreOneHypercover.toPreZeroHypercover, CategoryTheory.Functor.oneHypercoverDenseData, Nonempty.intro, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover, CategoryTheory.Presieve.coverByImage, CategoryTheory.Presieve.CoverByImageStructure.mk, CategoryTheory.Functor.PreOneHypercoverDenseData.X, CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData, rfl
-- 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 Y : C
i : (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.I₀
a : Y ⟶ (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.X i
⊢ (Sieve.coverByImage F X).arrows (a ≫ (F.oneHypercoverDenseData J₀ J X).toPreOneHypercover.f i)

Tactic:
exact ⟨{ fac := rfl, ..}⟩
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
hF :
  ∀ (S : C),
    ∃ (ι : Type w) (U : ι → C₀) (f : (i : ι) → F.obj (U i) ⟶ S),
      Sieve.ofArrows (fun (i : ι) ↦ F.obj (U i)) f ∈ (J : (a : C) → Set (Sieve a)) S
S : C
choose :
  ∀ (ι : (S : C) → Type w) (U : (S : C) → ι S → C₀) (f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S)
    (hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S),
    Nonempty (OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J S)
⊢ Nonempty (OneHypercoverDenseData.{w, v₀, v, u₀, u} F J₀ J S)

Tactic:
choose ι U f hf using hF
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
k : ι (pullback (f S i) (f S j))
⊢ F.map (F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j))) ≫ f S i =
    F.map (F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j))) ≫ f S j

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
⊢ F.IsCoverDense J

Tactic:
have := IsDenseSubsite.isCoverDense J₀ J F
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
rw :
  Membership.mem (γ := Set (Sieve.{v, u} (F.obj W₀))) ((J : (a : C) → Set (Sieve a)) (F.obj W₀))
    (Sieve.functorPushforward F
      ({ I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
            Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
            p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
              F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
            p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
              F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
            w := ⋯ : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F S }.sieve₁₀
        p₁ p₂))
⊢ { I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
          Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
          p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
            F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
          p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
            F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
          w := ⋯ : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F S }.sieve₁₀
      p₁ p₂ ∈
    (J₀ : (a : C₀) → Set (Sieve a)) W₀

Tactic:
rw [← functorPushforward_mem_iff J₀ J F]

Premises used: CategoryTheory.Functor.functorPushforward_mem_iff
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
⊢ Membership.mem (γ := Set (Sieve.{v, u} (F.obj W₀))) ((J : (a : C) → Set (Sieve a)) (F.obj W₀))
    (Sieve.functorPushforward F
      ({ I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
            Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
            p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
              F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
            p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
              F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
            w := ⋯ : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F S }.sieve₁₀
        p₁ p₂))

Tactic:
J.superset_covering ?_
          (IsCoverDense.functorPullback_pushforward_covering
            ⟨_, J.pullback_stable (pullback.lift _ _ hp) (hf (pullback (f _ i) (f _ j)))⟩)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Limits.pullback, CategoryTheory.Limits.pullback.lift, CategoryTheory.GrothendieckTopology.pullback_stable, Subtype.mk, CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
refine :
  Sieve.functorPushforward F
      (Sieve.functorPullback F
        (↑(Subtype.mk (p := fun (x : Sieve.{v, u} (F.obj W₀)) ↦
              Membership.mem (γ := Set (Sieve.{v, u} (F.obj W₀))) ((J : (a : C) → Set (Sieve a)) (F.obj W₀)) x)
              (Sieve.pullback (X := pullback (f S i) (f S j)) (pullback.lift (F.map p₁) (F.map p₂) hp)
                (Sieve.ofArrows (fun (i_1 : ι (pullback (f S i) (f S j))) ↦ F.obj (U (pullback (f S i) (f S j)) i_1))
                  (f (pullback (f S i) (f S j)))))
              ⋯) :
          Sieve (F.obj W₀))) ≤
    Sieve.functorPushforward F
      ({ I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
            Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
            p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
              F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
            p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
              F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
            w := ⋯ : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F S }.sieve₁₀
        p₁ p₂)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (F.obj W₀))) ((J : (a : C) → Set (Sieve a)) (F.obj W₀))
    (Sieve.functorPushforward F
      ({ I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
            Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
            p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
              F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
            p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
              F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
            w := ⋯ : PreOneHypercoverDenseData.{w, v₀, v, u₀, u} F S }.sieve₁₀
        p₁ p₂))

Tactic:
refine J.superset_covering ?_
          (IsCoverDense.functorPullback_pushforward_covering
            ⟨_, J.pullback_stable (pullback.lift _ _ hp) (hf (pullback (f _ i) (f _ j)))⟩)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.Limits.pullback, CategoryTheory.Limits.pullback.lift, CategoryTheory.GrothendieckTopology.pullback_stable, Subtype.mk, CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
⊢ (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.fst (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.fst (f S i) (f S j))

Tactic:
have fac₁ := fac =≫ pullback.fst _ _
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.fst (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.fst (f S i) (f S j))
⊢ (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.snd (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.snd (f S i) (f S j))

Tactic:
have fac₂ := fac =≫ pullback.snd _ _
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.fst (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.fst (f S i) (f S j))
fac₂ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.snd (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.snd (f S i) (f S j))
⊢ s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j) = F.map q ≫ F.map p₁

Tactic:
simp only [Category.assoc, pullback.lift_fst, pullback.lift_snd] at fac₁ fac₂

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.pullback.lift_fst
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.fst (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.fst (f S i) (f S j))
fac₂ :
  (s ≫ f (pullback (f S i) (f S j)) k) ≫ pullback.snd (f S i) (f S j) =
    CategoryStruct.comp (Y := pullback (f S i) (f S j)) (F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp)
      (pullback.snd (f S i) (f S j))
fac₃ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j) = F.map q ≫ F.map p₁
⊢ s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j) = F.map q ≫ F.map p₂

Tactic:
simp only [Category.assoc, pullback.lift_fst, pullback.lift_snd] at fac₁ fac₂

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.pullback.lift_fst
-- 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
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j) = F.map q ≫ F.map p₁
fac₂ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j) = F.map q ≫ F.map p₂
⊢ F.map (q ≫ p₁) =
    F.map
      (F.preimage s ≫
        { I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
              Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
              p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
              w := ⋯ }.p₁
          k)

Tactic:
simp [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 : IsDenseSubsite J₀ J F
inst_3 : HasPullbacks.{v, u} C
inst_4 : F.Full
inst_5 : F.Faithful
S : C
ι : (S : C) → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun (i : ι S) ↦ F.obj (U S i)) (f S) ∈ (J : (a : C) → Set (Sieve a)) S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j) = F.map q ≫ F.map p₁
fac₂ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j) = F.map q ≫ F.map p₂
⊢ F.map (q ≫ p₂) =
    F.map
      (F.preimage s ≫
        { I₀ := ι S, X := U S, f := f S, I₁ := fun (i j : ι S) ↦ ι (pullback (f S i) (f S j)),
              Y := fun (i j : ι S) ↦ U (pullback (f S i) (f S j)),
              p₁ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun (i j : ι S) (k : ι (pullback (f S i) (f S j))) ↦
                F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)),
              w := ⋯ }.p₂
          k)

Tactic:
simp [fac₂]