awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
a : S ⟶ Opposite.unop (D.obj i)
b : S ⟶ Opposite.unop (D.obj j)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
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 : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ
hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ
this : CreatesLimitsOfSize.{u, u, u, u, u + 1, u + 1} Scheme.Spec
⊢ Spec.map (φ ≫ a) = Spec.map (t.app (Opposite.op i))

Tactic:
simpa using ha.symm

Premises used: Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
a : S ⟶ Opposite.unop (D.obj i)
b : S ⟶ Opposite.unop (D.obj j)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
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 : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ
hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ
this : CreatesLimitsOfSize.{u, u, u, u, u + 1, u + 1} Scheme.Spec
⊢ Spec.map (φ ≫ b) = Spec.map (t.app (Opposite.op j))

Tactic:
simpa using hb.symm

Premises used: Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
a : S ⟶ Opposite.unop (D.obj i)
b : S ⟶ Opposite.unop (D.obj j)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
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 : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ
hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ
this : CreatesLimitsOfSize.{u, u, u, u, u + 1, u + 1} Scheme.Spec
simp : Spec.map ((liftLimit hc).π.app i).unop ≫ Spec.map a = Spec.map ((liftLimit hc).π.app j).unop ≫ Spec.map b
⊢ Spec.map (a ≫ (coconeLeftOpOfCone (liftLimit hc)).ι.app (Opposite.op i)) =
    Spec.map (b ≫ (coconeLeftOpOfCone (liftLimit hc)).ι.app (Opposite.op j))

Tactic:
simp only [coconeLeftOpOfCone_pt, Functor.const_obj_obj,
        Functor.leftOp_obj, coconeLeftOpOfCone_ι_app, Spec.map_comp]

