awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
⊢ Nonempty.{u + 1} ↥c.pt
have inl : IsEmpty I → Nonempty.{u + 1} ↥c.pt
Tactic: classical
  cases isEmpty_or_nonempty I
  · have e := (isLimitEquivIsTerminalOfIsEmpty _ _ hc).uniqueUpToIso specULiftZIsTerminal
    exact Nonempty.map e.inv inferInstance
  · have i := Nonempty.some ‹Nonempty I›
    have : IsCofiltered I := ⟨⟩
    let 𝒰 := (D.obj i).affineCover.finiteSubcover
    have (i' : _) : IsAffine (𝒰.X i') := inferInstanceAs (IsAffine (Spec _))
    obtain ⟨j, H⟩ :
        ∃ j : 𝒰.I₀, ∀ {i'} (f : i' ⟶ i), Nonempty ((𝒰.pullback₁ (D.map f)).X j) := by
      by_contra! H
      choose i' f hf using H
      let g (j) := IsCofiltered.infTo (insert i (Finset.univ.image i'))
        (Finset.univ.image fun j : 𝒰.I₀ ↦ ⟨_, _, by simp, by simp, f j⟩) (X := j)
      have (j : 𝒰.I₀) : IsEmpty ((𝒰.pullback₁ (D.map (g i (by simp)))).X j) := by
        let F : (𝒰.pullback₁ (D.map (g i (by simp)))).X j ⟶
            (𝒰.pullback₁ (D.map (f j))).X j :=
          pullback.map _ _ _ _ (D.map (g _ (by simp))) (𝟙 _) (𝟙 _) (by
            rw [← D.map_comp, IsCofiltered.infTo_commutes]
            · simp [g]
            · simp
            · exact Finset.mem_image_of_mem _ (Finset.mem_univ _)) (by simp)
        exact Function.isEmpty F
      obtain ⟨x, -⟩ :=
        Cover.covers (𝒰.pullback₁ (D.map (g i (by simp)))) (Nonempty.some inferInstance)
      exact (this _).elim x
    let F := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget _
    have (i' : _) : IsAffine (F.obj i') :=
      have : IsAffineHom (pullback.snd (D.map i'.hom) (𝒰.f j)) :=
        MorphismProperty.pullback_snd _ _ inferInstance
      isAffine_of_isAffineHom (pullback.snd (D.map i'.hom) (𝒰.f j))
    have (i' : _) : Nonempty (F.obj i') := H i'.hom
    let e : F ⟶ (F ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := Functor.whiskerLeft F ΓSpec.adjunction.unit
    have (i : _) : IsIso (e.app i) := IsAffine.affine
    have : IsIso e := NatIso.isIso_of_isIso_app e
    let c' : LimitCone F := ⟨_, (IsLimit.postcomposeInvEquiv (asIso e) _).symm
      (isLimitOfPreserves Scheme.Spec (limit.isLimit (F ⋙ Scheme.Γ.rightOp)))⟩
    have : Nonempty c'.1.pt := by
      apply +allowSynthFailures PrimeSpectrum.instNonemptyOfNontrivial
      have (i' : _) : Nontrivial ((F ⋙ Scheme.Γ.rightOp).leftOp.obj i') := by
        apply +allowSynthFailures Scheme.component_nontrivial
        simp
      exact CommRingCat.FilteredColimits.nontrivial
        (isColimitCoconeLeftOpOfCone _ (limit.isLimit (F ⋙ Scheme.Γ.rightOp)))
    let α : F ⟶ Over.forget _ ⋙ D := Functor.whiskerRight
      (Functor.whiskerLeft (Over.post D) (Over.mapPullbackAdj (𝒰.f j)).counit) (Over.forget _)
    exact this.map (((Functor.Initial.isLimitWhiskerEquiv (Over.forget i) c).symm hc).lift
        ((Cone.postcompose α).obj c'.1))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inl : IsEmpty I → Nonempty.{u + 1} ↥c.pt
⊢ Nonempty.{u + 1} ↥c.pt
have inr : Nonempty I → Nonempty.{u + 1} ↥c.pt
Tactic: classical
  cases isEmpty_or_nonempty I
  · have e := (isLimitEquivIsTerminalOfIsEmpty _ _ hc).uniqueUpToIso specULiftZIsTerminal
    exact Nonempty.map e.inv inferInstance
  · have i := Nonempty.some ‹Nonempty I›
    have : IsCofiltered I := ⟨⟩
    let 𝒰 := (D.obj i).affineCover.finiteSubcover
    have (i' : _) : IsAffine (𝒰.X i') := inferInstanceAs (IsAffine (Spec _))
    obtain ⟨j, H⟩ :
        ∃ j : 𝒰.I₀, ∀ {i'} (f : i' ⟶ i), Nonempty ((𝒰.pullback₁ (D.map f)).X j) := by
      by_contra! H
      choose i' f hf using H
      let g (j) := IsCofiltered.infTo (insert i (Finset.univ.image i'))
        (Finset.univ.image fun j : 𝒰.I₀ ↦ ⟨_, _, by simp, by simp, f j⟩) (X := j)
      have (j : 𝒰.I₀) : IsEmpty ((𝒰.pullback₁ (D.map (g i (by simp)))).X j) := by
        let F : (𝒰.pullback₁ (D.map (g i (by simp)))).X j ⟶
            (𝒰.pullback₁ (D.map (f j))).X j :=
          pullback.map _ _ _ _ (D.map (g _ (by simp))) (𝟙 _) (𝟙 _) (by
            rw [← D.map_comp, IsCofiltered.infTo_commutes]
            · simp [g]
            · simp
            · exact Finset.mem_image_of_mem _ (Finset.mem_univ _)) (by simp)
        exact Function.isEmpty F
      obtain ⟨x, -⟩ :=
        Cover.covers (𝒰.pullback₁ (D.map (g i (by simp)))) (Nonempty.some inferInstance)
      exact (this _).elim x
    let F := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget _
    have (i' : _) : IsAffine (F.obj i') :=
      have : IsAffineHom (pullback.snd (D.map i'.hom) (𝒰.f j)) :=
        MorphismProperty.pullback_snd _ _ inferInstance
      isAffine_of_isAffineHom (pullback.snd (D.map i'.hom) (𝒰.f j))
    have (i' : _) : Nonempty (F.obj i') := H i'.hom
    let e : F ⟶ (F ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := Functor.whiskerLeft F ΓSpec.adjunction.unit
    have (i : _) : IsIso (e.app i) := IsAffine.affine
    have : IsIso e := NatIso.isIso_of_isIso_app e
    let c' : LimitCone F := ⟨_, (IsLimit.postcomposeInvEquiv (asIso e) _).symm
      (isLimitOfPreserves Scheme.Spec (limit.isLimit (F ⋙ Scheme.Γ.rightOp)))⟩
    have : Nonempty c'.1.pt := by
      apply +allowSynthFailures PrimeSpectrum.instNonemptyOfNontrivial
      have (i' : _) : Nontrivial ((F ⋙ Scheme.Γ.rightOp).leftOp.obj i') := by
        apply +allowSynthFailures Scheme.component_nontrivial
        simp
      exact CommRingCat.FilteredColimits.nontrivial
        (isColimitCoconeLeftOpOfCone _ (limit.isLimit (F ⋙ Scheme.Γ.rightOp)))
    let α : F ⟶ Over.forget _ ⋙ D := Functor.whiskerRight
      (Functor.whiskerLeft (Over.post D) (Over.mapPullbackAdj (𝒰.f j)).counit) (Over.forget _)
    exact this.map (((Functor.Initial.isLimitWhiskerEquiv (Over.forget i) c).symm hc).lift
        ((Cone.postcompose α).obj c'.1))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
X Y : I
f : X ⟶ Y
⊢ vanishingIdeal { carrier := Z Y, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj Y) } ≤
    (vanishingIdeal { carrier := Z X, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj X) }).map (D.map f)
have rw : TopologicalSpace.Closeds.closure
    (⇑(D.map f) '' (↑{ carrier := Z X, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj X) } : Set ↥(D.obj X))) ≤
  (vanishingIdeal { carrier := Z Y, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj Y) }).support
Tactic: rw [map_vanishingIdeal, ← le_support_iff_le_vanishingIdeal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  {
    obj := fun (i : I) ↦
      (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).subscheme,
    map := fun {X Y : I} (f : X ⟶ Y) ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun (i : I) ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
i j : I
f : i ⟶ j
⊢ IsAffineHom (D'.map f)
have suffices : IsAffineHom (D'.map f ≫ ι.app j)
Tactic: suffices IsAffineHom (D'.map f ≫ ι.app j) from .of_comp _ (ι.app j)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  {
    obj := fun (i : I) ↦
      (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).subscheme,
    map := fun {X Y : I} (f : X ⟶ Y) ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun (i : I) ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
i j : I
f : i ⟶ j
⊢ IsAffineHom (D'.map f ≫ ι.app j)
have simp : IsAffineHom
  ((vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) }).subschemeι ≫ D.map f)
Tactic: simp only [subschemeMap_subschemeι, D', ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  {
    obj := fun (i : I) ↦
      (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).subscheme,
    map := fun {X Y : I} (f : X ⟶ Y) ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun (i : I) ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
⊢ ∃ (s : ↥c.pt), ∀ (i : I), Membership.mem (α := ↥(D.obj i)) (Z i) ((c.π.app i) s : ↥(D.obj i))
have this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
Tactic: haveI {i j} (f : i ⟶ j) : IsAffineHom (D'.map f) := by
    suffices IsAffineHom (D'.map f ≫ ι.app j) from .of_comp _ (ι.app j)
    simp only [subschemeMap_subschemeι, D', ι]
    infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  {
    obj := fun (i : I) ↦
      (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).subscheme,
    map := fun {X Y : I} (f : X ⟶ Y) ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun (i : I) ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
⊢ ∃ (s : ↥c.pt), ∀ (i : I), Membership.mem (α := ↥(D.obj i)) (Z i) ((c.π.app i) s : ↥(D.obj i))
have x : ∀ (i : I), Nonempty.{u + 1} ↥(D'.obj i)
Tactic: haveI _ (i) : Nonempty (D'.obj i) := Set.nonempty_coe_sort.mpr (hZne i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  {
    obj := fun (i : I) ↦
      (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).subscheme,
    map := fun {X Y : I} (f : X ⟶ Y) ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun (i : I) ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
h : ∀ (i : I), Nonempty.{u + 1} ↥(D'.obj i)
⊢ ∃ (s : ↥c.pt), ∀ (i : I), Membership.mem (α := ↥(D.obj i)) (Z i) ((c.π.app i) s : ↥(D.obj i))
have x : ∀ (i : I), CompactSpace.{u} ↥(D'.obj i)
Tactic: haveI _ (i) : CompactSpace (D'.obj i) := isCompact_iff_compactSpace.mp (hZcpt i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  {
    obj := fun (i : I) ↦
      (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).subscheme,
    map := fun {X Y : I} (f : X ⟶ Y) ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun (i : I) ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
h : ∀ (i : I), Nonempty.{u + 1} ↥(D'.obj i)
h_1 : ∀ (i : I), CompactSpace.{u} ↥(D'.obj i)
c' : Cone D' :=
  {
    pt :=
      subscheme (X := c.1)
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)),
    π :=
      {
        app := fun (i : I) ↦
          subschemeMap
            (⨆ (i : I),
              (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
                (c.π.app i))
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }) (c.π.app i) ⋯,
        naturality := ⋯ } }
s : Cone D'
⊢ Scheme.Hom.ker (X := c'.pt)
      (subschemeι
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
            (c.π.app i))) ≤
    Scheme.Hom.ker (X := s.pt) (hc.lift ((Cone.postcompose ι).obj s) : ((Cone.postcompose ι).obj s).pt ⟶ c.pt)
have suffices : ∀ (i : I),
  vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) } ≤
    Scheme.Hom.ker (s.π.app i ≫ ι.app i)
Tactic: suffices ∀ i, vanishingIdeal ⟨Z i, hZc i⟩ ≤ (s.π.app i ≫ ι.app i).ker by
        simpa [← le_map_iff_comap_le, ← Scheme.Hom.ker_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  {
    obj := fun (i : I) ↦
      (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).subscheme,
    map := fun {X Y : I} (f : X ⟶ Y) ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun (i : I) ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
h : ∀ (i : I), Nonempty.{u + 1} ↥(D'.obj i)
h_1 : ∀ (i : I), CompactSpace.{u} ↥(D'.obj i)
c' : Cone D' :=
  {
    pt :=
      subscheme (X := c.1)
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)),
    π :=
      {
        app := fun (i : I) ↦
          subschemeMap
            (⨆ (i : I),
              (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
                (c.π.app i))
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }) (c.π.app i) ⋯,
        naturality := ⋯ } }
s : Cone D'
⊢ ∀ (i : I),
    vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) } ≤
      Scheme.Hom.ker (s.π.app i ≫ ι.app i)
have refine : ∀ (i : I),
  vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) } ≤ Scheme.Hom.ker (ι.app i)
Tactic: refine fun i ↦ .trans ?_ (Scheme.Hom.le_ker_comp _ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  {
    obj := fun (i : I) ↦
      (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).subscheme,
    map := fun {X Y : I} (f : X ⟶ Y) ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun (i : I) ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
h : ∀ (i : I), Nonempty.{u + 1} ↥(D'.obj i)
h_1 : ∀ (i : I), CompactSpace.{u} ↥(D'.obj i)
c' : Cone D' :=
  {
    pt :=
      subscheme (X := c.1)
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)),
    π :=
      {
        app := fun (i : I) ↦
          subschemeMap
            (⨆ (i : I),
              (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
                (c.π.app i))
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }) (c.π.app i) ⋯,
        naturality := ⋯ } }
s : Cone D'
m : s.pt ⟶ c'.pt
hm : ∀ (j : I), m ≫ c'.π.app j = s.π.app j
⊢ m =
    IsClosedImmersion.lift
      (subschemeι
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
      (hc.lift ((Cone.postcompose ι).obj s)) ⋯
have rw : m ≫
    subschemeι
      (⨆ (i : I),
        (vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)) =
  CategoryStruct.comp (Y :=
    subscheme (X := c.1)
      (⨆ (i : I),
        (vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
    (IsClosedImmersion.lift
      (subschemeι
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
      (hc.lift ((Cone.postcompose ι).obj s)) sorry)
    (subschemeι
      (⨆ (i : I),
        (vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
Tactic: rw [← cancel_mono (subschemeι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  {
    obj := fun (i : I) ↦
      (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).subscheme,
    map := fun {X Y : I} (f : X ⟶ Y) ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun (i : I) ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
h : ∀ (i : I), Nonempty.{u + 1} ↥(D'.obj i)
h_1 : ∀ (i : I), CompactSpace.{u} ↥(D'.obj i)
c' : Cone D' :=
  {
    pt :=
      subscheme (X := c.1)
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)),
    π :=
      {
        app := fun (i : I) ↦
          subschemeMap
            (⨆ (i : I),
              (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
                (c.π.app i))
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }) (c.π.app i) ⋯,
        naturality := ⋯ } }
hc' : IsLimit c' :=
  {
    lift := fun (s : Cone D') ↦
      IsClosedImmersion.lift
        (subschemeι
          (⨆ (i : I),
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
              (c.π.app i)))
        (hc.lift ((Cone.postcompose ι).obj s)) ⋯,
    fac := ⋯, uniq := ⋯ }
⊢ ∃ (s : ↥c.pt), ∀ (i : I), Membership.mem (α := ↥(D.obj i)) (Z i) ((c.π.app i) s : ↥(D.obj i))
have this₁ : Nonempty.{u + 1}
  ↥(support
      (⨆ (i : I),
        (vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
Tactic: have : Nonempty (⨆ i, (vanishingIdeal ⟨Z i, hZc i⟩).comap (c.π.app i)).support :=
    Scheme.nonempty_of_isLimit D' c' hc'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
j : I
Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)
hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)
hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty
hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)
hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(D.map hi'i)) (Z i' (hi'i ≫ hij)) (Z i hij)
i₁ i₂ : Over j
f : i₁ ⟶ i₂
⊢ IsAffineHom ((Over.forget j ⋙ D).map f)
have dsimp : IsAffineHom (D.map (Over.Hom.left f))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (hypothesis)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
j : I
Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)
hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)
hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty
hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)
hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(D.map hi'i)) (Z i' (hi'i ≫ hij)) (Z i hij)
⊢ ∃ (s : ↥c.pt), ∀ (i : I) (hij : i ⟶ j), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((c.π.app i) s : ↥(D.obj i))
have this : ∀ {i₁ i₂ : Over j} (f : i₁ ⟶ i₂), IsAffineHom ((Over.forget j ⋙ D).map f)
Tactic: have {i₁ i₂ : Over j} (f : i₁ ⟶ i₂) : IsAffineHom ((Over.forget j ⋙ D).map f) := by
    dsimp; infer_instance