Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: 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₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U))
      ((ConcreteCategory.hom (Φ.obj.fiber.map t)) v) =
    (ConcreteCategory.hom (Φ.obj.toPresheafFiber V v (shrinkYoneda.{w, v, u}.obj U))) (shrinkYonedaObjObjEquiv.symm t)

pp: 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₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.toPresheafFiber V v (shrinkYoneda.{w, v, u}.obj U))) (shrinkYonedaObjObjEquiv.symm t) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u

Tactic:
· rw [← Φ.obj.presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app]
      exact Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.naturality_apply t v

Goal state after:
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₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
Φ : P.FullSubcategory
u : Φ.obj.fiber.obj U
V : C
v : Φ.obj.fiber.obj V
y : ToType (F₁.obj (op V))
hx₁ :
  (ConcreteCategory.hom (Φ.obj.presheafFiber.map f)) ((ConcreteCategory.hom (Φ.obj.toPresheafFiber V v F₁)) y) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u
t : unop (op V) ⟶ U
ht : shrinkYonedaObjObjEquiv.symm t = (ConcreteCategory.hom (f.app (op V))) y
⊢ (ConcreteCategory.hom (Φ.obj.toPresheafFiber V v (shrinkYoneda.{w, v, u}.obj U))) (shrinkYonedaObjObjEquiv.symm t) =
    (ConcreteCategory.hom (Φ.obj.shrinkYonedaCompPresheafFiberIso.inv.app U)) u