-- Mathlib/Geometry/RingedSpace/SheafedSpace.lean
lemma hom_stalk_ext {X Y : SheafedSpace C} (f g : X ⟶ Y) (h : f.base = g.base)
    (h' : ∀ x, f.stalkMap x = (Y.presheaf.stalkCongr (h ▸ rfl)).hom ≫ g.stalkMap x) :
    f = g

Proof state:
case mk.mk.e_c.w.h.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)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    { base := f, c := fc }.stalkMap x = (Y.presheaf.stalkCongr ⋯).hom ≫ { base := f, c := gc }.stalkMap x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ (Opens.map f).obj (unop (op U))
⊢ (ConcreteCategory.hom (X.presheaf.germ ((Opens.map f).obj (unop (op U))) x hx))
      ((ConcreteCategory.hom (fc.app (op U))) s) =
    (ConcreteCategory.hom (X.presheaf.germ ((Opens.map f).obj (unop (op U))) x hx))
      ((ConcreteCategory.hom (gc.app (op U))) s)

Tactic:
erw [← PresheafedSpace.stalkMap_germ_apply ⟨f, fc⟩, ← PresheafedSpace.stalkMap_germ_apply ⟨f, gc⟩]

Result:
case mk.mk.e_c.w.h.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)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    { base := f, c := fc }.stalkMap x = (Y.presheaf.stalkCongr ⋯).hom ≫ { base := f, c := gc }.stalkMap x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ (Opens.map f).obj (unop (op U))
⊢ (ConcreteCategory.hom ({ base := f, c := fc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := fc }.base) x) hx))
        s) =
    (ConcreteCategory.hom ({ base := f, c := gc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := gc }.base) x) hx))
        s)

Proof state:
case mk
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)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
g : X ⟶ Y
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h : { base := f, c := fc }.base = g.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    { base := f, c := fc }.stalkMap x = (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap g x
⊢ { base := f, c := fc } = g

Tactic:
obtain ⟨g, gc⟩ := g

Result:
case mk.mk
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)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
g : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
gc : Y.presheaf ⟶ (pushforward C g).obj X.presheaf
h : { base := f, c := fc }.base = { base := g, c := gc }.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    { base := f, c := fc }.stalkMap x = (Y.presheaf.stalkCongr ⋯).hom ≫ { base := g, c := gc }.stalkMap x
⊢ { base := f, c := fc } = { base := g, c := gc }

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)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f g : X ⟶ Y
h : f.base = g.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap f x = (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap g x
⊢ f = g

Tactic:
obtain ⟨f, fc⟩ := f

Result:
case mk
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)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
g : X ⟶ Y
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h : { base := f, c := fc }.base = g.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    { base := f, c := fc }.stalkMap x = (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap g x
⊢ { base := f, c := fc } = g

Proof state:
case mk.mk.e_c
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)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    { base := f, c := fc }.stalkMap x = (Y.presheaf.stalkCongr ⋯).hom ≫ { base := f, c := gc }.stalkMap x
⊢ fc = gc

Tactic:
ext U s

Result:
case mk.mk.e_c.w.h.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)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    { base := f, c := fc }.stalkMap x = (Y.presheaf.stalkCongr ⋯).hom ≫ { base := f, c := gc }.stalkMap x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (fc.app (op U))) s = (ConcreteCategory.hom (gc.app (op U))) s