-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst_1 : Category.{u, u} I
inst_2 : IsCofiltered I
R : CommRingCat
inst_3 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_4 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_5 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
e : Iso (C := I ⥤ Scheme) (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec)
  (Functor.obj (Functor.const I) (Spec R)) :=
  NatIso.ofComponents
    (fun (x : I) ↦ Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x)) ⋯
t : Functor.obj (Functor.const Iᵒᵖ) R ⟶ D.leftOp
ha :
  c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S)
    (ha :
      c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
        CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hc' : ∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')),
    ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
      c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
hc' : ¬∃ (c' : Cocone D.leftOp), c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')
inst_7 : IsAffine.{u} c.pt
e' : (D ⋙ Scheme.Spec).op ⋙ Γ ≅ D.leftOp := D.leftOp.isoWhiskerLeft SpecΓIdentity
c' : Cone D := coneOfCoconeLeftOp ((Cocone.precompose e'.inv).obj (Γ.mapCocone c.op))
inst : ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop ((D ⋙ Scheme.Spec).op.obj i))
inr :
  ∀ (i : I) (f : (D ⋙ Scheme.Spec).obj i ⟶ Spec S)
    (hf :
      (Scheme.Spec.mapCone c').π.app i ≫ f = Iso.inv c.pt.isoSpec ≫ a ∧
        f ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i),
    ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
      c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
⊢ ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i

Tactic:
obtain ⟨i, f, hf⟩ := this (Scheme.Spec.mapCone c') (isLimitOfPreserves _
      (isLimitConeOfCoconeLeftOp _ ((IsColimit.precomposeHomEquiv e'.symm _).symm
        (isColimitOfPreserves _ hc.op)))) (c.pt.isoSpec.inv ≫ a) (by
        ext i
        have : c.π.app i ≫ Spec.map (t.app (.op i)) = a ≫ Spec.map φ := by
          simpa using congr((($ha).app i))
        simp [c', e, e', ← this, Iso.eq_inv_comp, isoSpec_hom_naturality_assoc]) ⟨_, rfl⟩

Premises used: CategoryTheory.Limits.IsLimit.op, AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.Limits.isLimitConeOfCoconeLeftOp, AlgebraicGeometry.Scheme.Spec, CategoryTheory.Limits.Cone.pt, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.mapCone, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Iso.inv, CategoryTheory.Limits.IsColimit.precomposeHomEquiv, CategoryTheory.Limits.isColimitOfPreserves, rfl