awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)

Tactic:
fun i ↦ .trans ?_ (Scheme.Hom.le_ker_comp _ _)

Premises used: CategoryTheory.Limits.Cone.π, AlgebraicGeometry.Scheme.Hom.le_ker_comp, LE.le.trans, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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'
refine :
  ∀ (i : I),
    vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) } ≤ Scheme.Hom.ker (ι.app i)
⊢ ∀ (i : I),
    vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) } ≤
      Scheme.Hom.ker (s.π.app i ≫ ι.app i)

Tactic:
refine fun i ↦ .trans ?_ (Scheme.Hom.le_ker_comp _ _)
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 (ι.app i)

Tactic:
simp [ι]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
⊢ 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)) ⋯ ≫
      c'.π.app i =
    s.π.app i

Tactic:
simp [← cancel_mono (subschemeι _), c', ι]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
rw :
  m ≫
      subschemeι
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)) =
    CategoryStruct.comp (Y :=
      subscheme (X := c.1)
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
      (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)) ⋯)
      (subschemeι
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
⊢ 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)) ⋯

Tactic:
rw [← cancel_mono (subschemeι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 ≫
      subschemeι
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)) =
    CategoryStruct.comp (Y :=
      subscheme (X := c.1)
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
      (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)) ⋯)
      (subschemeι
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))

Tactic:
hc.hom_ext fun i ↦ ?_

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
i : I
⊢ (m ≫
        subschemeι
          (⨆ (i : I),
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
              (c.π.app i))) ≫
      c.π.app i =
    CategoryStruct.comp (Y :=
        subscheme (X := c.1)
          (⨆ (i : I),
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
              (c.π.app i)))
        (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)) ⋯)
        (subschemeι
          (⨆ (i : I),
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
              (c.π.app i))) ≫
      c.π.app i

Tactic:
simp [ι, c', ← hm]
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 := ⋯ }
⊢ Nonempty.{u + 1}
    ↥(support
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : 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'
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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_1 : ∀ {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 := ⋯ }
this :
  Nonempty.{u + 1}
    ↥(support
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
⊢ ∃ (s : ↥c.pt), ∀ (i : I), Membership.mem (α := ↥(D.obj i)) (Z i) ((c.π.app i) s : ↥(D.obj i))

Tactic:
simpa using this
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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₂
dsimp : IsAffineHom (D.map (Over.Hom.left f))
⊢ IsAffineHom ((Over.forget j ⋙ D).map f)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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 (D.map (Over.Hom.left f))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)

Tactic:
have {i₁ i₂ : Over j} (f : i₁ ⟶ i₂) : IsAffineHom ((Over.forget j ⋙ D).map f) := by
    dsimp; infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)
this : ∀ {i₁ i₂ : Over j} (f : i₁ ⟶ i₂), IsAffineHom ((Over.forget j ⋙ D).map f)
i₁ i₂ : Over j
f : i₁ ⟶ i₂
dsimp : Set.MapsTo (⇑(D.map (Over.Hom.left f))) (Z i₁.left i₁.hom) (Z i₂.left i₂.hom)
⊢ Set.MapsTo (α := ↥((Over.forget j ⋙ D).obj i₁)) (β := ↥((Over.forget j ⋙ D).obj i₂)) (⇑((Over.forget j ⋙ D).map f))
    ((fun (i : Over j) ↦ Z i.left i.hom) i₁) ((fun (i : Over j) ↦ Z i.left i.hom) i₂)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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)
this : ∀ {i₁ i₂ : Over j} (f : i₁ ⟶ i₂), IsAffineHom ((Over.forget j ⋙ D).map f)
i₁ i₂ : Over j
f : i₁ ⟶ i₂
rw : Set.MapsTo (⇑(D.map (Over.Hom.left f))) (Z i₁.left (Over.Hom.left f ≫ i₂.hom)) (Z i₂.left i₂.hom)
⊢ Set.MapsTo (⇑(D.map (Over.Hom.left f))) (Z i₁.left i₁.hom) (Z i₂.left i₂.hom)

Tactic:
rw [← Over.w f]

Premises used: CategoryTheory.Over.w