awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst_1 : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_2 : IsCofiltered I
inst_3 : ∀ (i : I), IsAffine.{u} (D.obj i)
R : CommRingCat
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
inst_4 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_5 : IsAffine.{u} (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst_6 : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine.{u} (D.obj i)]
    (t : D ⟶ Functor.obj (Functor.const I) (Spec R)) (a : c.pt ⟶ Spec S)
    (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ))
    (hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec),
    ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst_7 : ∀ (i : I), IsIso (e.app i)
inst_8 : IsIso e
inst : ∀ (i : I), IsAffine.{u} ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
i : I
g : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i ⟶ Spec S
hg : ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ g = a
hg' : g ≫ Spec.map φ = (inv e ≫ t).app i
⊢ ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i

Tactic:
exact ⟨i, e.app i ≫ g, by rwa [← Category.assoc], by simp [hg']⟩
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} (D.obj i)
t : D ⟶ Functor.obj (Functor.const I) (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
hD : ∃ (D' : I ⥤ CommRingCatᵒᵖ), D = D' ⋙ Scheme.Spec
obtain :
  ∀ (D : I ⥤ CommRingCatᵒᵖ) (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c)
    [∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)] (t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R))
    (a : c.pt ⟶ Spec S) (ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)),
    ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ Spec S), c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i

Tactic:
obtain ⟨D, rfl⟩ := hD

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
⊢ ∀ {X Y : I} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) X ⟶
        Functor.obj (Functor.obj (Functor.const I) (Spec R)) Y)
      (CategoryTheory.Functor.map (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) f ≫
        Iso.hom
          ((fun (x : I) ↦
              (Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x) :
                Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x ≅
                  Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x))
            Y))
      (Iso.hom
          ((fun (x : I) ↦
              (Iso.refl (Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x) :
                Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x ≅
                  Functor.obj (Functor.rightOp (Functor.obj (Functor.const Iᵒᵖ) R) ⋙ Scheme.Spec) x))
            X) ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const I) (Spec R)) f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
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)) ⋯
x x_1 : Iᵒᵖ
f : x ⟶ x_1
⊢ Eq (α := Spec (D.leftOp.obj x_1) ⟶ Spec (Functor.obj (Functor.obj (Functor.const Iᵒᵖ) R) x))
    (Spec.map
      (CategoryTheory.Functor.map (Functor.obj (Functor.const Iᵒᵖ) R) f ≫
        (fun (i : Iᵒᵖ) ↦
            (Spec.preimage (t.app (Opposite.unop i)) :
              Functor.obj (Functor.obj (Functor.const Iᵒᵖ) R) i ⟶ D.leftOp.obj i))
          x_1))
    (Spec.map
      ((fun (i : Iᵒᵖ) ↦
            (Spec.preimage (t.app (Opposite.unop i)) :
              Functor.obj (Functor.obj (Functor.const Iᵒᵖ) R) i ⟶ D.leftOp.obj i))
          x ≫
        D.leftOp.map f))

Tactic:
simpa using (t.naturality f.unop).symm

Premises used: Quiver.Hom.unop, CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
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)) ⋯
w :
  ∀ (x : I),
    t.app x =
      NatTrans.app
        (Functor.whiskerRight
            (NatTrans.rightOp { app := fun (i : Iᵒᵖ) ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := ⋯ })
            Scheme.Spec ≫
          e.hom)
        x
⊢ t =
    Functor.whiskerRight
        (NatTrans.rightOp { app := fun (i : Iᵒᵖ) ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := ⋯ })
        Scheme.Spec ≫
      e.hom

Tactic:
ext : 2
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
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)) ⋯
x : I
⊢ t.app x =
    NatTrans.app
      (Functor.whiskerRight
          (NatTrans.rightOp { app := fun (i : Iᵒᵖ) ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := ⋯ })
          Scheme.Spec ≫
        e.hom)
      x

Tactic:
simp [e]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ Functor.obj (Functor.const I) (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
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)) ⋯
obtain :
  ∀ (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 φ)),
    ∃ (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 φ = t.app i

Tactic:
obtain ⟨t, rfl⟩ : ∃ t' : (Functor.const Iᵒᵖ).obj R ⟶ D.leftOp,
      t = Functor.whiskerRight (NatTrans.rightOp t') Scheme.Spec ≫ e.hom :=
    ⟨⟨fun i ↦ Spec.preimage (t.app i.unop), fun _ _ f ↦ Spec.map_injective
      (by simpa using (t.naturality f.unop).symm)⟩, by ext : 2; simp [e]⟩

Premises used: Opposite, CategoryTheory.Functor.const, CategoryTheory.Functor.leftOp, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (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 φ)
inr :
  ∀
    (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')),
    ∃ (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
wlog :
  ∀ (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
⊢ ∃ (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:
wlog hc' : ∃ c' : Cocone D.leftOp, c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c') generalizing c

Premises used: CategoryTheory.Limits.Cocone, CategoryTheory.Functor.leftOp
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (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')
⊢ IsAffine.{u} c.pt

Tactic:
have inst : IsAffine c.pt := isAffine_of_isLimit _ hc
-- 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 : 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))
⊢ ∀ (i : Iᵒᵖ), IsAffine.{u} (Spec (Opposite.unop (D.obj (Opposite.unop i))))

Tactic:
infer_instance
-- 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 : 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))
⊢ ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop ((D ⋙ Scheme.Spec).op.obj i))

Tactic:
have inst : ∀ i, IsAffine ((D ⋙ Scheme.Spec).op.obj i).unop := by dsimp; infer_instance
-- 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))
w :
  ∀ (i : I),
    ((Scheme.Spec.mapCone c').π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i =
      NatTrans.app (CategoryTheory.Functor.map (Functor.const I) ((Iso.inv c.pt.isoSpec ≫ a) ≫ Spec.map φ)) i
⊢ (Scheme.Spec.mapCone c').π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) ((Iso.inv c.pt.isoSpec ≫ a) ≫ Spec.map φ)

Tactic:
ext i
-- 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))
i : I
⊢ c.π.app i ≫ Spec.map (t.app (Opposite.op i)) = a ≫ Spec.map φ

Tactic:
simpa using congr((($ha).app i))
-- 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))
i : I
⊢ c.π.app i ≫ Spec.map (t.app (Opposite.op i)) = a ≫ Spec.map φ

Tactic:
have : c.π.app i ≫ Spec.map (t.app (.op i)) = a ≫ Spec.map φ := by
          simpa using congr((($ha).app i))