-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : (↑X : Type v)
hy : y ∈ U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
⊢ Eq (α := ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
    ((fun (s : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)) ↦
        ((Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ U) ((↑s : F.EtaleSpace).base (CC := CC) (FC := FC)) ⋯,
            WithTopology.toTopology ⊥
              ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
                (surjInv ⋯ ((↑s : F.EtaleSpace).germ (CC := CC) (FC := FC))))) :
          ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))))
      ((fun (x_1 : ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))) ↦
          (match (motive :=
              ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)) →
                (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v))
              x_1 with
            | (⟨y, hy⟩, WithTopology.toTopology .(⊥) g) =>
              Subtype.mk (p := fun (x : F.EtaleSpace (CC := CC) (FC := FC)) ↦
                Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
                  (base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) x)
                (mk (CC := CC) (FC := FC) y
                  ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hy) :
                      (a : CC (F.obj (op U))) → CC (F.stalk y))
                    (surjInv ⋯ g)))
                hy :
            (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)))
        (Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ U) y hy, WithTopology.toTopology ⊥ g)))
    (Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ U) y hy, WithTopology.toTopology ⊥ g)
have simp : Eq (α := ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
  ((Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ U) y sorry,
      WithTopology.toTopology ⊥
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
          (surjInv (β := CC (F.stalk y)) (f :=
            ((⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y sorry)) : (a : CC (F.obj (op U))) → CC (F.stalk y)) :
              (a : CC (F.obj (op U))) → CC (F.stalk y)))
            sorry
            ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hy) : (a : CC (F.obj (op U))) → CC (F.stalk y))
                (surjInv sorry g) :
              CC (F.stalk y))))) :
    ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
  ((Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ U) y hy, WithTopology.toTopology ⊥ g) :
    ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
Tactic: simp only