-- 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
g : F.EtaleSpace (CC := CC) (FC := FC)
hg :
  Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
    (base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) g
f : CC (F.obj (op U))
hf :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (g.base (CC := CC) (FC := FC)) hg) :
        (a : CC (F.obj (op U))) → CC (F.stalk g.base))
      f =
    g.germ (CC := CC) (FC := FC)
g' : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)
hgU : (↑g' : F.EtaleSpace).base (CC := CC) (FC := FC) ∈ U
hgf :
  (↑g' : F.EtaleSpace).germ (CC := CC) (FC := FC) =
    (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U ((↑g' : F.EtaleSpace).base (CC := CC) (FC := FC)) hgU) :
        (a : CC (F.obj (op U))) → CC (F.stalk (↑g' : F.EtaleSpace).base))
      f
h :
  Eq (α := ToType (FC := FC) (CC := 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))
        (surjInv ⋯
          ((ConcreteCategory.hom (FC := FC) (CC := CC)
                (F.germ U ((↑g' : F.EtaleSpace).base (CC := CC) (FC := FC)) hgU) :
              (a : CC (F.obj (op U))) → CC (F.stalk (↑g' : F.EtaleSpace).base))
            f)) :
      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))
        (surjInv ⋯ (g.germ (CC := CC) (FC := FC))) :
      CC (F.stalk x))
⊢ Eq (α := ToType (FC := FC) (CC := 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))
        (surjInv ⋯ ((↑g' : F.EtaleSpace).germ (CC := CC) (FC := FC))) :
      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))
        (surjInv ⋯ (g.germ (CC := CC) (FC := FC))) :
      CC (F.stalk x))
have h₁ : Eq (α := ToType (FC := FC) (CC := 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))
      (surjInv sorry
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U ((↑g' : F.EtaleSpace).base (CC := CC) (FC := FC)) hgU) :
            (a : CC (F.obj (op U))) → CC (F.stalk (↑g' : F.EtaleSpace).base))
          f)) :
    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))
      (surjInv sorry
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (g.base (CC := CC) (FC := FC)) hg) :
            (a : CC (F.obj (op U))) → CC (F.stalk g.base))
          f)) :
    CC (F.stalk x))
Tactic: rw [hgf, ← hf, leftInverse_surjInv (hF_bij _ _), leftInverse_surjInv (hF_bij _ _)]