-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
S : Scheme
J : Type u_1
inst_2 : Category.{v_1, u_1} J
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
𝒰 : OpenCover.{u_2, u} S
inst_3 : Category.{v_2, u_2} 𝒰.I₀
inst_4 : LocallyDirected.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰
d : ColimitGluingData.{v_2, u, v_1, u_1, u_2} (P := P) D 𝒰
inst_5 :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
    PreservesColimitsOfShape.{v_1, u_1, u, u, u + 1, u + 1} (C := P.Over ⊤ (𝒰.X j)) J
      (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
inst_6 : Quiver.IsThin.{u_2, v_2} 𝒰.I₀
inst_7 : Small.{u, u_2} 𝒰.I₀
inst_8 : IsZariskiLocalAtTarget P
a : J
i : 𝒰.I₀
⊢ Eq (α :=
    pullback (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ⟶
      (Functor.obj.{v_1, u, u_1, u + 1} (Functor.obj (Functor.const J) (d.glued (P := P))) a).toComma (P := P) (Q := ⊤)
          (W := ⊤).left)
    (pullback.fst (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ≫
      CommaMorphism.left
        (OpenCover.glueMorphismsOverOfLocallyDirected
          (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰)
          (fun (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰).I₀) ↦
            ((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
              colimit.ι d.relativeGluingData (P := P).functor i)
          ⋯ ⋯))
    (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i)
have generalize_proofs : ∀ (pf : IsMultiplicative.{u, u + 1} (C := Scheme) ⊤) (pf_1 : IsMultiplicative (C := Discrete PUnit.{1}) ⊤)
  (pf_2 : HasPullback (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
  (pf_3 : (precoverage IsOpenImmersion).IsStableUnderBaseChange)
  (pf_4 : ∀ (i : 𝒰.I₀), HasPullback (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
  (pf_5 : ∀ (i : 𝒰.I₀), HasPullback (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
  (pf_6 :
    ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰).I₀),
      P.HasPullbacksAlong (𝒰.f i))
  (pf_7 :
    ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰).I₀),
      P.IsStableUnderBaseChangeAlong (𝒰.f i))
  (pf_8 : IsStableUnderBaseChange.{u, u + 1} (C := Scheme) ⊤) (pf_9 : HasColimit d.relativeGluingData (P := P).functor)
  (pf_10 :
    ∀ {j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰).I₀},
      P.HasPullbacksAlong (𝒰.f j))
  (pf_11 :
    ∀ {j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰).I₀},
      P.IsStableUnderBaseChangeAlong (𝒰.f j))
  (h1 :
    ∀ {i j : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰).I₀}
      (hij : i ⟶ j),
      Eq (α :=
        (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰).X i ⟶
          Over.left
            ((Functor.obj.{v_1, u, u_1, u + 1} (Functor.obj (Functor.const J) (d.glued (P := P))) a).toComma (P := P)
              (Q := ⊤) (W := ⊤)))
        (Cover.trans (P := IsOpenImmersion)
            (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰) hij ≫
          ((d.cocone (P := P) j).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
            colimit.ι d.relativeGluingData (P := P).functor j)
        (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
          colimit.ι d.relativeGluingData (P := P).functor i))
  (h2 :
    ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰).I₀),
      (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
            colimit.ι d.relativeGluingData (P := P).functor i) ≫
          Over.hom
            ((Functor.obj.{v_1, u, u_1, u + 1} (Functor.obj (Functor.const J) (d.glued (P := P))) a).toComma (P := P)
              (Q := ⊤) (W := ⊤)) =
        (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰).f i ≫
          Over.hom ((D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤)))
  (pf_12 : P.HasPullbacksAlong (𝒰.f i)) (pf_13 : P.IsStableUnderBaseChangeAlong (𝒰.f i)),
  pullback.fst (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ≫
      (OpenCover.glueMorphismsOverOfLocallyDirected
          (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰)
          (fun (i : (Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰).I₀) ↦
            ((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
              colimit.ι d.relativeGluingData (P := P).functor i)
          (@h1) h2).left =
    ((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i
Tactic: generalize_proofs _ _ _ _ _ _ _ _ _ _ _ _ h1 h2