awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 :
  ∀ (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
this : c.π.app i ≫ Spec.map (t.app (Opposite.op i)) = a ≫ Spec.map φ
⊢ ((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

Tactic:
simp [c', e, e', ← this, Iso.eq_inv_comp, isoSpec_hom_naturality_assoc]

Premises used: AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, CategoryTheory.Iso.eq_inv_comp
-- 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
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

Tactic:
⟨i, f, ?_⟩

Premises used: Exists.intro
-- 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
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
inr : c.π.app i ≫ f = 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

Tactic:
refine ⟨i, f, ?_⟩
-- 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
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
⊢ c.π.app i ≫ f = a ∧ f ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i

Tactic:
simpa [Iso.eq_inv_comp, c', isoSpec_hom_naturality_assoc, e'] using hf

Premises used: AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, CategoryTheory.Iso.eq_inv_comp
-- 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ᵒᵖ
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
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
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')
obtain :
  ∀ (c' : Cocone D.leftOp) (hc : IsLimit (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')))
    (a : (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).pt ⟶ Spec S)
    (ha :
      (Scheme.Spec.mapCone (coneOfCoconeLeftOp 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),
      (Scheme.Spec.mapCone (coneOfCoconeLeftOp 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 ⟨c', rfl⟩ := hc'

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ᵒᵖ
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
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
c' : Cocone D.leftOp
hc : IsLimit (Scheme.Spec.mapCone (coneOfCoconeLeftOp c'))
a : (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).pt ⟶ Spec S
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (a ≫ Spec.map φ)
obtain :
  ∀ (ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt)
    (ha :
      (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
        CategoryTheory.Functor.map (Functor.const I) (Spec.map ψ ≫ Spec.map φ)),
    ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
      (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π.app i ≫ g = Spec.map ψ ∧
        g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
⊢ ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π.app i ≫ g = a ∧
      g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i

Tactic:
obtain ⟨ψ, rfl⟩ := Spec.map_surjective a

Premises used: AlgebraicGeometry.Spec.map_surjective, 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ᵒᵖ
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
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
c' : Cocone D.leftOp
hc : IsLimit (Scheme.Spec.mapCone (coneOfCoconeLeftOp c'))
ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (Spec.map ψ ≫ Spec.map φ)
replace :
  ∀ (hc : IsColimit c'),
    ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
      (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π.app i ≫ g = Spec.map ψ ∧
        g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
⊢ ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π.app i ≫ g = Spec.map ψ ∧
      g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i

Tactic:
replace hc := isColimitOfConeOfCoconeLeftOp _ (isLimitOfReflects _ hc)
-- 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ᵒᵖ
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
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
c' : Cocone D.leftOp
ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (Spec.map ψ ≫ Spec.map φ)
hc : IsColimit c'
i : Iᵒᵖ
a : Spec.map (φ ≫ ψ) = Spec.map (t.app i ≫ c'.ι.app i)
⊢ φ ≫ ψ = t.app i ≫ c'.ι.app i

Tactic:
apply Spec.map_injective

Premises used: AlgebraicGeometry.Spec.map_injective
-- 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ᵒᵖ
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
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
c' : Cocone D.leftOp
ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (Spec.map ψ ≫ Spec.map φ)
hc : IsColimit c'
i : Iᵒᵖ
⊢ Spec.map (φ ≫ ψ) = Spec.map (t.app i ≫ c'.ι.app i)

Tactic:
simpa using congr(($ha).app i.unop).symm

Premises used: congrArg, id, Eq.symm, Opposite.unop, CategoryTheory.NatTrans.app
-- 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ᵒᵖ
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
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
c' : Cocone D.leftOp
ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (Spec.map ψ ≫ Spec.map φ)
hc : IsColimit c'
obtain :
  ∀ (i : Iᵒᵖ) (g : S ⟶ D.leftOp.obj i) (hg : φ ≫ g = t.app i) (hg' : ψ = g ≫ c'.ι.app i),
    ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
      (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π.app i ≫ g = Spec.map ψ ∧
        g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
⊢ ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π.app i ≫ g = Spec.map ψ ∧
      g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i

Tactic:
obtain ⟨i, g, hg, hg'⟩ :=
    RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit _ D.leftOp t _ _ hc
    (HasRingHomProperty.Spec_iff.mp ‹LocallyOfFinitePresentation (Spec.map φ)›) ψ fun i ↦ by
    apply Spec.map_injective; simpa using congr(($ha).app i.unop).symm

Premises used: RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit, AlgebraicGeometry.HasRingHomProperty.Spec_iff, Iff.mp, 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ᵒᵖ
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
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
c' : Cocone D.leftOp
ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (Spec.map ψ ≫ Spec.map φ)
hc : IsColimit c'
i : Iᵒᵖ
g : S ⟶ D.leftOp.obj i
hg : φ ≫ g = t.app i
hg' : ψ = g ≫ c'.ι.app i
⊢ (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π.app (Opposite.unop i) ≫ Spec.map g = Spec.map ψ

Tactic:
simpa using congr(Spec.map $hg').symm

Premises used: congrArg, AlgebraicGeometry.Spec.map, id, 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ᵒᵖ
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
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
c' : Cocone D.leftOp
ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (Spec.map ψ ≫ Spec.map φ)
hc : IsColimit c'
i : Iᵒᵖ
g : S ⟶ D.leftOp.obj i
hg : φ ≫ g = t.app i
hg' : ψ = g ≫ c'.ι.app i
⊢ Spec.map g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app (Opposite.unop i)

Tactic:
simpa using congr(Spec.map $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 ⥤ CommRingCatᵒᵖ
inst_5 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
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
c' : Cocone D.leftOp
ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    CategoryTheory.Functor.map (Functor.const I) (Spec.map ψ ≫ Spec.map φ)
hc : IsColimit c'
i : Iᵒᵖ
g : S ⟶ D.leftOp.obj i
hg : φ ≫ g = t.app i
hg' : ψ = g ≫ c'.ι.app i
⊢ ∃ (i : I) (g : (D ⋙ Scheme.Spec).obj i ⟶ Spec S),
    (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π.app i ≫ g = Spec.map ψ ∧
      g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i

Tactic:
exact ⟨i.unop, Spec.map g, by simpa using congr(Spec.map $hg').symm,
    by simpa using congr(Spec.map $hg)⟩
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : LocallyOfFinitePresentation f
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_5 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
⊢ IsOpenCover (X := ↥c.pt)
    fun
      (V :
        { x :
          TopologicalSpace.Opens ↥c.pt ×
            { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
              x.1 ∈ X.affineOpens ∧
                x.1 ≤
                  (Opens.comap (TopCat.Hom.hom f.base) : (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                    (↑x.2 : TopologicalSpace.Opens ↥S) } //
          Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt)) c.pt.affineOpens x.1 ∧
            x.1 ≤
              (Opens.comap (TopCat.Hom.hom a.base) : (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) ↦
    (↑V :
        TopologicalSpace.Opens ↥c.pt ×
          { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
            x.1 ∈ X.affineOpens ∧
              x.1 ≤
                (Opens.comap (TopCat.Hom.hom f.base) : (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                  (↑x.2 : TopologicalSpace.Opens ↥S) }).1

Tactic:
have 𝒰 := (c.pt.isBasis_affineOpens).isOpenCover_mem_and_le
    (((X.isBasis_affineOpens).isOpenCover_mem_and_le
    ((S.isBasis_affineOpens).isOpenCover.comap f.base.hom)).comap a.base.hom)
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst_2 : LocallyOfFiniteType f
x : ↥X
hx : IsClosed (X := ↥X) {x}
⊢ IsClosedImmersion (X.fromSpecResidueField x)

Tactic:
rw [isClosed_singleton_iff_isClosedImmersion] at hx

Premises used: AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion