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
inst_2 : IsDenseSubsite J K G
U V : C
f₁ f₂ : U ⟶ V
e : G.map f₁ = G.map f₂
⊢ Sieve.equalizer f₁ f₂ ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
letI := IsDenseSubsite.isLocallyFaithful J K G
  IsDenseSubsite.functorPushforward_mem_iff.mp (G.functorPushforward_equalizer_mem K f₁ f₂ e)

Premises used: CategoryTheory.Functor.functorPushforward_equalizer_mem, CategoryTheory.Functor.IsDenseSubsite.functorPushforward_mem_iff, Iff.mp
-- 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 : C
f₁ f₂ : X ⟶ Y
h : G.map f₁ = G.map f₂
W₀ : C
a : W₀ ⟶ X
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (Sieve.equalizer f₁ f₂) ⋯) :
        Sieve X).arrows
    a
dsimp :
  F.obj (P := Presheaf.IsSheaf J).map f₁.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op =
    F.obj (P := Presheaf.IsSheaf J).map f₂.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op
⊢ F.obj (P := Presheaf.IsSheaf J).map f₁.op ≫
      F.obj (P := Presheaf.IsSheaf J).map
        { Y := W₀, f := a, hf := ha :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X)
                  (Sieve.equalizer f₁ f₂) ⋯) }.f.op =
    F.obj (P := Presheaf.IsSheaf J).map f₂.op ≫ F.obj (P := Presheaf.IsSheaf J).map { Y := W₀, f := a, hf := ha }.f.op

Tactic:
dsimp at ha ⊢
-- 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 : C
f₁ f₂ : X ⟶ Y
h : G.map f₁ = G.map f₂
W₀ : C
a : W₀ ⟶ X
ha : a ≫ f₁ = a ≫ f₂
⊢ F.obj (P := Presheaf.IsSheaf J).map f₁.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op =
    F.obj (P := Presheaf.IsSheaf J).map f₂.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op

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

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_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
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha :
  (↑(Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Z) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Z)
            (Sieve.pullback p (G.imageSieve f)) ⋯) :
        Sieve Z).arrows
    a
dsimp :
  (mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map p.op) ≫ F.obj (P := Presheaf.IsSheaf J).map a.op =
    F.obj (P := Presheaf.IsSheaf J).map g.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op
⊢ (mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map p.op) ≫
      F.obj (P := Presheaf.IsSheaf J).map
        { Y := W₀, f := a, hf := ha :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} Z) ↦ S ∈ (J : (a : C) → Set (Sieve a)) Z)
                  (Sieve.pullback p (G.imageSieve f)) ⋯) }.f.op =
    F.obj (P := Presheaf.IsSheaf J).map g.op ≫ F.obj (P := Presheaf.IsSheaf J).map { Y := W₀, f := a, hf := ha }.f.op

Tactic:
dsimp at ha ⊢
-- 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
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
rw :
  ⋯.amalgamate (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) ⋯)
        (fun
            (x :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f)
                  ⋯)) ↦
          (match (motive :=
              (x :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X)
                      (G.imageSieve f) ⋯)) →
                F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y))
              x with
            | { Y := W₀, f := a, hf := ha } =>
              F.obj (P := Presheaf.IsSheaf J).map
                (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map a ≫ f) ha).op :
            F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y)))
        ⋯ ≫
      F.obj (P := Presheaf.IsSheaf J).map (a ≫ p).op =
    F.obj (P := Presheaf.IsSheaf J).map g.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op
⊢ (mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map p.op) ≫ F.obj (P := Presheaf.IsSheaf J).map a.op =
    F.obj (P := Presheaf.IsSheaf J).map g.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op

Tactic:
rw [Category.assoc, ← Functor.map_comp, ← op_comp, mapPreimage]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.IsDenseSubsite.mapPreimage
-- 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
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
rw :
  (match (motive :=
      (x :
          GrothendieckTopology.Cover.Arrow
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) ⋯)) →
        F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y))
      { Y := W₀, f := a ≫ p, hf := ha } with
    | { Y := W₀, f := a, hf := ha } =>
      F.obj (P := Presheaf.IsSheaf J).map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map a ≫ f) ha).op) =
    F.obj (P := Presheaf.IsSheaf J).map (a ≫ g).op
⊢ ⋯.amalgamate (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) ⋯)
        (fun
            (x :
              GrothendieckTopology.Cover.Arrow
                (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f)
                  ⋯)) ↦
          (match (motive :=
              (x :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X)
                      (G.imageSieve f) ⋯)) →
                F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y))
              x with
            | { Y := W₀, f := a, hf := ha } =>
              F.obj (P := Presheaf.IsSheaf J).map
                (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map a ≫ f) ha).op :
            F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y)))
        ⋯ ≫
      F.obj (P := Presheaf.IsSheaf J).map (a ≫ p).op =
    F.obj (P := Presheaf.IsSheaf J).map g.op ≫ F.obj (P := Presheaf.IsSheaf J).map a.op

