awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ :
  F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₁.op =
    F.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₁.op) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₁))) → F.obj.obj (Opposite.op W))
        (x g₁ hg₁) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.obj (P := Presheaf.IsSheaf (J.over Y)).map
              (((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₁))) → F.obj.obj (Opposite.op W))
        (x g₁ hg₁) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))

Tactic:
apply ConcreteCategory.congr_hom

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ : f₁.op = ((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op
⊢ F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₁.op =
    F.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ : f₁.op = Quiver.Hom.op ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯))
⊢ f₁.op = ((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op

Tactic:
rw [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ : f₁ = (Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)
⊢ f₁.op = Quiver.Hom.op ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ :
  Over.Hom.left f₁ =
    Over.Hom.left ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯))
⊢ f₁ = (Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ Over.Hom.left f₁ =
    Over.Hom.left ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ :
  Eq (α := F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₂.op) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₂))) → F.obj.obj (Opposite.op W))
        (x g₂ hg₂) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.obj (P := Presheaf.IsSheaf (J.over Y)).map
              (((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₂))) → F.obj.obj (Opposite.op W))
        (x g₂ hg₂) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₂.op) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₂))) → F.obj.obj (Opposite.op W))
        (x g₂ hg₂) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.obj (P := Presheaf.IsSheaf (J.over Y)).map (Over.isoMk (Iso.refl W.left) ⋯).inv.op) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj (Over.mk (Over.Hom.left f₁ ≫ Y₁.hom))))) →
            F.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.obj (P := Presheaf.IsSheaf (J.over Y)).map ((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op) :
              (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₂))) →
                F.obj.obj (Opposite.op ((Over.map f).obj (Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)))))
            (x g₂ hg₂) :
          F.obj (P := Presheaf.IsSheaf (J.over Y)).obj
            (Opposite.op ((Over.map f).obj (Over.mk (Over.Hom.left f₁ ≫ Y₁.hom))))) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))

Tactic:
rw [← Functor.map_comp_apply]

Premises used: CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ :
  F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₂.op =
    F.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₂.op) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₂))) → F.obj.obj (Opposite.op W))
        (x g₂ hg₂) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.obj (P := Presheaf.IsSheaf (J.over Y)).map
              (((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)) :
          (a : F.obj.obj (Opposite.op ((Over.map f).obj Y₂))) → F.obj.obj (Opposite.op W))
        (x g₂ hg₂) :
      F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W))

Tactic:
apply ConcreteCategory.congr_hom

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ : f₂.op = ((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op
⊢ F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₂.op =
    F.obj (P := Presheaf.IsSheaf (J.over Y)).map
      (((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ : f₂.op = Quiver.Hom.op ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯))
⊢ f₂.op = ((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op

Tactic:
rw [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ : f₂ = (Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)
⊢ f₂.op = Quiver.Hom.op ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ :
  Over.Hom.left f₂ =
    Over.Hom.left ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯))
⊢ f₂ = (Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ Over.Hom.left f₂ =
    Over.Hom.left ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (Over.map f).IsContinuous (J.over X) (J.over Y)

Tactic:
Functor.isContinuous_of_coverPreserving
    (over_map_compatiblePreserving J f)
    (over_map_coverPreserving J f)

Premises used: CategoryTheory.GrothendieckTopology.over_map_coverPreserving, CategoryTheory.Functor.isContinuous_of_coverPreserving, CategoryTheory.GrothendieckTopology.over_map_compatiblePreserving
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
hS :
  Membership.mem (γ := Set (Sieve ((Over.map f).obj U)))
    ((J.over Y : (a : Over Y) → Set (Sieve a)) ((Over.map f).obj U)) S
rw :
  ∀
    (hS :
      Membership.mem (α := Sieve.{v, u} ((Over.map f).obj U).left) (γ := Set (Sieve.{v, u} ((Over.map f).obj U).left))
        ((J : (a : C) → Set (Sieve a)) ((Over.map f).obj U).left)
        ((Sieve.overEquiv ((Over.map f).obj U) : (a : Sieve ((Over.map f).obj U)) → Sieve ((Over.map f).obj U).left) S :
          Sieve.{v, u} ((Over.map f).obj U).left)),
    Membership.mem (α := Sieve.{v, u} U.left) (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
      ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) (Sieve.functorPullback (Over.map f) S) : Sieve.{v, u} U.left)
⊢ Sieve.functorPullback (Over.map f) S ∈ (J.over X : (a : Over X) → Set (Sieve a)) U

Tactic:
rw [J.mem_over_iff] at hS ⊢

Premises used: CategoryTheory.GrothendieckTopology.mem_over_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
hS :
  Membership.mem (α := Sieve.{v, u} ((Over.map f).obj U).left) (γ := Set (Sieve.{v, u} ((Over.map f).obj U).left))
    ((J : (a : C) → Set (Sieve a)) ((Over.map f).obj U).left)
    ((Sieve.overEquiv ((Over.map f).obj U) : (a : Sieve ((Over.map f).obj U)) → Sieve ((Over.map f).obj U).left) S :
      Sieve.{v, u} ((Over.map f).obj U).left)
rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (α := Sieve.{v, u} U.left) (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
    ((Sieve.overEquiv ((Over.map f).obj U) : (a : Sieve ((Over.map f).obj U)) → Sieve ((Over.map f).obj U).left) S :
      Sieve.{v, u} ((Over.map f).obj U).left)
⊢ Membership.mem (α := Sieve.{v, u} U.left) (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
    ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) (Sieve.functorPullback (Over.map f) S) : Sieve.{v, u} U.left)

Tactic:
rwa [Sieve.overEquiv_functorPullback_map]

Premises used: CategoryTheory.Sieve.overEquiv_functorPullback_map
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.IsCocontinuous J K
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
hS :
  Membership.mem (γ := Set (Sieve (Functor.obj (Over.post F) U)))
    ((K.over (F.obj X) : (a : Over (F.obj X)) → Set (Sieve a)) (Functor.obj (Over.post F) U)) S
rw :
  ∀
    (hS :
      Membership.mem (α := Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left) (γ :=
        Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left))
        ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) U).left)
        ((Sieve.overEquiv (Functor.obj (Over.post F) U) :
              (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
            S :
          Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left)),
    Membership.mem (α := Sieve.{v, u} U.left) (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
      ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) (Sieve.functorPullback (Over.post F) S) : Sieve.{v, u} U.left)
⊢ Sieve.functorPullback (Over.post F) S ∈ (J.over X : (a : Over X) → Set (Sieve a)) U

Tactic:
rw [GrothendieckTopology.mem_over_iff] at hS ⊢

Premises used: CategoryTheory.GrothendieckTopology.mem_over_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.IsCocontinuous J K
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
hS :
  Membership.mem (α := Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left) (γ :=
    Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left))
    ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) U).left)
    ((Sieve.overEquiv (Functor.obj (Over.post F) U) :
          (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S :
      Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left)
rw :
  Membership.mem (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
    (Sieve.functorPullback F
      ((Sieve.overEquiv (Functor.obj (Over.post F) U) :
          (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S))
⊢ Membership.mem (α := Sieve.{v, u} U.left) (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
    ((Sieve.overEquiv U : (a : Sieve U) → Sieve U.left) (Sieve.functorPullback (Over.post F) S) : Sieve.{v, u} U.left)

Tactic:
rw [Sieve.overEquiv_functorPullback_post]

Premises used: CategoryTheory.Sieve.overEquiv_functorPullback_post
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
K : GrothendieckTopology.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
inst_2 : F.IsCocontinuous J K
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
hS :
  Membership.mem (α := Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left) (γ :=
    Set (Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left))
    ((K : (a : D) → Set (Sieve a)) (Functor.obj (Over.post F) U).left)
    ((Sieve.overEquiv (Functor.obj (Over.post F) U) :
          (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S :
      Sieve.{v_1, u_1} (Functor.obj (Over.post F) U).left)
⊢ Membership.mem (γ := Set (Sieve.{v, u} U.left)) ((J : (a : C) → Set (Sieve a)) U.left)
    (Sieve.functorPullback F
      ((Sieve.overEquiv (Functor.obj (Over.post F) U) :
          (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S))

Tactic:
F.cover_lift J K hS

Premises used: CategoryTheory.Functor.cover_lift