awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S : Scheme
n : Type v
R : CommRingCat
h : IsIntegralHom (Y := Spec R) (AffineSpace.{v, u} n (Spec R) ↘ Spec R)
h_1 : Nonempty ↥(Spec R)
this_1 : Nontrivial (↑R : Type (max u v))
i : n
this :
  (RingHom.toMorphismProperty fun {R S : Type (max u v)} [CommRing R] [CommRing S] (f : R →+* S) ↦
      f.IsIntegral).RespectsIso
false :
  ∀
    (h :
      IsAffine (Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))) ∧
        RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type (max u v))) (A :=
          (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), Spec.map (CommRingCat.ofHom C) ⁻¹ᵁ ⊤) :
            Type (max u v)))
          (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤))),
    Nonempty ↥(Spec R) →
      ∀ (this : Nontrivial (↑R : Type (max u v))) (i : n)
        (this :
          (RingHom.toMorphismProperty fun {R S : Type (max u v)} [CommRing R] [CommRing S] (f : R →+* S) ↦
              f.IsIntegral).RespectsIso),
        False
⊢ False

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso @IsIntegralHom (SpecIso n R).inv,
      SpecIso_inv_over, HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom)] at h

Premises used: AlgebraicGeometry.AffineSpace.SpecIso, AlgebraicGeometry.IsIntegralHom, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, AlgebraicGeometry.AffineSpace.SpecIso_inv_over, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))) ∧
    RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type (max u v))) (A :=
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), Spec.map (CommRingCat.ofHom C) ⁻¹ᵁ ⊤) :
        Type (max u v)))
      (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤))
h_1 : Nonempty ↥(Spec R)
this_1 : Nontrivial (↑R : Type (max u v))
i : n
this :
  (RingHom.toMorphismProperty fun {R S : Type (max u v)} [CommRing R] [CommRing S] (f : R →+* S) ↦
      f.IsIntegral).RespectsIso
false :
  ∀ (p : Polynomial (↑R : Type (max u v))) (hp : p.Monic)
    (hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0), False
⊢ False

Tactic:
obtain ⟨p : Polynomial R, hp, hp'⟩ :=
      (MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
        (arrowIsoΓSpecOfIsAffine _)).mpr h.2 (X i)

Premises used: Iff.mpr, CommRingCat.carrier, MvPolynomial.X, Polynomial, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, And.right, RingHom.toMorphismProperty, RingHom.IsIntegral, AlgebraicGeometry.arrowIsoΓSpecOfIsAffine
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))) ∧
    RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type (max u v))) (A :=
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), Spec.map (CommRingCat.ofHom C) ⁻¹ᵁ ⊤) :
        Type (max u v)))
      (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤))
h_1 : Nonempty ↥(Spec R)
this_1 : Nontrivial (↑R : Type (max u v))
i : n
this :
  (RingHom.toMorphismProperty fun {R S : Type (max u v)} [CommRing R] [CommRing S] (f : R →+* S) ↦
      f.IsIntegral).RespectsIso
p : Polynomial (↑R : Type (max u v))
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
⊢ Eq (α := MvPolynomial n (↑R : Type (max u v)))
    ((AlgHom.comp (rename fun (x : PUnit.{v + 1}) ↦ i)
            (↑(AlgEquiv.symm (uniqueAlgEquiv (↑R : Type (max u v)) PUnit.{v + 1})) :
              Polynomial (↑R : Type (max u v)) →ₐ[(↑R : Type (max u v))]
                MvPolynomial PUnit.{v + 1} (↑R : Type (max u v))) :
          (a : Polynomial (↑R : Type (max u v))) → MvPolynomial n (↑R : Type (max u v)))
        p :
      MvPolynomial n (↑R : Type (max u v)))
    (0 : MvPolynomial n (↑R : Type (max u v)))

Tactic:
simp [← hp', ← algebraMap_eq]

Premises used: MvPolynomial.algebraMap_eq
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))) ∧
    RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type (max u v))) (A :=
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), Spec.map (CommRingCat.ofHom C) ⁻¹ᵁ ⊤) :
        Type (max u v)))
      (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤))