Tactic:
rw [F.2.amalgamate_map ⟨_, imageSieve_mem J K G f⟩
        (fun ⟨W₀, a, ha⟩ ↦ F.obj.map ha.choose.op) _ ⟨W₀, a ≫ p, ha⟩,
        ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Presheaf.IsSheaf.amalgamate_map, Quiver.Hom, Quiver.Hom.op, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, Subtype.mk, Opposite.op, CategoryTheory.CategoryStruct.comp, CategoryTheory.GrothendieckTopology.Cover.Arrow.mk, CategoryTheory.Functor.map_comp, Exists.choose, CategoryTheory.GrothendieckTopology.Cover.Arrow.Y, CategoryTheory.Functor.obj, CategoryTheory.Functor.IsDenseSubsite.mapPreimage.match_1, CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem
-- 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
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
h : G.map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map (a ≫ p) ≫ f) ha) = G.map (a ≫ g)
⊢ (match (motive :=
      (x :
          GrothendieckTopology.Cover.Arrow
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) ⋯)) →
        F.obj (P := Presheaf.IsSheaf J).obj (op Y) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op x.Y))
      { Y := W₀, f := a ≫ p, hf := ha } with
    | { Y := W₀, f := a, hf := ha } =>
      F.obj (P := Presheaf.IsSheaf J).map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map a ≫ f) ha).op) =
    F.obj (P := Presheaf.IsSheaf J).map (a ≫ g).op

Tactic:
apply map_eq_of_eq K G

Premises used: CategoryTheory.Functor.IsDenseSubsite.map_eq_of_eq
-- 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
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (G.imageSieve f).arrows (a ≫ p)
h : G.map (a ≫ p) ≫ f = G.map (a ≫ g)
h₁ : G.map a ≫ G.map p ≫ f = G.map (a ≫ g)
h₂ : G.map a ≫ G.map p ≫ f = G.map a ≫ G.map g
h₃ h₄ : G.map a ≫ G.map g = G.map a ≫ G.map g
⊢ G.map (Exists.choose (p := fun (l : W₀ ⟶ Y) ↦ G.map l = G.map (a ≫ p) ≫ f) ha) = G.map (a ≫ g)

Tactic:
rw [ha.choose_spec, Functor.map_comp_assoc, Functor.map_comp, fac]

Premises used: Exists.choose_spec, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_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
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y : C
f : G.obj X ⟶ G.obj Y
g : X ⟶ Y
h : G.map g = f
⊢ G.map (𝟙 X) ≫ f = G.map g

Tactic:
simpa using h.symm

Premises used: Eq.symm
-- 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 : C
f : G.obj X ⟶ G.obj Y
g : X ⟶ Y
h : G.map g = f
⊢ mapPreimage K G F f = F.obj (P := Presheaf.IsSheaf J).map g.op

Tactic:
simpa using mapPreimage_map_of_fac K G F f (𝟙 _) g (by simpa using h.symm)

Premises used: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac, CategoryTheory.CategoryStruct.id
-- 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 : C
f : X ⟶ Y
⊢ mapPreimage K G F (G.map f) = F.obj (P := Presheaf.IsSheaf J).map f.op

Tactic:
mapPreimage_of_eq K G F (G.map f) f rfl

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_of_eq, rfl
-- 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 : C
rw : mapPreimage K G F (G.map (𝟙 X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
rw₁ : F.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (𝟙 X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
rw₂ : F.obj (P := Presheaf.IsSheaf J).map (𝟙 (op X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))
rw₃ rw₄ :
  Eq.{v_4 + 1} (α := F.obj (P := Presheaf.IsSheaf J).obj (op X) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op X))
    (𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))) (𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X)))
⊢ mapPreimage K G F (𝟙 (G.obj X)) = 𝟙 (F.obj (P := Presheaf.IsSheaf J).obj (op X))

Tactic:
rw [← G.map_id, mapPreimage_map, op_id, map_id]

Premises used: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map, CategoryTheory.Functor.map_id, CategoryTheory.op_id
-- 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 : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
h :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} T₀) ↦ S ∈ (J : (a : C) → Set (Sieve a)) T₀)
          (Sieve.pullback b (G.imageSieve g)) ⋯)),
    Eq (α := F.obj (P := Presheaf.IsSheaf J).obj (op Z) ⟶ F.obj (P := Presheaf.IsSheaf J).obj (op I.Y))
      ((mapPreimage K G F (f ≫ g) ≫
          F.obj (P := Presheaf.IsSheaf J).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := a, hf := ⋯ }))) ≫
        F.obj (P := Presheaf.IsSheaf J).map I.f.op)
      (((mapPreimage K G F g ≫ mapPreimage K G F f) ≫
          F.obj (P := Presheaf.IsSheaf J).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := a, hf := ⋯ }))) ≫
        F.obj (P := Presheaf.IsSheaf J).map I.f.op)
⊢ Eq (α :=
    F.obj (P := Presheaf.IsSheaf J).obj (op Z) ⟶
      F.obj (P := Presheaf.IsSheaf J).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J) (S :=
            Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) ⋯)
            { Y := T₀, f := a, hf := ⋯ })))
    (mapPreimage K G F (f ≫ g) ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := a, hf := ⋯ })))
    ((mapPreimage K G F g ≫ mapPreimage K G F f) ≫
      F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := a, hf := ⋯ })))

