-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have refine : ∀
  (x :
    (MultispanShape.prod
        (Cover.gluedCover (X :=
              (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                Scheme))
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange
                    (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.J).R)
  (k : ↥(F.obj ↓i))
  (hk :
    Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
      (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
      k),
  Eq (α :=
    (Cover.gluedCover (X :=
                (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                  Scheme))
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange
                      (F.map
                        i_1.snd (β := fun (k : J) ↦
                            (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram.right
        (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
          Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
            (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
            x)
          k hk) ⟶
      s.pt)
    (Multicoequalizer.π
        (Cover.gluedCover (X :=
              (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                Scheme))
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange
                    (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram
        (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
          Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
            (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
            x)
          k hk) ≫
      Iso.inv
          (Cover.gluedCover (X :=
              (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                Scheme))
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).isoLocallyRingedSpace ≫
        Hom.toLRSHom
            (Cover.fromGlued
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))) ≫
          Hom.toLRSHom (Opens.ι (V F (↓i) ↓j)) ≫ s.ι.app ↓i)
    (CategoryStruct.comp (Y :=
      multicoequalizer
        (Cover.gluedCover (X :=
              (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                Scheme))
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange
                    (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram)
      (Multicoequalizer.π
          (Cover.gluedCover (X :=
                (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                  Scheme))
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange
                      (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram
          (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
            Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
              (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
              x)
            k hk) :
        (Cover.gluedCover (X :=
                    (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                      Scheme))
                    (Cover.ulift (P := IsOpenImmersion)
                      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                        Hom.opensRange
                          (F.map
                            i_1.snd (β := fun (k : J) ↦
                                (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram.right
            (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
              Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                x)
              k hk) ⟶
          multicoequalizer
            (Cover.gluedCover (X :=
                  (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                    Scheme))
                  (Cover.ulift (P := IsOpenImmersion)
                    (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                      Hom.opensRange
                        (F.map
                          i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram)
      (Iso.inv
            (Cover.gluedCover (X :=
                (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                  Scheme))
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).isoLocallyRingedSpace ≫
          Hom.toLRSHom
              (Cover.fromGlued
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))) ≫
            Hom.toLRSHom (tAux F (↓i) ↓j) ≫ s.ι.app ↓j :
        (Cover.gluedCover (X :=
                (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                  Scheme))
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange
                      (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.glued ⟶
          s.pt))
Tactic: refine Multicoequalizer.hom_ext _ _ _ fun ⟨k, hk⟩ ↦ ?_