-- Mathlib/CategoryTheory/Sites/Sheaf.lean
lemma IsSheaf.hom_ext_ofArrows
    {P : Cᵒᵖ ⥤ A} (hP : Presheaf.IsSheaf J P) {I : Type*} {S : C} {X : I → C}
    (f : ∀ i, X i ⟶ S) (hf : Sieve.ofArrows _ f ∈ J S) {E : A}
    {x y : E ⟶ P.obj (op S)} (h : ∀ i, x ≫ P.map (f i).op = y ≫ P.map (f i).op) :
    x = y

Proof state:
case h.mk.intro.intro.intro.intro.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ x ≫ P.map ((f i).op ≫ g.op) = y ≫ P.map ((f i).op ≫ g.op)

Tactic:
rw [P.map_comp, reassoc_of% (h i)]

Result:
no goals

Proof state:
case h.mk.intro.intro.intro.intro.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ x ≫ P.map { Y := Z, f := g ≫ f i, hf := ⋯ }.f.op = y ≫ P.map { Y := Z, f := g ≫ f i, hf := ⋯ }.f.op

Tactic:
dsimp

Result:
case h.mk.intro.intro.intro.intro.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ x ≫ P.map ((f i).op ≫ g.op) = y ≫ P.map ((f i).op ≫ g.op)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
⊢ ∀ (I_1 : GrothendieckTopology.Cover.Arrow ⟨ofArrows X f, hf⟩), x ≫ P.map I_1.f.op = y ≫ P.map I_1.f.op

Tactic:
rintro ⟨Z, _, _, g, _, ⟨i⟩, rfl⟩

Result:
case h.mk.intro.intro.intro.intro.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ x ≫ P.map { Y := Z, f := g ≫ f i, hf := ⋯ }.f.op = y ≫ P.map { Y := Z, f := g ≫ f i, hf := ⋯ }.f.op

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
⊢ x = y

Tactic:
apply hP.hom_ext ⟨_, hf⟩

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
⊢ ∀ (I_1 : GrothendieckTopology.Cover.Arrow ⟨ofArrows X f, hf⟩), x ≫ P.map I_1.f.op = y ≫ P.map I_1.f.op