h_1 : Nonempty ↥(Spec R)
this_1 : Nontrivial (↑R : Type (max u v))
i : n
this :
  (RingHom.toMorphismProperty fun {R S : Type (max u v)} [CommRing R] [CommRing S] (f : R →+* S) ↦
      f.IsIntegral).RespectsIso
p : Polynomial (↑R : Type (max u v))
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
⊢ Eq (α := MvPolynomial n (↑R : Type (max u v)))
    ((AlgHom.comp (rename fun (x : PUnit.{v + 1}) ↦ i)
            (↑(AlgEquiv.symm (uniqueAlgEquiv (↑R : Type (max u v)) PUnit.{v + 1})) :
              Polynomial (↑R : Type (max u v)) →ₐ[(↑R : Type (max u v))]
                MvPolynomial PUnit.{v + 1} (↑R : Type (max u v))) :
          (a : Polynomial (↑R : Type (max u v))) → MvPolynomial n (↑R : Type (max u v)))
        p :
      MvPolynomial n (↑R : Type (max u v)))
    (0 : MvPolynomial n (↑R : Type (max u v)))

Tactic:
have : (rename fun _ ↦ i).comp (uniqueAlgEquiv.{_, v} _ PUnit).symm.toAlgHom p = 0 := by
      simp [← hp', ← algebraMap_eq]
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))) ∧
    RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type (max u v))) (A :=
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), Spec.map (CommRingCat.ofHom C) ⁻¹ᵁ ⊤) :
        Type (max u v)))
      (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤))
h_1 : Nonempty ↥(Spec R)
this_1 : Nontrivial (↑R : Type (max u v))
i : n
this_2 :
  (RingHom.toMorphismProperty fun {R S : Type (max u v)} [CommRing R] [CommRing S] (f : R →+* S) ↦
      f.IsIntegral).RespectsIso
p : Polynomial (↑R : Type (max u v))
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
this :
  Eq (α := MvPolynomial n (↑R : Type (max u v)))
    ((AlgHom.comp (rename fun (x : PUnit.{v + 1}) ↦ i)
            (↑(AlgEquiv.symm (uniqueAlgEquiv (↑R : Type (max u v)) PUnit.{v + 1})) :
              Polynomial (↑R : Type (max u v)) →ₐ[(↑R : Type (max u v))]
                MvPolynomial PUnit.{v + 1} (↑R : Type (max u v))) :
          (a : Polynomial (↑R : Type (max u v))) → MvPolynomial n (↑R : Type (max u v)))
        p :
      MvPolynomial n (↑R : Type (max u v)))
    (0 : MvPolynomial n (↑R : Type (max u v)))
⊢ Eq (α := MvPolynomial PUnit.{v + 1} (↑R : Type (max u v)))
    (((↑(AlgEquiv.symm (uniqueAlgEquiv (↑R : Type (max u v)) PUnit.{v + 1})) :
            Polynomial (↑R : Type (max u v)) →ₐ[(↑R : Type (max u v))]
              MvPolynomial PUnit.{v + 1} (↑R : Type (max u v))) :
          (a : Polynomial (↑R : Type (max u v))) → MvPolynomial PUnit.{v + 1} (↑R : Type (max u v)))
        p :
      MvPolynomial PUnit.{v + 1} (↑R : Type (max u v)))
    (0 : MvPolynomial PUnit.{v + 1} (↑R : Type (max u v)))

Tactic:
rw [AlgHom.comp_apply, map_eq_zero_iff _ (rename_injective _ (fun _ _ _ ↦ rfl))] at this

Premises used: AlgHom.comp_apply, MvPolynomial.rename_injective, map_eq_zero_iff
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))) ∧
    RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type (max u v))) (A :=
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), Spec.map (CommRingCat.ofHom C) ⁻¹ᵁ ⊤) :
        Type (max u v)))
      (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤))
h_1 : Nonempty ↥(Spec R)
this_1 : Nontrivial (↑R : Type (max u v))
i : n
this_2 :
  (RingHom.toMorphismProperty fun {R S : Type (max u v)} [CommRing R] [CommRing S] (f : R →+* S) ↦
      f.IsIntegral).RespectsIso
p : Polynomial (↑R : Type (max u v))
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
this :
  Eq (α := MvPolynomial PUnit.{v + 1} (↑R : Type (max u v)))
    (((↑(AlgEquiv.symm (uniqueAlgEquiv (↑R : Type (max u v)) PUnit.{v + 1})) :
            Polynomial (↑R : Type (max u v)) →ₐ[(↑R : Type (max u v))]
              MvPolynomial PUnit.{v + 1} (↑R : Type (max u v))) :
          (a : Polynomial (↑R : Type (max u v))) → MvPolynomial PUnit.{v + 1} (↑R : Type (max u v)))
        p :
      MvPolynomial PUnit.{v + 1} (↑R : Type (max u v)))
    (0 : MvPolynomial PUnit.{v + 1} (↑R : Type (max u v)))
⊢ p = 0

Tactic:
simp only [AlgEquiv.coe_algHom, EmbeddingLike.map_eq_zero_iff] at this

Premises used: AlgEquiv.coe_algHom, EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v))))) ∧
    RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type (max u v))) (A :=
      (↑Γ(Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))), Spec.map (CommRingCat.ofHom C) ⁻¹ᵁ ⊤) :
        Type (max u v)))
      (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤))
h_1 : Nonempty ↥(Spec R)
this_1 : Nontrivial (↑R : Type (max u v))
i : n
this_2 :
  (RingHom.toMorphismProperty fun {R S : Type (max u v)} [CommRing R] [CommRing S] (f : R →+* S) ↦
      f.IsIntegral).RespectsIso
p : Polynomial (↑R : Type (max u v))
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
this : p = 0
⊢ False

Tactic:
simp [this] at hp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsEmpty ↥S
⊢ IsIntegralHom (AffineSpace.{v, u} n S ↘ S)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsEmpty n
⊢ IsIntegralHom (AffineSpace.{v, u} n S ↘ S)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
inst : Nonempty ↥S
inst_1 : Nonempty n
⊢ ¬IsIntegralHom (AffineSpace.{v, u} n S ↘ S)

Tactic:
simp [isIntegralHom_over_iff_isEmpty]

Premises used: AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
R : CommRingCat
p q : ↥(Spec R)
⊢ p ≤ q ↔ q.asIdeal ≤ p.asIdeal

Tactic:
aesop (add simp PrimeSpectrum.le_iff_specializes)

Premises used: PrimeSpectrum.le_iff_specializes
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
R : CommRingCat
⊢ Eq.{u_1 + 1} (α := Preorder ↥(Spec R)) inferInstance inferInstance

Tactic:
aesop (add simp spec_le_iff)

Premises used: AlgebraicGeometry.AffineSpace.spec_le_iff
-- 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)
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
inr : Nonempty I → Nonempty.{u + 1} ↥c.pt
⊢ Nonempty.{u + 1} ↥c.pt

Tactic:
cases isEmpty_or_nonempty I

Premises used: isEmpty_or_nonempty
-- 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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : IsEmpty I
inl : ∀ (e : c.pt ≅ Spec (CommRingCat.of (ULift.{u, 0} ℤ))), Nonempty.{u + 1} ↥c.pt
⊢ Nonempty.{u + 1} ↥c.pt

Tactic:
have e := (isLimitEquivIsTerminalOfIsEmpty _ _ hc).uniqueUpToIso specULiftZIsTerminal
-- 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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : IsEmpty I
e : c.pt ≅ Spec (CommRingCat.of (ULift.{u, 0} ℤ))
⊢ Nonempty.{u + 1} ↥c.pt

Tactic:
Nonempty.map e.inv inferInstance

Premises used: CategoryTheory.ConcreteCategory.hom, inferInstance, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Nonempty.map, DFunLike.coe, CategoryTheory.Iso.inv
-- 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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : IsEmpty I
e : c.pt ≅ Spec (CommRingCat.of (ULift.{u, 0} ℤ))
⊢ Nonempty.{u + 1} ↥c.pt

Tactic:
exact Nonempty.map e.inv inferInstance

Premises used: CategoryTheory.ConcreteCategory.hom, inferInstance, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Nonempty.map, DFunLike.coe, CategoryTheory.Iso.inv
-- 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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : Nonempty I
inr : ∀ (i : I), Nonempty.{u + 1} ↥c.pt
⊢ Nonempty.{u + 1} ↥c.pt

Tactic:
have i := Nonempty.some ‹Nonempty I›
-- 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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : Nonempty I
i : I
⊢ IsCofiltered I

Tactic:
have : IsCofiltered I := ⟨⟩
-- 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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : Nonempty I
i : I
this : IsCofiltered I
𝒰 : (D.obj i).OpenCover := OpenCover.finiteSubcover (D.obj i).affineCover
⊢ ∀ (i' : 𝒰.I₀), IsAffine.{u} (𝒰.X i')

Tactic:
have (i' : _) : IsAffine (𝒰.X i') := inferInstanceAs (IsAffine (Spec _))
-- 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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : Nonempty I
i : I
this_1 : IsCofiltered I
𝒰 : (D.obj i).OpenCover := OpenCover.finiteSubcover (D.obj i).affineCover
this : ∀ (i' : 𝒰.I₀), IsAffine.{u} (𝒰.X i')
by_contra! :
  ∀
    (H :
      ∀ (j : 𝒰.I₀), ∃ (i' : I) (f : i' ⟶ i), IsEmpty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)),
    False
⊢ ∃ (j : 𝒰.I₀), ∀ {i' : I} (f : i' ⟶ i), Nonempty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)

Tactic:
by_contra! H
-- 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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : Nonempty I
i : I
this_1 : IsCofiltered I
𝒰 : (D.obj i).OpenCover := OpenCover.finiteSubcover (D.obj i).affineCover
this : ∀ (i' : 𝒰.I₀), IsAffine.{u} (𝒰.X i')
H : ∀ (j : 𝒰.I₀), ∃ (i' : I) (f : i' ⟶ i), IsEmpty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
choose :
  ∀ (i' : (j : 𝒰.I₀) → I) (f : (j : 𝒰.I₀) → i' j ⟶ i)
    (hf : ∀ (j : 𝒰.I₀), IsEmpty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)), False
⊢ False

