-- 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:
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)

Tactic:
rw [reassoc_of% eq]

Result:
no goals

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:
apply hF.hom_ext ⟨_, G.cover_lift J K (K.pullback_stable j.hom.unop S.2)⟩

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
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback G (Sieve.pullback j.hom.unop ↑S), ⋯⟩),
    (f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map I.f.op =
      (g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map I.f.op

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
⊢ (f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map { Y := W, f := i, hf := hi }.f.op =
    (g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map { Y := W, f := i, hf := hi }.f.op

Tactic:
have eq := h (GrothendieckTopology.Cover.Arrow.mk _ (G.map i ≫ j.hom.unop) hi)

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 { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi }.f.op =
    g ≫ R.map { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi }.f.op
⊢ (f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map { Y := W, f := i, hf := hi }.f.op =
    (g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map { Y := W, f := i, hf := hi }.f.op

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 { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi }.f.op =
    g ≫ R.map { Y := G.obj W, f := G.map i ≫ j.hom.unop, hf := hi }.f.op
⊢ (f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map { Y := W, f := i, hf := hi }.f.op =
    (g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map { Y := W, f := i, hf := hi }.f.op

Tactic:
dsimp at eq ⊢

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 ≫ α.app j.right) ≫ F.map i.op = (g ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op

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
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback G (Sieve.pullback j.hom.unop ↑S), ⋯⟩),
    (f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map I.f.op =
      (g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map I.f.op

Tactic:
intro ⟨W, i, hi⟩

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
⊢ (f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map { Y := W, f := i, hf := hi }.f.op =
    (g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map { Y := W, f := i, hf := hi }.f.op