Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
eq₁ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (G.obj.map g₁.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₁))) (t f₁ hf₁))
eq₂ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂)) =
    (ConcreteCategory.hom (G.obj.map g₂.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₂))) (t f₂ hf₂))
eq₃ :
  (ConcreteCategory.hom (G.obj.map g₁.op))
      ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₁))) (Presheaf.localPreimage f.hom s f₁ hf₁)) =
    (ConcreteCategory.hom (G.obj.map g₁.op)) ((ConcreteCategory.hom (G.obj.map f₁.op)) s)
eq₄ :
  (ConcreteCategory.hom (G.obj.map g₂.op))
      ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₂))) (Presheaf.localPreimage f.hom s f₂ hf₂)) =
    (ConcreteCategory.hom (G.obj.map g₂.op)) ((ConcreteCategory.hom (G.obj.map f₂.op)) s)
⊢ (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂))

Tactic:
refine eq₁.trans (eq₃.trans (Eq.trans ?_ (eq₄.symm.trans eq₂.symm)))

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
eq₁ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (G.obj.map g₁.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₁))) (t f₁ hf₁))
eq₂ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂)) =
    (ConcreteCategory.hom (G.obj.map g₂.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₂))) (t f₂ hf₂))
eq₃ :
  (ConcreteCategory.hom (G.obj.map g₁.op))
      ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₁))) (Presheaf.localPreimage f.hom s f₁ hf₁)) =
    (ConcreteCategory.hom (G.obj.map g₁.op)) ((ConcreteCategory.hom (G.obj.map f₁.op)) s)
eq₄ :
  (ConcreteCategory.hom (G.obj.map g₂.op))
      ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₂))) (Presheaf.localPreimage f.hom s f₂ hf₂)) =
    (ConcreteCategory.hom (G.obj.map g₂.op)) ((ConcreteCategory.hom (G.obj.map f₂.op)) s)
⊢ (ConcreteCategory.hom (G.obj.map g₁.op)) ((ConcreteCategory.hom (G.obj.map f₁.op)) s) =
    (ConcreteCategory.hom (G.obj.map g₂.op)) ((ConcreteCategory.hom (G.obj.map f₂.op)) s)