Tactic:
choose i' f hf using H
-- 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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : Nonempty I
i : I
this_1 : IsCofiltered I
𝒰 : (D.obj i).OpenCover := OpenCover.finiteSubcover (D.obj i).affineCover
this : ∀ (i' : 𝒰.I₀), IsAffine.{u} (𝒰.X i')
i' : (j : 𝒰.I₀) → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
j_1 : I
j : 𝒰.I₀
⊢ i' j ∈ insert i (Finset.image i' Finset.univ)

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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : Nonempty I
i : I
this_1 : IsCofiltered I
𝒰 : (D.obj i).OpenCover := OpenCover.finiteSubcover (D.obj i).affineCover
this : ∀ (i' : 𝒰.I₀), IsAffine.{u} (𝒰.X i')
i' : (j : 𝒰.I₀) → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
j_1 : I
j : 𝒰.I₀
⊢ i ∈ insert i (Finset.image i' Finset.univ)

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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : Nonempty I
i : I
this_1 : IsCofiltered I
𝒰 : (D.obj i).OpenCover := OpenCover.finiteSubcover (D.obj i).affineCover
this : ∀ (i' : 𝒰.I₀), IsAffine.{u} (𝒰.X i')
i' : (j : 𝒰.I₀) → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  (m : j ∈ insert i (Finset.image i' Finset.univ)) →
    IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image
          (fun (j : 𝒰.I₀) ↦
            PSigma.mk (β := fun (X : I) ↦
              (Y : I) ×'
                (_ : X ∈ insert i (Finset.image i' Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image i' Finset.univ)) ×' (X ⟶ Y))
              (i' j)
              (PSigma.mk (β := fun (Y : I) ↦
                (_ : i' j ∈ insert i (Finset.image i' Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image i' Finset.univ)) ×' (i' j ⟶ Y))
                i
                (PSigma.mk (β := fun (x : i' j ∈ insert i (Finset.image i' Finset.univ)) ↦
                  (_ : i ∈ insert i (Finset.image i' Finset.univ)) ×' (i' j ⟶ i)) ⋯
                  (PSigma.mk (β := fun (x : i ∈ insert i (Finset.image i' Finset.univ)) ↦ i' j ⟶ i) ⋯ (f j)))))
          Finset.univ) ⟶
      j :=
  fun (j : I) ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image
        (fun (j : 𝒰.I₀) ↦
          PSigma.mk (β := fun (X : I) ↦
            (Y : I) ×'
              (_ : X ∈ insert i (Finset.image i' Finset.univ)) ×'
                (_ : Y ∈ insert i (Finset.image i' Finset.univ)) ×' (X ⟶ Y))
            (i' j)
            (PSigma.mk (β := fun (Y : I) ↦
              (_ : i' j ∈ insert i (Finset.image i' Finset.univ)) ×'
                (_ : Y ∈ insert i (Finset.image i' Finset.univ)) ×' (i' j ⟶ Y))
              i
              (PSigma.mk (β := fun (x : i' j ∈ insert i (Finset.image i' Finset.univ)) ↦
                (_ : i ∈ insert i (Finset.image i' Finset.univ)) ×' (i' j ⟶ i)) ⋯
                (PSigma.mk (β := fun (x : i ∈ insert i (Finset.image i' Finset.univ)) ↦ i' j ⟶ i) ⋯ (f j)))))
        Finset.univ)
j : 𝒰.I₀
⊢ i ∈ insert i (Finset.image i' Finset.univ)

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)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : Nonempty I
i : I
this_1 : IsCofiltered I
𝒰 : (D.obj i).OpenCover := OpenCover.finiteSubcover (D.obj i).affineCover
this : ∀ (i' : 𝒰.I₀), IsAffine.{u} (𝒰.X i')
i' : (j : 𝒰.I₀) → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  (m : j ∈ insert i (Finset.image i' Finset.univ)) →
    IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image
          (fun (j : 𝒰.I₀) ↦
            PSigma.mk (β := fun (X : I) ↦
              (Y : I) ×'
                (_ : X ∈ insert i (Finset.image i' Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image i' Finset.univ)) ×' (X ⟶ Y))
              (i' j)
              (PSigma.mk (β := fun (Y : I) ↦
                (_ : i' j ∈ insert i (Finset.image i' Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image i' Finset.univ)) ×' (i' j ⟶ Y))
                i
                (PSigma.mk (β := fun (x : i' j ∈ insert i (Finset.image i' Finset.univ)) ↦
                  (_ : i ∈ insert i (Finset.image i' Finset.univ)) ×' (i' j ⟶ i)) ⋯
                  (PSigma.mk (β := fun (x : i ∈ insert i (Finset.image i' Finset.univ)) ↦ i' j ⟶ i) ⋯ (f j)))))
          Finset.univ) ⟶
      j :=
  fun (j : I) ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image
        (fun (j : 𝒰.I₀) ↦
          PSigma.mk (β := fun (X : I) ↦
            (Y : I) ×'
              (_ : X ∈ insert i (Finset.image i' Finset.univ)) ×'
                (_ : Y ∈ insert i (Finset.image i' Finset.univ)) ×' (X ⟶ Y))
            (i' j)
            (PSigma.mk (β := fun (Y : I) ↦
              (_ : i' j ∈ insert i (Finset.image i' Finset.univ)) ×'
                (_ : Y ∈ insert i (Finset.image i' Finset.univ)) ×' (i' j ⟶ Y))
              i
              (PSigma.mk (β := fun (x : i' j ∈ insert i (Finset.image i' Finset.univ)) ↦
                (_ : i ∈ insert i (Finset.image i' Finset.univ)) ×' (i' j ⟶ i)) ⋯
                (PSigma.mk (β := fun (x : i ∈ insert i (Finset.image i' Finset.univ)) ↦ i' j ⟶ i) ⋯ (f j)))))
        Finset.univ)
j : 𝒰.I₀
⊢ i' j ∈ insert i (Finset.image i' Finset.univ)

Tactic:
simp