awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u'
inst : Category.{v_1, u'} C
inst_1 : HasBinaryProducts.{v_1, u'} C
J : GrothendieckTopology.{v_1, u'} C
X U : C
S : Sieve.{v_1, u'} U
hs : S ∈ (J : (a : C) → Set (Sieve a)) U
refine :
  LE.le (α := Sieve.{v_1, u'} (Over.left.{v_1, u'} (Functor.obj (Over.star X) U))) (Sieve.pullback prod.snd S)
    ((Sieve.overEquiv (Functor.obj (Over.star X) U) :
        (a : Sieve ((Over.star X).obj U)) → Sieve ((Over.star X).obj U).left)
      (Sieve.functorPushforward (Over.star X) S))
⊢ Membership.mem (γ := Set (Sieve (C := Over.{v_1, u'} X) (Functor.obj (Over.star X) U)))
    ((J.over X : (a : Over X) → Set (Sieve a)) (Functor.obj (Over.star X) U)) (Sieve.functorPushforward (Over.star X) S)

Tactic:
refine J.superset_covering ?_ (J.pullback_stable prod.snd hs)

Premises used: CategoryTheory.GrothendieckTopology.superset_covering, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Limits.prod.snd
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u'
inst : Category.{v_1, u'} C
inst_1 : HasBinaryProducts.{v_1, u'} C
J : GrothendieckTopology.{v_1, u'} C
X U : C
S : Sieve.{v_1, u'} U
hs : S ∈ (J : (a : C) → Set (Sieve a)) U
y : C
f : y ⟶ Over.left.{v_1, u'} (Functor.obj (Over.star X) U)
hf : Sieve.arrows (Sieve.pullback prod.snd S) f
rw : Presieve.functorPushforward (Over.star X ⋙ Over.forget X) S.arrows f
⊢ Presieve.functorPushforward (Over.forget X) (X := Functor.obj (Over.star X) U)
    (Presieve.functorPushforward (Over.star X) S.arrows) (Y := y) f

Tactic:
rw [← Presieve.functorPushforward_comp]

Premises used: CategoryTheory.Presieve.functorPushforward_comp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u'
inst : Category.{v_1, u'} C
inst_1 : HasBinaryProducts.{v_1, u'} C
J : GrothendieckTopology.{v_1, u'} C
X U : C
S : Sieve.{v_1, u'} U
hs : S ∈ (J : (a : C) → Set (Sieve a)) U
y : C
f : y ⟶ Over.left.{v_1, u'} (Functor.obj (Over.star X) U)
hf : Sieve.arrows (Sieve.pullback prod.snd S) f
⊢ Presieve.functorPushforward (Over.star X ⋙ Over.forget X) S.arrows f

Tactic:
⟨_, _, prod.lift (f ≫ prod.fst) (𝟙 _), hf, Limits.prod.hom_ext ?_ ?_⟩

Premises used: CategoryTheory.Limits.prod.fst, CategoryTheory.CategoryStruct.id, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Presieve.functorPushforward, CategoryTheory.Limits.prod.hom_ext, CategoryTheory.Limits.prod.lift
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u'
inst : Category.{v_1, u'} C
inst_1 : HasBinaryProducts.{v_1, u'} C
J : GrothendieckTopology.{v_1, u'} C
X U : C
S : Sieve.{v_1, u'} U
hs : S ∈ (J : (a : C) → Set (Sieve a)) U
y : C
f : y ⟶ Over.left.{v_1, u'} (Functor.obj (Over.star X) U)
hf : Sieve.arrows (Sieve.pullback prod.snd S) f
refine_1 :
  f ≫ prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v_1, u'} X U)
      (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u', u'} (Over.star X ⋙ Over.forget X) y)
        (prod.lift (f ≫ prod.fst) (𝟙 y)) (Functor.map (Over.star X ⋙ Over.forget X) (f ≫ prod.snd)))
      prod.fst
refine_2 :
  f ≫ prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v_1, u'} X U)
      (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u', u'} (Over.star X ⋙ Over.forget X) y)
        (prod.lift (f ≫ prod.fst) (𝟙 y)) (Functor.map (Over.star X ⋙ Over.forget X) (f ≫ prod.snd)))
      prod.snd
⊢ Presieve.functorPushforward (Over.star X ⋙ Over.forget X) S.arrows f

Tactic:
refine ⟨_, _, prod.lift (f ≫ prod.fst) (𝟙 _), hf, Limits.prod.hom_ext ?_ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u'
inst : Category.{v_1, u'} C
inst_1 : HasBinaryProducts.{v_1, u'} C
J : GrothendieckTopology.{v_1, u'} C
X U : C
S : Sieve.{v_1, u'} U
hs : S ∈ (J : (a : C) → Set (Sieve a)) U
y : C
f : y ⟶ Over.left.{v_1, u'} (Functor.obj (Over.star X) U)
hf : Sieve.arrows (Sieve.pullback prod.snd S) f
⊢ f ≫ prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v_1, u'} X U)
      (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u', u'} (Over.star X ⋙ Over.forget X) y)
        (prod.lift (f ≫ prod.fst) (𝟙 y)) (Functor.map (Over.star X ⋙ Over.forget X) (f ≫ prod.snd)))
      prod.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u'
inst : Category.{v_1, u'} C
inst_1 : HasBinaryProducts.{v_1, u'} C
J : GrothendieckTopology.{v_1, u'} C
X U : C
S : Sieve.{v_1, u'} U
hs : S ∈ (J : (a : C) → Set (Sieve a)) U
y : C
f : y ⟶ Over.left.{v_1, u'} (Functor.obj (Over.star X) U)
hf : Sieve.arrows (Sieve.pullback prod.snd S) f
⊢ f ≫ prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v_1, u'} X U)
      (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u', u'} (Over.star X ⋙ Over.forget X) y)
        (prod.lift (f ≫ prod.fst) (𝟙 y)) (Functor.map (Over.star X ⋙ Over.forget X) (f ≫ prod.snd)))
      prod.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
J_1 : GrothendieckTopology.{v, u} C_1
C : Type u'
inst_1 : Category.{v_1, u'} C
inst_2 : HasBinaryProducts.{v_1, u'} C
J : GrothendieckTopology.{v_1, u'} C
X : C
⊢ Functor.IsContinuous (Over.star X) J (J.over X)

Tactic:
Functor.isContinuous_of_coverPreserving
    (compatiblePreservingOfFlat (J.over X) (Over.star X)) (coverPreserving_over_star X)

Premises used: CategoryTheory.compatiblePreservingOfFlat, CategoryTheory.Functor.isContinuous_of_coverPreserving, CategoryTheory.GrothendieckTopology.coverPreserving_over_star, CategoryTheory.Over.star, CategoryTheory.GrothendieckTopology.over
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f g : X ⟶ Y
h : f = g
subst : Eq (α := Sheaf (J.over Y) A ⥤ Sheaf (J.over X) A) (J.overMapPullback A f) (J.overMapPullback A f)
⊢ Eq (α := Sheaf (J.over Y) A ⥤ Sheaf (J.over X) A) (J.overMapPullback A f) (J.overMapPullback A g)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
⊢ Eq (α := Sheaf (J.over Y) A ⥤ Sheaf (J.over X) A) (J.overMapPullback A f) (J.overMapPullback A f)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f g : X ⟶ Y
h : f = g
⊢ Eq (α := Iso (C := Sheaf (J.over Y) A ⥤ Sheaf (J.over X) A) (J.overMapPullback A f) (J.overMapPullback A g))
    (J.overMapPullbackCongr A h) (eqToIso ⋯)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
w :
  ∀ (x : Sheaf (J.over Y) A) (x_1 : (Over.{v, u} X)ᵒᵖ),
    (NatTrans.app
              (Iso.inv (J.overMapPullbackComp A f (𝟙 Y)) ≫
                Functor.whiskerRight (Iso.hom (J.overMapPullbackId A Y)) (J.overMapPullback A f) ≫
                  Iso.hom (Functor.leftUnitor (J.overMapPullback A f)))
              x).hom.app
        x_1 =
      (NatTrans.app (Iso.hom (J.overMapPullbackCongr A ⋯)) x).hom.app x_1
⊢ Eq (α :=
    Quiver.Hom (V := Sheaf (J.over Y) A ⥤ Sheaf (J.over X) A) (J.overMapPullback A (f ≫ 𝟙 Y)) (J.overMapPullback A f))
    (Iso.inv (J.overMapPullbackComp A f (𝟙 Y)) ≫
      Functor.whiskerRight (Iso.hom (J.overMapPullbackId A Y)) (J.overMapPullback A f) ≫
        Iso.hom (Functor.leftUnitor (J.overMapPullback A f)))
    (Iso.hom (J.overMapPullbackCongr A ⋯))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x : Sheaf (J.over Y) A
x_1 : (Over.{v, u} X)ᵒᵖ
w :
  (NatTrans.app (Iso.inv (J.overMapPullbackComp A f (𝟙 Y))) x).hom.app x_1 ≫
      (NatTrans.app (Iso.hom (J.overMapPullbackId A Y)) x).hom.app
          (Opposite.op ((Over.map f).obj (Opposite.unop x_1))) ≫
        𝟙 (x.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op ((Over.map f).obj (Opposite.unop x_1)))) =
    x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (Quiver.Hom.op ((Over.mapCongr (f ≫ 𝟙 Y) f ⋯).inv.app (Opposite.unop x_1)))
⊢ (NatTrans.app
            (Iso.inv (J.overMapPullbackComp A f (𝟙 Y)) ≫
              Functor.whiskerRight (Iso.hom (J.overMapPullbackId A Y)) (J.overMapPullback A f) ≫
                Iso.hom (Functor.leftUnitor (J.overMapPullback A f)))
            x).hom.app
      x_1 =
    (NatTrans.app (Iso.hom (J.overMapPullbackCongr A ⋯)) x).hom.app x_1

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x : Sheaf (J.over Y) A
x_1 : (Over.{v, u} X)ᵒᵖ
w :
  x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (NatTrans.app (Iso.inv (Over.mapId Y)) ((Over.map f).obj (Opposite.unop x_1)) ≫
          (Over.mapComp f (𝟙 Y)).inv.app (Opposite.unop x_1)).op =
    x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (Quiver.Hom.op ((Over.mapCongr (f ≫ 𝟙 Y) f ⋯).inv.app (Opposite.unop x_1)))
⊢ (NatTrans.app (Iso.inv (J.overMapPullbackComp A f (𝟙 Y))) x).hom.app x_1 ≫
      (NatTrans.app (Iso.hom (J.overMapPullbackId A Y)) x).hom.app
          (Opposite.op ((Over.map f).obj (Opposite.unop x_1))) ≫
        𝟙 (x.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op ((Over.map f).obj (Opposite.unop x_1)))) =
    x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (Quiver.Hom.op ((Over.mapCongr (f ≫ 𝟙 Y) f ⋯).inv.app (Opposite.unop x_1)))

Tactic:
simp only [overMapPullbackComp_inv_app_hom_app, overMapPullbackId_hom_app_hom_app,
    comp_id, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_hom_app, CategoryTheory.Category.comp_id, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_app, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x : Sheaf (J.over Y) A
x_1 : (Over.{v, u} X)ᵒᵖ
w :
  NatTrans.app (Iso.inv (Over.mapId Y)) ((Over.map f).obj (Opposite.unop x_1)) ≫
      (Over.mapComp f (𝟙 Y)).inv.app (Opposite.unop x_1) =
    (Over.mapCongr (f ≫ 𝟙 Y) f ⋯).inv.app (Opposite.unop x_1)
⊢ x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (NatTrans.app (Iso.inv (Over.mapId Y)) ((Over.map f).obj (Opposite.unop x_1)) ≫
          (Over.mapComp f (𝟙 Y)).inv.app (Opposite.unop x_1)).op =
    x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (Quiver.Hom.op ((Over.mapCongr (f ≫ 𝟙 Y) f ⋯).inv.app (Opposite.unop x_1)))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
w :
  ∀ (x : Sheaf (J.over Y) A) (x_1 : (Over.{v, u} X)ᵒᵖ),
    (NatTrans.app
              (Iso.inv (J.overMapPullbackComp A (𝟙 X) f) ≫
                Functor.whiskerLeft (J.overMapPullback A f) (Iso.hom (J.overMapPullbackId A X)) ≫
                  Iso.hom (Functor.rightUnitor (J.overMapPullback A f)))
              x).hom.app
        x_1 =
      (NatTrans.app (Iso.hom (J.overMapPullbackCongr A ⋯)) x).hom.app x_1
⊢ Eq (α :=
    Quiver.Hom (V := Sheaf (J.over Y) A ⥤ Sheaf (J.over X) A) (J.overMapPullback A (𝟙 X ≫ f)) (J.overMapPullback A f))
    (Iso.inv (J.overMapPullbackComp A (𝟙 X) f) ≫
      Functor.whiskerLeft (J.overMapPullback A f) (Iso.hom (J.overMapPullbackId A X)) ≫
        Iso.hom (Functor.rightUnitor (J.overMapPullback A f)))
    (Iso.hom (J.overMapPullbackCongr A ⋯))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x : Sheaf (J.over Y) A
x_1 : (Over.{v, u} X)ᵒᵖ
w :
  (NatTrans.app (Iso.inv (J.overMapPullbackComp A (𝟙 X) f)) x).hom.app x_1 ≫
      (NatTrans.app (Iso.hom (J.overMapPullbackId A X)) (Functor.obj (J.overMapPullback A f) x)).hom.app x_1 ≫
        𝟙 (x.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op ((Over.map f).obj (Opposite.unop x_1)))) =
    x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (Quiver.Hom.op ((Over.mapCongr (𝟙 X ≫ f) f ⋯).inv.app (Opposite.unop x_1)))
⊢ (NatTrans.app
            (Iso.inv (J.overMapPullbackComp A (𝟙 X) f) ≫
              Functor.whiskerLeft (J.overMapPullback A f) (Iso.hom (J.overMapPullbackId A X)) ≫
                Iso.hom (Functor.rightUnitor (J.overMapPullback A f)))
            x).hom.app
      x_1 =
    (NatTrans.app (Iso.hom (J.overMapPullbackCongr A ⋯)) x).hom.app x_1

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x : Sheaf (J.over Y) A
x_1 : (Over.{v, u} X)ᵒᵖ
w :
  x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      ((Over.map f).map (NatTrans.app (Iso.inv (Over.mapId X)) (Opposite.unop x_1)) ≫
          NatTrans.app (Iso.inv (Over.mapComp (𝟙 X) f)) (Opposite.unop x_1)).op =
    x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (Quiver.Hom.op ((Over.mapCongr (𝟙 X ≫ f) f ⋯).inv.app (Opposite.unop x_1)))
⊢ (NatTrans.app (Iso.inv (J.overMapPullbackComp A (𝟙 X) f)) x).hom.app x_1 ≫
      (NatTrans.app (Iso.hom (J.overMapPullbackId A X)) (Functor.obj (J.overMapPullback A f) x)).hom.app x_1 ≫
        𝟙 (x.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op ((Over.map f).obj (Opposite.unop x_1)))) =
    x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (Quiver.Hom.op ((Over.mapCongr (𝟙 X ≫ f) f ⋯).inv.app (Opposite.unop x_1)))

Tactic:
simp only [overMapPullbackComp_inv_app_hom_app, overMapPullbackId_hom_app_hom_app,
    Functor.sheafPushforwardContinuous_obj_obj_map, Quiver.Hom.unop_op,
    comp_id, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, Quiver.Hom.unop_op, CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_hom_app, CategoryTheory.Category.comp_id, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_app, CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_map, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x : Sheaf (J.over Y) A
x_1 : (Over.{v, u} X)ᵒᵖ
w :
  (Over.map f).map (NatTrans.app (Iso.inv (Over.mapId X)) (Opposite.unop x_1)) ≫
      NatTrans.app (Iso.inv (Over.mapComp (𝟙 X) f)) (Opposite.unop x_1) =
    (Over.mapCongr (𝟙 X ≫ f) f ⋯).inv.app (Opposite.unop x_1)
⊢ x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      ((Over.map f).map (NatTrans.app (Iso.inv (Over.mapId X)) (Opposite.unop x_1)) ≫
          NatTrans.app (Iso.inv (Over.mapComp (𝟙 X) f)) (Opposite.unop x_1)).op =
    x.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (Quiver.Hom.op ((Over.mapCongr (𝟙 X ≫ f) f ⋯).inv.app (Opposite.unop x_1)))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ f ≫ g ≫ h = (f ≫ g) ≫ h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
w :
  ∀ (x : Sheaf (J.over T) A) (x_1 : (Over.{v, u} X)ᵒᵖ),
    (NatTrans.app
              (Iso.inv (J.overMapPullbackComp A f (g ≫ h)) ≫
                Functor.whiskerRight (Iso.inv (J.overMapPullbackComp A g h)) (J.overMapPullback A f) ≫
                  Iso.hom (Functor.associator (J.overMapPullback A h) (J.overMapPullback A g) (J.overMapPullback A f)) ≫
                    Functor.whiskerLeft (J.overMapPullback A h) (Iso.hom (J.overMapPullbackComp A f g)) ≫
                      Iso.hom (J.overMapPullbackComp A (f ≫ g) h))
              x).hom.app
        x_1 =
      (NatTrans.app (Iso.hom (J.overMapPullbackCongr A ⋯)) x).hom.app x_1
⊢ Eq (α :=
    Quiver.Hom (V := Sheaf (J.over T) A ⥤ Sheaf (J.over X) A) (J.overMapPullback A (f ≫ g ≫ h))
      (J.overMapPullback A ((f ≫ g) ≫ h)))
    (Iso.inv (J.overMapPullbackComp A f (g ≫ h)) ≫
      Functor.whiskerRight (Iso.inv (J.overMapPullbackComp A g h)) (J.overMapPullback A f) ≫
        Iso.hom (Functor.associator (J.overMapPullback A h) (J.overMapPullback A g) (J.overMapPullback A f)) ≫
          Functor.whiskerLeft (J.overMapPullback A h) (Iso.hom (J.overMapPullbackComp A f g)) ≫
            Iso.hom (J.overMapPullbackComp A (f ≫ g) h))
    (Iso.hom (J.overMapPullbackCongr A ⋯))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
x : Sheaf (J.over T) A
x_1 : (Over.{v, u} X)ᵒᵖ
w :
  (NatTrans.app (Iso.inv (J.overMapPullbackComp A f (g ≫ h))) x).hom.app x_1 ≫
      (NatTrans.app (Iso.inv (J.overMapPullbackComp A g h)) x).hom.app
          (Opposite.op ((Over.map f).obj (Opposite.unop x_1))) ≫
        𝟙
            (x.obj (P := Presheaf.IsSheaf (J.over T)).obj
              (Opposite.op ((Over.map h).obj ((Over.map g).obj ((Over.map f).obj (Opposite.unop x_1)))))) ≫
          (NatTrans.app (Iso.hom (J.overMapPullbackComp A f g)) (Functor.obj (J.overMapPullback A h) x)).hom.app x_1 ≫
            (NatTrans.app (Iso.hom (J.overMapPullbackComp A (f ≫ g) h)) x).hom.app x_1 =
    x.obj (P := Presheaf.IsSheaf (J.over T)).map
      (Quiver.Hom.op ((Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) ⋯).inv.app (Opposite.unop x_1)))
⊢ (NatTrans.app
            (Iso.inv (J.overMapPullbackComp A f (g ≫ h)) ≫
              Functor.whiskerRight (Iso.inv (J.overMapPullbackComp A g h)) (J.overMapPullback A f) ≫
                Iso.hom (Functor.associator (J.overMapPullback A h) (J.overMapPullback A g) (J.overMapPullback A f)) ≫
                  Functor.whiskerLeft (J.overMapPullback A h) (Iso.hom (J.overMapPullbackComp A f g)) ≫
                    Iso.hom (J.overMapPullbackComp A (f ≫ g) h))
            x).hom.app
      x_1 =
    (NatTrans.app (Iso.hom (J.overMapPullbackCongr A ⋯)) x).hom.app x_1

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
x : Sheaf (J.over T) A
x_1 : (Over.{v, u} X)ᵒᵖ
w :
  Eq (α :=
    x.obj (P := Presheaf.IsSheaf (J.over T)).obj (Opposite.op ((Over.map (f ≫ g ≫ h)).obj (Opposite.unop x_1))) ⟶
      x.obj (P := Presheaf.IsSheaf (J.over T)).obj (Opposite.op ((Over.map ((f ≫ g) ≫ h)).obj (Opposite.unop x_1))))
    (x.obj (P := Presheaf.IsSheaf (J.over T)).map
      (Quiver.Hom.op
        ((Over.mapComp (f ≫ g) h).hom.app (Opposite.unop x_1) ≫
          (Over.map h).map ((Over.mapComp f g).hom.app (Opposite.unop x_1)) ≫
            (Over.mapComp g h).inv.app ((Over.map f).obj (Opposite.unop x_1)) ≫
              (Over.mapComp f (g ≫ h)).inv.app (Opposite.unop x_1))))
    (x.obj (P := Presheaf.IsSheaf (J.over T)).map
      (Quiver.Hom.op ((Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) ⋯).inv.app (Opposite.unop x_1))))
⊢ (NatTrans.app (Iso.inv (J.overMapPullbackComp A f (g ≫ h))) x).hom.app x_1 ≫
      (NatTrans.app (Iso.inv (J.overMapPullbackComp A g h)) x).hom.app
          (Opposite.op ((Over.map f).obj (Opposite.unop x_1))) ≫
        𝟙
            (x.obj (P := Presheaf.IsSheaf (J.over T)).obj
              (Opposite.op ((Over.map h).obj ((Over.map g).obj ((Over.map f).obj (Opposite.unop x_1)))))) ≫
          (NatTrans.app (Iso.hom (J.overMapPullbackComp A f g)) (Functor.obj (J.overMapPullback A h) x)).hom.app x_1 ≫
            (NatTrans.app (Iso.hom (J.overMapPullbackComp A (f ≫ g) h)) x).hom.app x_1 =
    x.obj (P := Presheaf.IsSheaf (J.over T)).map
      (Quiver.Hom.op ((Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) ⋯).inv.app (Opposite.unop x_1)))

Tactic:
simp only [overMapPullbackComp_inv_app_hom_app,
    overMapPullbackComp_hom_app_hom_app, Functor.sheafPushforwardContinuous_obj_obj_map,
    Quiver.Hom.unop_op, ← Functor.map_comp, ← op_comp, id_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, Quiver.Hom.unop_op, CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_hom_app, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_app, CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_map, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
x : Sheaf (J.over T) A
x_1 : (Over.{v, u} X)ᵒᵖ
w :
  Eq (α := (Over.map ((f ≫ g) ≫ h)).obj (Opposite.unop x_1) ⟶ (Over.map (f ≫ g ≫ h)).obj (Opposite.unop x_1))
    ((Over.mapComp (f ≫ g) h).hom.app (Opposite.unop x_1) ≫
      (Over.map h).map ((Over.mapComp f g).hom.app (Opposite.unop x_1)) ≫
        (Over.mapComp g h).inv.app ((Over.map f).obj (Opposite.unop x_1)) ≫
          (Over.mapComp f (g ≫ h)).inv.app (Opposite.unop x_1))
    ((Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) ⋯).inv.app (Opposite.unop x_1))
⊢ Eq (α :=
    x.obj (P := Presheaf.IsSheaf (J.over T)).obj (Opposite.op ((Over.map (f ≫ g ≫ h)).obj (Opposite.unop x_1))) ⟶
      x.obj (P := Presheaf.IsSheaf (J.over T)).obj (Opposite.op ((Over.map ((f ≫ g) ≫ h)).obj (Opposite.unop x_1))))
    (x.obj (P := Presheaf.IsSheaf (J.over T)).map
      (Quiver.Hom.op
        ((Over.mapComp (f ≫ g) h).hom.app (Opposite.unop x_1) ≫
          (Over.map h).map ((Over.mapComp f g).hom.app (Opposite.unop x_1)) ≫
            (Over.mapComp g h).inv.app ((Over.map f).obj (Opposite.unop x_1)) ≫
              (Over.mapComp f (g ≫ h)).inv.app (Opposite.unop x_1))))
    (x.obj (P := Presheaf.IsSheaf (J.over T)).map
      (Quiver.Hom.op ((Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) ⋯).inv.app (Opposite.unop x_1))))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
⊢ K.toGrothendieck.over X = (Precoverage.comap (Over.forget X) K).toGrothendieck

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X : C
refine_1 : K.toGrothendieck.over X ≤ (Precoverage.comap (Over.forget X) K).toGrothendieck
refine_2 : (Precoverage.comap (Over.forget X) K).toGrothendieck ≤ K.toGrothendieck.over X
⊢ K.toGrothendieck.over X = (Precoverage.comap (Over.forget X) K).toGrothendieck

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm