-- Mathlib/CategoryTheory/Sites/Over.lean
lemma over_map_compatiblePreserving {X Y : C} (f : X ⟶ Y) :
    CompatiblePreserving (J.over Y) (Over.map f) where
  compatible {F Z _ x hx Y₁ Y₂ W f₁ f₂ g₁ g₂ hg₁ hg₂ h}

Proof state:
case h.e'_3.h.e_a
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₂.op = ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk f₂.left ⋯)).op

Tactic:
congr 1

Result:
case h.e'_3.h.e_a.e_f
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₂ = (Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk f₂.left ⋯)

Proof state:
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ F.val.map f₂.op (x g₂ hg₂) =
    F.val.map (((Over.map f).map (Over.homMk f₂.left ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op) (x g₂ hg₂)

Tactic:
apply congr_fun

Result:
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ F.val.map f₂.op = F.val.map (((Over.map f).map (Over.homMk f₂.left ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)

Proof state:
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ F.val.map f₂.op (x g₂ hg₂) =
    F.val.map (Over.isoMk (Iso.refl W.left) ⋯).inv.op
      (F.val.map ((Over.map f).map (Over.homMk f₂.left ⋯)).op (x g₂ hg₂))

Tactic:
rw [← FunctorToTypes.map_comp_apply]

Result:
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ F.val.map f₂.op (x g₂ hg₂) =
    F.val.map (((Over.map f).map (Over.homMk f₂.left ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op) (x g₂ hg₂)

Proof state:
case h.e'_3.h.e_a.e_f.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ f₂.left = ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk f₂.left ⋯)).left

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ F.val.map f₂.op (x g₂ hg₂) = F.val.map e.inv.op (((Over.map f).op ⋙ F.val).map g₂'.op (x g₂ hg₂))

Tactic:
dsimp [e, W', g₁', g₂']

Result:
case h.e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.val) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁.left ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂.left ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ F.val.map f₂.op (x g₂ hg₂) =
    F.val.map (Over.isoMk (Iso.refl W.left) ⋯).inv.op
      (F.val.map ((Over.map f).map (Over.homMk f₂.left ⋯)).op (x g₂ hg₂))