awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
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
⊢ ((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
have this₁ : 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))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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) (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
have 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
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⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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
have inr : c.π.app i ≫ f = a ∧ f ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
Tactic: refine ⟨i, f, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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')
⊢ ∃ (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
have 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
Tactic: obtain ⟨c', rfl⟩ := hc'
Cleared hypotheses: c, hc, a, ha, hc'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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 φ)
⊢ ∃ (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
have 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
Tactic: obtain ⟨ψ, rfl⟩ := Spec.map_surjective a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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 φ)
⊢ ∃ (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
have 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
Tactic: replace hc := isColimitOfConeOfCoconeLeftOp _ (isLimitOfReflects _ hc)
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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ᵒᵖ
⊢ φ ≫ ψ = t.app i ≫ c'.ι.app i
have a : Spec.map (φ ≫ ψ) = Spec.map (t.app i ≫ c'.ι.app i)
Tactic: apply Spec.map_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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 : (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
have 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
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
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)
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
have 𝒰 : 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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (hypothesis)
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}
⊢ IsFinite (X.fromSpecResidueField x ≫ f)
have hx₁ : IsClosedImmersion (X.fromSpecResidueField x)
Tactic: rw [isClosed_singleton_iff_isClosedImmersion] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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 : IsClosedImmersion (X.fromSpecResidueField x)
⊢ IsFinite (X.fromSpecResidueField x ≫ f)
have rw : LocallyOfFiniteType (X.fromSpecResidueField x ≫ f)
Tactic: rw [isFinite_iff_locallyOfFiniteType_of_jacobsonSpace]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (hypothesis)
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}
⊢ IsIso (Spec.preimage (X.fromSpecResidueField x ≫ f))
have this : IsFinite (X.fromSpecResidueField x ≫ f)
Tactic: have : IsFinite (X.fromSpecResidueField x ≫ f) := by
      rw [isClosed_singleton_iff_isClosedImmersion] at hx
      rw [isFinite_iff_locallyOfFiniteType_of_jacobsonSpace]
      infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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}
this : IsFinite (X.fromSpecResidueField x ≫ f)
⊢ IsIso (Spec.preimage (X.fromSpecResidueField x ≫ f))
have rw : Function.Bijective (α := (↑(CommRingCat.of K) : Type u)) (β := (↑(X.residueField x) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (Spec.preimage (X.fromSpecResidueField x ≫ f))) :
    (a : (↑(CommRingCat.of K) : Type u)) → (↑(X.residueField x) : Type u))
Tactic: rw [ConcreteCategory.isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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}
this : IsFinite (X.fromSpecResidueField x ≫ f)
⊢ Function.Bijective (α := (↑(CommRingCat.of K) : Type u)) (β := (↑(X.residueField x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Spec.preimage (X.fromSpecResidueField x ≫ f))) :
      (a : (↑(CommRingCat.of K) : Type u)) → (↑(X.residueField x) : Type u))
have refine : (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
    (Spec.preimage (X.fromSpecResidueField x ≫ f))).IsIntegral
Tactic: refine IsAlgClosed.ringHom_bijective_of_isIntegral _ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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}
this : IsFinite (X.fromSpecResidueField x ≫ f)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) (Spec.preimage (X.fromSpecResidueField x ≫ f))).IsIntegral
have rw : IsIntegralHom (X.fromSpecResidueField x ≫ f)
Tactic: rw [← IsIntegralHom.SpecMap_iff, Spec.map_preimage]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (hypothesis)
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}
p : { p : Spec (CommRingCat.of K) ⟶ X // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) (closedPoints ↥X)
    ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X)
have this : IsClosedImmersion (↑p : Spec (CommRingCat.of K) ⟶ X)
Tactic: have := isClosedImmersion_of_comp_eq_id _ _ p.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (hypothesis)
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}
p : { p : Spec (CommRingCat.of K) ⟶ X // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
this : IsClosedImmersion (↑p : Spec (CommRingCat.of K) ⟶ X)
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) (closedPoints ↥X)
    ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X)
have this₁ : IsClosed (X := ↥X) (Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑(↑p : Spec (CommRingCat.of K) ⟶ X))
Tactic: have := p.1.isClosedEmbedding.isClosed_range
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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}
p : { p : Spec (CommRingCat.of K) ⟶ X // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
this_1 : IsClosedImmersion (↑p : Spec (CommRingCat.of K) ⟶ X)
this : IsClosed (X := ↥X) (Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑(↑p : Spec (CommRingCat.of K) ⟶ X))
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) (closedPoints ↥X)
    ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X)
have rwa : ∀ (x : ↥(Spec (CommRingCat.of K))),
  Eq (α := ↥X) ((↑p : Spec (CommRingCat.of K) ⟶ X) x : ↥X)
    ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X)
Tactic: rwa [Set.range_eq_singleton] at this