-- 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)
inst_3 : PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
inst_4 : HasLimits.{v, u} C
inst_5 : PreservesLimits (forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (forget C (FC := FC) (CC := CC))
F : Sheaf C X
U : Opens (↑X : Type v)
s t :
  ToType (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op U))
h :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Eq (α := CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          s :
        CC (F.presheaf.stalk x))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.germ U x hx) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.stalk x))
          t :
        CC (F.presheaf.stalk x))
V : (x : ↥U) → Opens (↑X : Type v)
m : ∀ (x : ↥U), (↑x : (↑X : Type v)) ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U),
    Eq (α := CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₁ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          s :
        CC (F.presheaf.obj (op (V x))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
            (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
          t :
        CC (F.presheaf.obj (op (V x))))
x : ↥U
⊢ Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (i₁ x).op) :
          (a : CC (F.obj.obj (op U))) → CC (F.obj.obj (op (V x))))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (i₁ x).op) :
          (a : CC (F.obj.obj (op U))) → CC (F.obj.obj (op (V x))))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
have h₁ : Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.presheaf.map (i₂ x).op) :
        (a : CC (F.presheaf.obj (op U))) → CC (F.presheaf.obj (op (V x))))
      t :
    CC (F.presheaf.obj (op (V x))))
  ((ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map (i₁ x).op) :
        (a : CC (F.obj.obj (op U))) → CC (F.obj.obj (op (V x))))
      t :
    CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).obj (op (V x))))
Tactic: rw [heq, Subsingleton.elim (i₁ x) (i₂ x)]