Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case inr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this✝ :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
hf' : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f'))
this : Presheaf.IsLocallySurjective J f'
V : C
g : V ⟶ U
v : ToType ((pullback f (shrinkYonedaEquiv.symm s)).obj (op V))
hv :
  (ConcreteCategory.hom (f'.app (op V))) v =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U))
⊢ (ConcreteCategory.hom ((shrinkYonedaEquiv.symm s).app (op V)))
      ((ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U))) =
    (ConcreteCategory.hom (F₂.map g.op)) s

Tactic:
refine (congr_arg _ (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op (𝟙 _))).trans ?_

Goal state after:
case inr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this✝ :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
hf' : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f'))
this : Presheaf.IsLocallySurjective J f'
V : C
g : V ⟶ U
v : ToType ((pullback f (shrinkYonedaEquiv.symm s)).obj (op V))
hv :
  (ConcreteCategory.hom (f'.app (op V))) v =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj U).map g.op)) (shrinkYonedaObjObjEquiv.symm (𝟙 U))
⊢ (ConcreteCategory.hom ((shrinkYonedaEquiv.symm s).app (op V)))
      (shrinkYonedaObjObjEquiv.symm (g.op.unop ≫ 𝟙 (unop (op U)))) =
    (ConcreteCategory.hom (F₂.map g.op)) s