-- Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
theorem eq_of_locally_eq' (V : Opens X) (iUV : ∀ i : ι, U i ⟶ V) (hcover : V ≤ iSup U)
    (s t : ToType (F.1.obj (op V))) (h : ∀ i, F.1.map (iUV i).op s = F.1.map (iUV i).op t) :
    s = t

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
⊢ (ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) t

Tactic:
apply eq_of_locally_eq

Result:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
⊢ ∀ (i : ι),
    (ConcreteCategory.hom (F.val.map (leSupr U i).op)) ((ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) s) =
      (ConcreteCategory.hom (F.val.map (leSupr U i).op)) ((ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) t)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
⊢ s = t

Tactic:
suffices F.1.map (eqToHom V_eq_supr_U.symm).op s = F.1.map (eqToHom V_eq_supr_U.symm).op t by
  convert congr_arg (F.1.map (eqToHom V_eq_supr_U).op) this <;>
  rw [← ConcreteCategory.comp_apply, ← F.1.map_comp, eqToHom_op, eqToHom_op, eqToHom_trans,
    eqToHom_refl, F.1.map_id, ConcreteCategory.id_apply]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
⊢ (ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) t

Proof state:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
i : ι
⊢ (ConcreteCategory.hom (F.val.map (leSupr U i).op)) ((ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) s) =
    (ConcreteCategory.hom (F.val.map (leSupr U i).op)) ((ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) t)

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, ← F.1.map_comp]

Result:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
i : ι
⊢ (ConcreteCategory.hom (F.val.map ((eqToHom ⋯).op ≫ (leSupr U i).op))) s =
    (ConcreteCategory.hom (F.val.map ((eqToHom ⋯).op ≫ (leSupr U i).op))) t

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) t
⊢ s = t

Tactic:
convert congr_arg (F.1.map (eqToHom V_eq_supr_U).op) this <;>
rw [← ConcreteCategory.comp_apply, ← F.1.map_comp, eqToHom_op, eqToHom_op, eqToHom_trans,
  eqToHom_refl, F.1.map_id, ConcreteCategory.id_apply]

Result:
no goals

Proof state:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
⊢ ∀ (i : ι),
    (ConcreteCategory.hom (F.val.map (leSupr U i).op)) ((ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) s) =
      (ConcreteCategory.hom (F.val.map (leSupr U i).op)) ((ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) t)

Tactic:
intro i

Result:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.val.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = (ConcreteCategory.hom (F.val.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
i : ι
⊢ (ConcreteCategory.hom (F.val.map (leSupr U i).op)) ((ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) s) =
    (ConcreteCategory.hom (F.val.map (leSupr U i).op)) ((ConcreteCategory.hom (F.val.map (eqToHom ⋯).op)) t)