Tactic:
apply Presheaf.IsSheaf.hom_ext F.property
        ⟨_, J.pullback_stable b (imageSieve_mem J K G g)⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.GrothendieckTopology.pullback_stable, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem
-- 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 : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
h :
  (mapPreimage K G F (f ≫ g) ≫ F.obj (P := Presheaf.IsSheaf J).map a.op) ≫ F.obj (P := Presheaf.IsSheaf J).map c.op =
    ((mapPreimage K G F g ≫ mapPreimage K G F f) ≫ F.obj (P := Presheaf.IsSheaf J).map a.op) ≫
      F.obj (P := Presheaf.IsSheaf J).map c.op
⊢ Eq (α :=
    F.obj (P := Presheaf.IsSheaf J).obj (op Z) ⟶
      F.obj (P := Presheaf.IsSheaf J).obj
        (op
          (GrothendieckTopology.Cover.Arrow.Y (J := J) (S :=
            Subtype.mk (p := fun (S : Sieve.{v_1, u_1} T₀) ↦ S ∈ (J : (a : C) → Set (Sieve a)) T₀)
              (Sieve.pullback b (G.imageSieve g)) ⋯)
            { Y := U₀, f := c, hf := ⋯ })))
    (CategoryStruct.comp (Y := F.obj (P := Presheaf.IsSheaf J).obj (op T₀))
      (mapPreimage K G F (f ≫ g) ≫
          F.obj (P := Presheaf.IsSheaf J).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := a, hf := ⋯ })) :
        F.obj (P := Presheaf.IsSheaf J).obj (op Z) ⟶
          F.obj (P := Presheaf.IsSheaf J).obj
            (op
              (GrothendieckTopology.Cover.Arrow.Y (J := J) (S :=
                Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) ⋯)
                { Y := T₀, f := a, hf := ⋯ })))
      (F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := U₀, f := c, hf := ⋯ }))))
    (CategoryStruct.comp (Y := F.obj (P := Presheaf.IsSheaf J).obj (op T₀))
      ((mapPreimage K G F g ≫ mapPreimage K G F f) ≫
          F.obj (P := Presheaf.IsSheaf J).map
            (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := T₀, f := a, hf := ⋯ })) :
        F.obj (P := Presheaf.IsSheaf J).obj (op Z) ⟶
          F.obj (P := Presheaf.IsSheaf J).obj
            (op
              (GrothendieckTopology.Cover.Arrow.Y (J := J) (S :=
                Subtype.mk (p := fun (S : Sieve.{v_1, u_1} X) ↦ S ∈ (J : (a : C) → Set (Sieve a)) X) (G.imageSieve f) ⋯)
                { Y := T₀, f := a, hf := ⋯ })))
      (F.obj (P := Presheaf.IsSheaf J).map
        (Quiver.Hom.op (GrothendieckTopology.Cover.Arrow.f { Y := U₀, f := c, hf := ⋯ }))))

Tactic:
dsimp
-- 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 : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
h :
  mapPreimage K G F (f ≫ g) ≫ F.obj (P := Presheaf.IsSheaf J).map (c ≫ a).op =
    mapPreimage K G F g ≫ mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map (c ≫ a).op
⊢ (mapPreimage K G F (f ≫ g) ≫ F.obj (P := Presheaf.IsSheaf J).map a.op) ≫ F.obj (P := Presheaf.IsSheaf J).map c.op =
    ((mapPreimage K G F g ≫ mapPreimage K G F f) ≫ F.obj (P := Presheaf.IsSheaf J).map a.op) ≫
      F.obj (P := Presheaf.IsSheaf J).map c.op

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Functor.map_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
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
h : G.map (c ≫ b) ≫ g = G.map d
h₁ : G.map (c ≫ a) ≫ f = G.map (c ≫ b)
h₂ : G.map (c ≫ a) ≫ f ≫ g = G.map d
⊢ mapPreimage K G F (f ≫ g) ≫ F.obj (P := Presheaf.IsSheaf J).map (c ≫ a).op =
    mapPreimage K G F g ≫ mapPreimage K G F f ≫ F.obj (P := Presheaf.IsSheaf J).map (c ≫ a).op

Tactic:
rw [mapPreimage_map_of_fac K G F (f ≫ g) (c ≫ a) d,
        mapPreimage_map_of_fac K G F f (c ≫ a) (c ≫ b),
        mapPreimage_map_of_fac K G F g (c ≫ b) d]

Premises used: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac, CategoryTheory.CategoryStruct.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
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ b) ≫ g = G.map d

Tactic:
simp only [Functor.map_comp, Category.assoc, fac₁, fac₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_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
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ a) ≫ f = G.map (c ≫ b)

Tactic:
simp only [Functor.map_comp, Category.assoc, fac₁, fac₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_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
F : Sheaf.{v_1, v_4, u_1, u_4} J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ a) ≫ f ≫ g = G.map d

Tactic:
simp only [Functor.map_comp, Category.assoc, fac₁, fac₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp