-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
lemma hom_ext {W : A} {f g : W ⟶ R.obj (op X)}
    (h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op) : f = g

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.43558, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W : A
f g : W ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
⊢ ∀ (j : StructuredArrow (op X) G.op),
    f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j =
      g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j

Tactic:
intro j

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.43558, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W : A
f g : W ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
⊢ f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j =
    g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.43558, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W : A
f g : W ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
⊢ f = g

Tactic:
apply (hR (op X)).hom_ext

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.43558, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W : A
f g : W ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
⊢ ∀ (j : StructuredArrow (op X) G.op),
    f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j =
      g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.43558, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W✝ : A
f g : W✝ ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi : (↑⟨Sieve.functorPullback G (Sieve.pullback j.hom.unop ↑S), ⋯⟩).arrows i
eq : f ≫ R.map (j.hom ≫ (G.map i).op) = g ≫ R.map (j.hom ≫ (G.map i).op)
⊢ (f ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op = (g ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op

Tactic:
simp only [Category.assoc, ← NatTrans.naturality, Functor.comp_map, ← Functor.map_comp_assoc,
  Functor.op_map, Quiver.Hom.unop_op]

Result:
case h
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.43558, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W✝ : A
f g : W✝ ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi : (↑⟨Sieve.functorPullback G (Sieve.pullback j.hom.unop ↑S), ⋯⟩).arrows i
eq : f ≫ R.map (j.hom ≫ (G.map i).op) = g ≫ R.map (j.hom ≫ (G.map i).op)
⊢ f ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W) = g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W)