-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (hypothesis)
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
x : ↥X
h :
  Eq (α := (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U))
            (Hom.app (𝒰.f (Cover.idx 𝒰 x)) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
        f :
      (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U))
            (Hom.app (𝒰.f (Cover.idx 𝒰 x)) U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
        g :
      (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
⊢ Eq (α :=
    (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
          (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 x)) (𝒰.f (Cover.idx 𝒰 x)) ⊓ U))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj (op U))
            (Y :=
            X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
              (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 x)) (𝒰.f (Cover.idx 𝒰 x)) ⊓ U)))
            (X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(X.sheaf.obj.obj (op U)) : Type u)) →
            (↑(X.sheaf.obj.obj (op (Hom.opensRange (𝒰.f (Cover.idx 𝒰 x)) ⊓ U))) : Type u))
        f :
      (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
            (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 x)) (𝒰.f (Cover.idx 𝒰 x)) ⊓ U))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj (op U))
            (Y :=
            X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
              (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 x)) (𝒰.f (Cover.idx 𝒰 x)) ⊓ U)))
            (X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(X.sheaf.obj.obj (op U)) : Type u)) →
            (↑(X.sheaf.obj.obj (op (Hom.opensRange (𝒰.f (Cover.idx 𝒰 x)) ⊓ U))) : Type u))
        g :
      (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
            (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 x)) (𝒰.f (Cover.idx 𝒰 x)) ⊓ U))) :
        Type u))
have h₁ : Eq (α := (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U))
          (CategoryStruct.comp (Y :=
            X.presheaf.obj (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 x)) (𝒰.f (Cover.idx 𝒰 x)) ⊓ U)))
            (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) (Iso.inv (IsOpenImmersion.ΓIso (𝒰.f (Cover.idx 𝒰 x)) U))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
      f :
    (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U))
          (CategoryStruct.comp (Y :=
            X.presheaf.obj (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 x)) (𝒰.f (Cover.idx 𝒰 x)) ⊓ U)))
            (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) (Iso.inv (IsOpenImmersion.ΓIso (𝒰.f (Cover.idx 𝒰 x)) U))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
      g :
    (↑Γ(𝒰.X (Cover.idx 𝒰 x), 𝒰.f (Cover.idx 𝒰 x) ⁻¹ᵁ U) : Type u))
Tactic: rw [← IsOpenImmersion.map_ΓIso_inv] at h
Cleared hypotheses: h