Premises used: CategoryTheory.Functor.leftOp_obj, AlgebraicGeometry.Spec.map_comp, CategoryTheory.Limits.coconeLeftOpOfCone_ι_app, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Limits.coconeLeftOpOfCone_pt
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
a : S ⟶ Opposite.unop (D.obj i)
b : S ⟶ Opposite.unop (D.obj j)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
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 : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ
hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ
this : CreatesLimitsOfSize.{u, u, u, u, u + 1, u + 1} Scheme.Spec
obtain :
  ∀ (k : Iᵒᵖ) (hik : Opposite.op i ⟶ k) (hjk : Opposite.op j ⟶ k) (H : a ≫ D.leftOp.map hik = b ≫ D.leftOp.map hjk),
    ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j),
      (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b

Tactic:
obtain ⟨k, hik, hjk, H⟩ := (HasRingHomProperty.Spec_iff.mp ‹LocallyOfFiniteType (Spec.map φ)›)
    |>.essFiniteType.exists_comp_map_eq_of_isColimit _ D.leftOp t _
    (coconeLeftOpOfCone (liftLimit hc))
    (isColimitCoconeLeftOpOfCone _ (liftedLimitIsLimit _))
    a (Spec.map_injective (by simpa using ha.symm))
    b (Spec.map_injective (by simpa using hb.symm))
    (Spec.map_injective (by
      simp only [coconeLeftOpOfCone_pt, Functor.const_obj_obj,
        Functor.leftOp_obj, coconeLeftOpOfCone_ι_app, Spec.map_comp]
      simp only [← Scheme.Spec_map, ← liftedLimitMapsToOriginal_hom_π, Category.assoc, hab]))
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
a : S ⟶ Opposite.unop (D.obj i)
b : S ⟶ Opposite.unop (D.obj j)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
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 : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ
hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ
this : CreatesLimitsOfSize.{u, u, u, u, u + 1, u + 1} Scheme.Spec
k : Iᵒᵖ
hik : Opposite.op i ⟶ k
hjk : Opposite.op j ⟶ k
H : a ≫ D.leftOp.map hik = b ≫ D.leftOp.map hjk
⊢ (D ⋙ Scheme.Spec).map hik.unop ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk.unop ≫ Spec.map b

Tactic:
simpa [← Spec.map_comp, Spec.map_inj] using H

Premises used: AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Spec.map_inj
-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
i j : I
R : CommRingCat
inst_2 : IsAffine.{u} (Spec R)
S : CommRingCat
inst_3 : IsAffine.{u} (Spec S)
φ : R ⟶ S
inst_4 : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst_5 : ∀ (i : I), CompactSpace.{u} ↥((D ⋙ Scheme.Spec).obj i)
inst_6 : ∀ (i : I), IsAffine.{u} ((D ⋙ Scheme.Spec).obj i)
inst_7 : IsAffine.{u} c.pt
a : S ⟶ Opposite.unop (D.obj i)
b : S ⟶ Opposite.unop (D.obj j)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
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 : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ
hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ
this : CreatesLimitsOfSize.{u, u, u, u, u + 1, u + 1} Scheme.Spec
k : Iᵒᵖ
hik : Opposite.op i ⟶ k
hjk : Opposite.op j ⟶ k
H : a ≫ D.leftOp.map hik = b ≫ D.leftOp.map hjk
⊢ ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b

Tactic:
exact ⟨k.unop, hik.unop, hjk.unop, by simpa [← Spec.map_comp, Spec.map_inj] using H⟩
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
by_contra! :
  ∀
    (h :
      ∀ (i' : I) (hii' : i' ⟶ A.i),
        Set.Nonempty (α := ↥(D.obj i'))
          (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
            (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)),
    False
⊢ ∃ (i' : I) (hii' : i' ⟶ A.i),
    Eq (α := Set ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
      ∅

Tactic:
by_contra! h
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
⊢ ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')

Tactic:
have hZ (i') (hii' : i' ⟶ A.i) : IsClosed (Z i' hii') :=
    (W.isOpen.isClosed_compl).preimage <| Scheme.Hom.continuous _
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
i i' : I
hii' : i' ⟶ i
hij : i ⟶ A.i
⊢ Set.MapsTo (⇑(D.map hii')) (Z i' (hii' ≫ hij)) (Z i hij)

Tactic:
simp [Z, Set.MapsTo]

Premises used: Set.MapsTo
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
⊢ False

Tactic:
hs A.i (𝟙 A.i) (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange _ _ _ ?_)

Premises used: CategoryTheory.CategoryStruct.id, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, AlgebraicGeometry.ExistsHomHomCompEqCompAux.i
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
refine :
  Membership.mem (α := ↥(pullback.diagonalObj f)) (γ := Set ↥(pullback.diagonalObj f))
    (Set.range (ι := ↥X) ⇑(pullback.diagonal f))
    ((D.map (𝟙 A.i) ≫ pullback.lift A.a A.b ⋯) ((A.c.π.app A.i) s : ↥(D.obj A.i)) : ↥(pullback f f))
⊢ False

Tactic:
refine hs A.i (𝟙 A.i) (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange _ _ _ ?_)

Premises used: CategoryTheory.CategoryStruct.id, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange, AlgebraicGeometry.ExistsHomHomCompEqCompAux.i
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
h₁ :
  Eq (α := ↥(pullback.diagonalObj f)) ((pullback.diagonal f) ((A.c.π.app A.i ≫ A.a) s : ↥X) : ↥(pullback.diagonalObj f))
    ((D.map (𝟙 A.i) ≫ pullback.lift A.a A.b ⋯) ((A.c.π.app A.i) s : ↥(D.obj A.i)) : ↥(pullback f f))
⊢ Membership.mem (α := ↥(pullback.diagonalObj f)) (γ := Set ↥(pullback.diagonalObj f))
    (Set.range (ι := ↥X) ⇑(pullback.diagonal f))
    ((D.map (𝟙 A.i) ≫ pullback.lift A.a A.b ⋯) ((A.c.π.app A.i) s : ↥(D.obj A.i)) : ↥(pullback f f))

Tactic:
use (A.c.π.app A.i ≫ A.a) s

Premises used: CategoryTheory.Limits.Cone.π, AlgebraicGeometry.ExistsHomHomCompEqCompAux.a, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.ExistsHomHomCompEqCompAux.c, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.ExistsHomHomCompEqCompAux.i, DFunLike.coe, CategoryTheory.NatTrans.app
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
h₀ :
  CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (pullback.fst f f) =
    CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯) (pullback.fst f f)
h₁ :
  CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (pullback.snd f f) =
    CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯) (pullback.snd f f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const I) A.c.pt) A.i ⟶ pullback.diagonalObj f)
    (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯)

Tactic:
ext
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
⊢ CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (pullback.fst f f) =
    CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯) (pullback.fst f f)

Tactic:
simp [hab]

Premises used: AlgebraicGeometry.ExistsHomHomCompEqCompAux.hab
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
⊢ CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (pullback.snd f f) =
    CategoryStruct.comp (Y := pullback f f) (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯) (pullback.snd f f)

Tactic:
simp [hab]

Premises used: AlgebraicGeometry.ExistsHomHomCompEqCompAux.hab
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const I) A.c.pt) A.i ⟶ pullback.diagonalObj f)
    (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯)

Tactic:
have H : A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f =
      A.c.π.app A.i ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb) := by ext <;> simp [hab]
-- 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
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : IsCofiltered I
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    Set.Nonempty (α := ↥(D.obj i'))
      (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹'
        (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X) : Set ↥(pullback f f))ᶜ)
Z : (i' : I) → (hii' : i' ⟶ A.i) → Set ↥(D.obj i') :=
  fun (i' : I) (hii' : i' ⟶ A.i) ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W : Set ↥(pullback f f))ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), Membership.mem (α := ↥(D.obj i)) (Z i hij) ((A.c.π.app i) s : ↥(D.obj i))
H :
  Eq (α := Functor.obj (Functor.obj (Functor.const I) A.c.pt) A.i ⟶ pullback.diagonalObj f)
    (A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f) (A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯)
⊢ Eq (α := ↥(pullback.diagonalObj f)) ((pullback.diagonal f) ((A.c.π.app A.i ≫ A.a) s : ↥X) : ↥(pullback.diagonalObj f))
    ((D.map (𝟙 A.i) ≫ pullback.lift A.a A.b ⋯) ((A.c.π.app A.i) s : ↥(D.obj A.i)) : ↥(pullback f f))

Tactic:
simp [← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base, H]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Hom.comp_base