-- Lean 4 proof step from Mathlib.Topology.Sheaves.Stalks (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst_2 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
F : Presheaf C X
U V : Opens (↑X : Type v)
x : (↑X : Type v)
hxU : x ∈ U
hxV : x ∈ V
W : Opens (↑X : Type v)
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (FC := FC) (CC := CC) (F.obj (op U))
sV : ToType (FC := FC) (CC := CC) (F.obj (op V))
ih :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) sU :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) sV :
      CC (F.obj (op W)))
rw :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op U))) → CC (F.stalk x))
        sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) sV :
      CC (F.stalk x))
rw₁ :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op U))) → CC (F.stalk x))
        sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op V))) → CC (F.stalk x))
        sV :
      CC (F.stalk x))
rw₂ :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) sU :
          CC (F.obj (op W))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op ≫ F.germ W x hxW) :
          (a : CC (F.obj (op V))) → CC (F.stalk x))
        sV :
      CC (F.stalk x))
rw₃ :
  Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W))) sU :
          CC (F.obj (op W))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) sV :
          CC (F.obj (op W))) :
      CC (F.stalk x))
⊢ Eq (α := CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hxU) : (a : CC (F.obj (op U))) → CC (F.stalk x)) sU :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V x hxV) : (a : CC (F.obj (op V))) → CC (F.stalk x)) sV :
      CC (F.stalk x))
have rw₄ : Eq (α := CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) sV :
        CC (F.obj (op W))) :
    CC (F.stalk x))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ W x hxW) : (a : CC (F.obj (op W))) → CC (F.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map iWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) sV :
        CC (F.obj (op W))) :
    CC (F.stalk x))
Tactic: rw [← F.germ_res iWU x hxW, ← F.germ_res iWV x hxW, ConcreteCategory.comp_apply,
    ConcreteCategory.comp_apply, ih]