-- Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean
lemma Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff
    [HasWeakSheafify J (Type v)]
    (F : Sheaf J (Type v)) (sq : Square C) :
    (sq.op.map ((yoneda ⋙ presheafToSheaf J _).op ⋙ yoneda.obj F)).IsPullback ↔
      (sq.op.map F.val).IsPullback

Proof state:
case refine_4.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
x : (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₃
⊢ (⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
        (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₃₄)
      x =
    ((sq.op.map F.val).f₃₄ ∘
        ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv))
      x

Tactic:
dsimp

Result:
case refine_4.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
x : (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₃
⊢ yonedaEquiv
      (((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₁) F)
        ((presheafToSheaf J (Type v)).map (yoneda.map sq.f₁₃) ≫ x)) =
    F.val.map sq.f₁₃.op (yonedaEquiv (((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₃) F) x))

Proof state:
case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₃₄ =
    (sq.op.map F.val).f₃₄ ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv)

Tactic:
ext x

Result:
case refine_4.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
x : (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₃
⊢ (⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
        (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₃₄)
      x =
    ((sq.op.map F.val).f₃₄ ∘
        ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv))
      x

Proof state:
case refine_4.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
x : (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₃
⊢ yonedaEquiv
      (((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₁) F)
        ((presheafToSheaf J (Type v)).map (yoneda.map sq.f₁₃) ≫ x)) =
    yonedaEquiv (yoneda.map sq.f₁₃ ≫ ((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₃) F) x)

Tactic:
erw [Adjunction.homEquiv_naturality_left]

Result:
case refine_4.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
x : (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₃
⊢ yonedaEquiv (yoneda.map sq.f₁₃ ≫ ((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₃) F) x) =
    yonedaEquiv (yoneda.map sq.f₁₃ ≫ ((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₃) F) x)

Proof state:
case refine_4.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
x : (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₃
⊢ yonedaEquiv (yoneda.map sq.f₁₃ ≫ ((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₃) F) x) =
    yonedaEquiv (yoneda.map sq.f₁₃ ≫ ((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₃) F) x)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).IsPullback ↔ (sq.op.map F.val).IsPullback

Tactic:
refine Square.IsPullback.iff_of_equiv _ _
  (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
  (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
  (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
  (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv) ?_ ?_ ?_ ?_

Result:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv) ∘
      (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₁₂ =
    (sq.op.map F.val).f₁₂ ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv)

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv) ∘
      (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₁₃ =
    (sq.op.map F.val).f₁₃ ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv)

case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₂₄ =
    (sq.op.map F.val).f₂₄ ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv)

case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₃₄ =
    (sq.op.map F.val).f₃₄ ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv)

Proof state:
case refine_4.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
x : (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₃
⊢ yonedaEquiv
      (((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₁) F)
        ((presheafToSheaf J (Type v)).map (yoneda.map sq.f₁₃) ≫ x)) =
    F.val.map sq.f₁₃.op (yonedaEquiv (((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₃) F) x))

Tactic:
rw [yonedaEquiv_naturality]

Result:
case refine_4.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
x : (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₃
⊢ yonedaEquiv
      (((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₁) F)
        ((presheafToSheaf J (Type v)).map (yoneda.map sq.f₁₃) ≫ x)) =
    yonedaEquiv (yoneda.map sq.f₁₃ ≫ ((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj sq.X₃) F) x)