awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
X_1 Y Z : Type vᵒᵖ
f : X_1 ⟶ Y
g : Y ⟶ Z
x : Scheme
⊢ Eq (α := AffineSpace.{v, u} (Opposite.unop X_1) x ⟶ AffineSpace.{v, u} (Opposite.unop Z) x)
    (reindex (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (g.unop ≫ f.unop)) : (a : Opposite.unop Z) → Opposite.unop X_1)
      x)
    (CategoryStruct.comp (Y := AffineSpace.{v, u} (Opposite.unop Y) x)
      (reindex (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.unop) : (a : Opposite.unop Y) → Opposite.unop X_1) x)
      (reindex (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g.unop) : (a : Opposite.unop Z) → Opposite.unop Y) x))

Tactic:
exact reindex_comp _ _ _

Premises used: AlgebraicGeometry.AffineSpace.reindex_comp
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
⊢ IsAffineHom (AffineSpace.{v, u} n S ↘ S)

Tactic:
MorphismProperty.pullback_fst _ _ inferInstance

Premises used: CategoryTheory.Limits.limit.π, AlgebraicGeometry.AffineSpace, inferInstance, CategoryTheory.MorphismProperty.pullback_fst, CategoryTheory.over
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
⊢ IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))

Tactic:
have := isIso_of_isTerminal specULiftZIsTerminal terminalIsTerminal (terminal.from _)
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
rw : Surjective (X := Spec ℤ[n]) (Spec.map (CommRingCat.ofHom C))
⊢ Surjective (Y := ⊤_ Scheme) (terminal.from (Spec ℤ[n]))

Tactic:
rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),
    MorphismProperty.cancel_right_of_respectsIso (P := @Surjective)]

Premises used: CommRingCat.ofHom, AlgebraicGeometry.Spec.map, CategoryTheory.Limits.terminal.comp_from, AlgebraicGeometry.Surjective, MvPolynomial.C, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
⊢ Surjective (X := Spec ℤ[n]) (Spec.map (CommRingCat.ofHom C))

Tactic:
⟨MvPolynomial.comap_C_surjective⟩

Premises used: MvPolynomial.comap_C_surjective, AlgebraicGeometry.Surjective.mk
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : Finite n
⊢ IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))

Tactic:
have := isIso_of_isTerminal specULiftZIsTerminal.{max u v} terminalIsTerminal (terminal.from _)
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : Finite n
this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
rw : Algebra.FinitePresentation (↑(CommRingCat.of (ULift.{max u v, 0} ℤ)) : Type (max u v)) (↑ℤ[n] : Type (max u v))
⊢ LocallyOfFinitePresentation (Y := ⊤_ Scheme) (terminal.from (Spec ℤ[n]))

Tactic:
rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C)),
    MorphismProperty.cancel_right_of_respectsIso (P := @LocallyOfFinitePresentation),
    HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation), RingHom.FinitePresentation]

Premises used: RingHom.FinitePresentation, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, CategoryTheory.Limits.terminal.comp_from, AlgebraicGeometry.HasRingHomProperty.Spec_iff, MvPolynomial.C, AlgebraicGeometry.LocallyOfFinitePresentation, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : Finite n
this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
⊢ Algebra.FinitePresentation (ULift.{max u v, 0} ℤ) (↑ℤ[n] : Type (max u v))

Tactic:
(inferInstance : Algebra.FinitePresentation (ULift ℤ) ℤ[n])

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : Finite n
this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
h :
  Eq (α := CommSemiring (↑(CommRingCat.of (ULift.{max u v, 0} ℤ)) : Type (max u v))) CommRing.toCommSemiring
      ULift.commSemiring →
    Eq (α := Semiring (↑ℤ[n] : Type (max u v))) CommSemiring.toSemiring AddMonoidAlgebra.semiring →
      Eq (α := Algebra (↑(CommRingCat.of (ULift.{max u v, 0} ℤ)) : Type (max u v)) (↑ℤ[n] : Type (max u v)))
        (RingHom.toAlgebra (CommRingCat.Hom.hom (CommRingCat.ofHom C))) AddMonoidAlgebra.algebra
⊢ Algebra.FinitePresentation (↑(CommRingCat.of (ULift.{max u v, 0} ℤ)) : Type (max u v)) (↑ℤ[n] : Type (max u v))

Tactic:
convert! (inferInstance : Algebra.FinitePresentation (ULift ℤ) ℤ[n])

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : Finite n
this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
e_3 :
  Eq (α := CommSemiring (↑(CommRingCat.of (ULift.{max u v, 0} ℤ)) : Type (max u v))) CommRing.toCommSemiring
    ULift.commSemiring
e_4 : Eq (α := Semiring (↑ℤ[n] : Type (max u v))) CommSemiring.toSemiring AddMonoidAlgebra.semiring
⊢ Eq (α := Algebra (↑(CommRingCat.of (ULift.{max u v, 0} ℤ)) : Type (max u v)) (↑ℤ[n] : Type (max u v)))
    (RingHom.toAlgebra (CommRingCat.Hom.hom (CommRingCat.ofHom C))) AddMonoidAlgebra.algebra

Tactic:
Algebra.algebra_ext _ _ fun _ ↦ rfl

Premises used: Algebra.algebra_ext, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : Finite n
this : IsIso (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
e_3 :
  Eq (α := CommSemiring (↑(CommRingCat.of (ULift.{max u v, 0} ℤ)) : Type (max u v))) CommRing.toCommSemiring
    ULift.commSemiring
e_4 : Eq (α := Semiring (↑ℤ[n] : Type (max u v))) CommSemiring.toSemiring AddMonoidAlgebra.semiring
⊢ Eq (α := Algebra (↑(CommRingCat.of (ULift.{max u v, 0} ℤ)) : Type (max u v)) (↑ℤ[n] : Type (max u v)))
    (RingHom.toAlgebra (CommRingCat.Hom.hom (CommRingCat.ofHom C))) AddMonoidAlgebra.algebra

Tactic:
exact Algebra.algebra_ext _ _ fun _ ↦ rfl

Premises used: Algebra.algebra_ext, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
change : topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
⊢ IsOpenMap (X := ↥(AffineSpace.{v, u} n S)) (Y := ↥S) ⇑(AffineSpace.{v, u} n S ↘ S)

Tactic:
change topologically @IsOpenMap _

Premises used: IsOpenMap, AlgebraicGeometry.topologically
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
inr :
  ∀
    (this :
      ∀ {n : Type v} (S : Scheme) (hS : ∃ (R : CommRingCat), S = Spec R),
        topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S))
    (hS : ¬∃ (R : CommRingCat), S = Spec R), topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
wlog :
  ∀ {n : Type v} (S : Scheme) (hS : ∃ (R : CommRingCat), S = Spec R),
    topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
⊢ topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)

Tactic:
wlog hS : ∃ R, S = Spec R
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
this :
  ∀ {n : Type v} (S : Scheme) (hS : ∃ (R : CommRingCat), S = Spec R),
    topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
hS : ¬∃ (R : CommRingCat), S = Spec R
⊢ topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)

Tactic:
(IsZariskiLocalAtTarget.iff_of_openCover
      (P := topologically @IsOpenMap) S.affineCover).mpr ?_

Premises used: Iff.mpr, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
this :
  ∀ {n : Type v} (S : Scheme) (hS : ∃ (R : CommRingCat), S = Spec R),
    topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
hS : ¬∃ (R : CommRingCat), S = Spec R
inr :
  ∀ (i : S.affineCover.toPreZeroHypercover.1),
    topologically @IsOpenMap (X :=
      (Precoverage.ZeroHypercover.pullback₁ (AffineSpace.{v, u} n S ↘ S) S.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) S.affineCover (AffineSpace.{v, u} n S ↘ S) i :
        (Precoverage.ZeroHypercover.pullback₁ (AffineSpace.{v, u} n S ↘ S) S.affineCover).X i ⟶ S.affineCover.X i)
⊢ topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)

Tactic:
refine (IsZariskiLocalAtTarget.iff_of_openCover
      (P := topologically @IsOpenMap) S.affineCover).mpr ?_

Premises used: Iff.mpr, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
this :
  ∀ {n : Type v} (S : Scheme) (hS : ∃ (R : CommRingCat), S = Spec R),
    topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
hS : ¬∃ (R : CommRingCat), S = Spec R
i : S.affineCover.toPreZeroHypercover.1
⊢ topologically @IsOpenMap (Y := S.affineCover.X i) (AffineSpace.{v, u} n (S.affineCover.X i) ↘ S.affineCover.X i)

Tactic:
have := this (n := n) (S.affineCover.X i) ⟨_, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
this_1 :
  ∀ {n : Type v} (S : Scheme) (hS : ∃ (R : CommRingCat), S = Spec R),
    topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
hS : ¬∃ (R : CommRingCat), S = Spec R
i : S.affineCover.toPreZeroHypercover.1
this : topologically @IsOpenMap (Y := S.affineCover.X i) (AffineSpace.{v, u} n (S.affineCover.X i) ↘ S.affineCover.X i)
inr :
  ∀
    (this :
      topologically (@IsOpenMap)
        (CategoryStruct.comp (Y := pullback (AffineSpace.{v, u} n S ↘ S) (S.affineCover.f i))
          (Iso.hom (IsPullback.isoPullback ⋯)) (pullback.snd (AffineSpace.{v, u} n S ↘ S) (S.affineCover.f i)))),
    topologically @IsOpenMap (X :=
      (Precoverage.ZeroHypercover.pullback₁ (AffineSpace.{v, u} n S ↘ S) S.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) S.affineCover (AffineSpace.{v, u} n S ↘ S) i :
        (Precoverage.ZeroHypercover.pullback₁ (AffineSpace.{v, u} n S ↘ S) S.affineCover).X i ⟶ S.affineCover.X i)
inr₁ inr₂ inr₃ inr₄ :
  ∀
    (this :
      topologically @IsOpenMap (X := pullback (AffineSpace.{v, u} n S ↘ S) (S.affineCover.f i))
        (pullback.snd (AffineSpace.{v, u} n S ↘ S) (S.affineCover.f i))),
    topologically @IsOpenMap (X :=
      (Precoverage.ZeroHypercover.pullback₁ (AffineSpace.{v, u} n S ↘ S) S.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) S.affineCover (AffineSpace.{v, u} n S ↘ S) i :
        (Precoverage.ZeroHypercover.pullback₁ (AffineSpace.{v, u} n S ↘ S) S.affineCover).X i ⟶ S.affineCover.X i)
⊢ topologically @IsOpenMap (X := (Precoverage.ZeroHypercover.pullback₁ (AffineSpace.{v, u} n S ↘ S) S.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) S.affineCover (AffineSpace.{v, u} n S ↘ S) i :
      (Precoverage.ZeroHypercover.pullback₁ (AffineSpace.{v, u} n S ↘ S) S.affineCover).X i ⟶ S.affineCover.X i)

Tactic:
rwa [← (isPullback_map (n := n) (S.affineCover.f i)).isoPullback_hom_snd,
      MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)] at this

Premises used: CategoryTheory.PreZeroHypercover.f, IsOpenMap, AlgebraicGeometry.topologically, AlgebraicGeometry.AffineSpace.isPullback_map, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.IsPullback.isoPullback_hom_snd, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S_1 : Scheme
n : Type v
S : Scheme
hS : ∃ (R : CommRingCat), S = Spec R
obtain : ∀ (R : CommRingCat), topologically @IsOpenMap (Y := Spec R) (AffineSpace.{v, u} n (Spec R) ↘ Spec R)
⊢ topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)

Tactic:
obtain ⟨R, rfl⟩ := hS

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S : Scheme
n : Type v
R : CommRingCat
rw :
  topologically @IsOpenMap (X := Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))))
    (Spec.map (CommRingCat.ofHom C))
⊢ topologically @IsOpenMap (Y := Spec R) (AffineSpace.{v, u} n (Spec R) ↘ Spec R)

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)
    (SpecIso n R).inv, SpecIso_inv_over]

Premises used: AlgebraicGeometry.AffineSpace.SpecIso, IsOpenMap, AlgebraicGeometry.topologically, 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
⊢ topologically @IsOpenMap (X := Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))))
    (Spec.map (CommRingCat.ofHom C))

Tactic:
MvPolynomial.isOpenMap_comap_C

Premises used: MvPolynomial.isOpenMap_comap_C, Set.Mem, setOf, AlgebraicGeometry.topologically, AddMonoidAlgebra, PrimeSpectrum.comap, MvPolynomial.C
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S : Scheme
n : Type v
R : CommRingCat
⊢ topologically @IsOpenMap (X := Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))))
    (Spec.map (CommRingCat.ofHom C))

Tactic:
exact MvPolynomial.isOpenMap_comap_C

Premises used: MvPolynomial.isOpenMap_comap_C
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsEmpty n
rw :
  isomorphisms Scheme (X := Spec ℤ[n]) (Y := ⊤_ Scheme)
    (Spec.map (CommRingCat.ofHom C) ≫ terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
⊢ isomorphisms Scheme (Y := ⊤_ Scheme) (terminal.from (Spec ℤ[n]))

Tactic:
rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C))]

Premises used: CommRingCat.ofHom, AlgebraicGeometry.Spec.map, CategoryTheory.Limits.terminal.comp_from, MvPolynomial.C
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsEmpty n
a : isomorphisms Scheme (X := Spec ℤ[n]) (Spec.map (CommRingCat.ofHom C))
a₁ : isomorphisms Scheme (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
⊢ isomorphisms Scheme (X := Spec ℤ[n]) (Y := ⊤_ Scheme)
    (Spec.map (CommRingCat.ofHom C) ≫ terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))

Tactic:
apply IsStableUnderComposition.comp_mem

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsEmpty n
a :
  IsAffine (Spec ℤ[n]) ∧
    isomorphisms CommRingCat (X := CommRingCat.of (ULift.{max u v, 0} ℤ)) (Y := ℤ[n]) (CommRingCat.ofHom C)
⊢ isomorphisms Scheme (X := Spec ℤ[n]) (Spec.map (CommRingCat.ofHom C))

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := isomorphisms _), ← isomorphisms,
      ← arrow_mk_iso_iff (isomorphisms _) (arrowIsoΓSpecOfIsAffine _)]

Premises used: CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, AlgebraicGeometry.arrowIsoΓSpecOfIsAffine
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsEmpty n
⊢ IsAffine (Spec ℤ[n]) ∧
    isomorphisms CommRingCat (X := CommRingCat.of (ULift.{max u v, 0} ℤ)) (Y := ℤ[n]) (CommRingCat.ofHom C)

Tactic:
⟨inferInstance, (ConcreteCategory.isIso_iff_bijective _).mpr
      ⟨C_injective n _, C_surjective _⟩⟩

Premises used: Iff.mpr, inferInstance, MvPolynomial.C_surjective, CategoryTheory.ConcreteCategory.isIso_iff_bijective, And.intro, MvPolynomial.C_injective
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsEmpty n
⊢ IsAffine (Spec ℤ[n]) ∧
    isomorphisms CommRingCat (X := CommRingCat.of (ULift.{max u v, 0} ℤ)) (Y := ℤ[n]) (CommRingCat.ofHom C)

Tactic:
exact ⟨inferInstance, (ConcreteCategory.isIso_iff_bijective _).mpr
      ⟨C_injective n _, C_surjective _⟩⟩
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsEmpty n
⊢ isomorphisms Scheme (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))

Tactic:
isIso_of_isTerminal specULiftZIsTerminal terminalIsTerminal (terminal.from _)

Premises used: AlgebraicGeometry.specULiftZIsTerminal, CategoryTheory.Limits.isIso_of_isTerminal, CategoryTheory.Limits.terminal.from, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsEmpty n
⊢ isomorphisms Scheme (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))

Tactic:
exact isIso_of_isTerminal specULiftZIsTerminal terminalIsTerminal (terminal.from _)

Premises used: AlgebraicGeometry.specULiftZIsTerminal, CategoryTheory.Limits.isIso_of_isTerminal, CategoryTheory.Limits.terminal.from, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
mp : IsIntegralHom (AffineSpace.{v, u} n S ↘ S) → IsEmpty ↥S ∨ IsEmpty n
mpr : IsEmpty ↥S ∨ IsEmpty n → IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
⊢ IsIntegralHom (AffineSpace.{v, u} n S ↘ S) ↔ IsEmpty ↥S ∨ IsEmpty n

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
mp : IsEmpty ↥S → IsEmpty ↥S ∨ IsEmpty n
mp₁ : Nonempty ↥S → IsEmpty ↥S ∨ IsEmpty n
⊢ IsEmpty ↥S ∨ IsEmpty n

Tactic:
cases isEmpty_or_nonempty S

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, isEmpty_or_nonempty, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : IsEmpty ↥S
⊢ IsEmpty ↥S ∨ IsEmpty n

Tactic:
.inl ‹_›

Premises used: Or.inl
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : IsEmpty ↥S
⊢ IsEmpty ↥S ∨ IsEmpty n

Tactic:
exact .inl ‹_›
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : Nonempty ↥S
⊢ IsEmpty ↥S ∨ IsEmpty n

Tactic:
.inr ?_

Premises used: Or.inr
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : Nonempty ↥S
mp : IsEmpty n
⊢ IsEmpty ↥S ∨ IsEmpty n

Tactic:
refine .inr ?_
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : Nonempty ↥S
mp :
  ∀
    (this :
      ∀ {n : Type v} (S : Scheme) (h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)),
        Nonempty ↥S → ∀ (hS : ∃ (R : CommRingCat), S = Spec R), IsEmpty n)
    (hS : ¬∃ (R : CommRingCat), S = Spec R), IsEmpty n
wlog :
  ∀ {n : Type v} (S : Scheme) (h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)),
    Nonempty ↥S → ∀ (hS : ∃ (R : CommRingCat), S = Spec R), IsEmpty n
⊢ IsEmpty n

Tactic:
wlog hS : ∃ R, S = Spec R
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : Nonempty ↥S
this :
  ∀ {n : Type v} (S : Scheme) (h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)),
    Nonempty ↥S → ∀ (hS : ∃ (R : CommRingCat), S = Spec R), IsEmpty n
hS : ¬∃ (R : CommRingCat), S = Spec R
mp : ∀ (x : ↥S), IsEmpty n
⊢ IsEmpty n

Tactic:
obtain ⟨x⟩ := ‹Nonempty S›

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, Nonempty, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : Nonempty ↥S
this :
  ∀ {n : Type v} (S : Scheme) (h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)),
    Nonempty ↥S → ∀ (hS : ∃ (R : CommRingCat), S = Spec R), IsEmpty n
hS : ¬∃ (R : CommRingCat), S = Spec R
x : ↥S
mp :
  ∀ (y : ↥(S.affineCover.X (Scheme.Cover.idx S.affineCover x)))
    (hy : (S.affineCover.f (Scheme.Cover.idx S.affineCover x)) y = x), IsEmpty n
⊢ IsEmpty n

Tactic:
obtain ⟨y, hy⟩ := S.affineCover.covers x

Premises used: AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : Nonempty ↥S
this :
  ∀ {n : Type v} (S : Scheme) (h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)),
    Nonempty ↥S → ∀ (hS : ∃ (R : CommRingCat), S = Spec R), IsEmpty n
hS : ¬∃ (R : CommRingCat), S = Spec R
x : ↥S
y : ↥(S.affineCover.X (Scheme.Cover.idx S.affineCover x))
hy : (S.affineCover.f (Scheme.Cover.idx S.affineCover x)) y = x
⊢ IsEmpty n

Tactic:
this (S.affineCover.X _) (MorphismProperty.IsStableUnderBaseChange.of_isPullback
        (isPullback_map (S.affineCover.f _)) h) ⟨y⟩ ⟨_, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.AffineSpace.isPullback_map, Nonempty.intro, Exists.intro, CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : Nonempty ↥S
this :
  ∀ {n : Type v} (S : Scheme) (h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)),
    Nonempty ↥S → ∀ (hS : ∃ (R : CommRingCat), S = Spec R), IsEmpty n
hS : ¬∃ (R : CommRingCat), S = Spec R
x : ↥S
y : ↥(S.affineCover.X (Scheme.Cover.idx S.affineCover x))
hy : (S.affineCover.f (Scheme.Cover.idx S.affineCover x)) y = x
⊢ IsEmpty n

Tactic:
exact this (S.affineCover.X _) (MorphismProperty.IsStableUnderBaseChange.of_isPullback
        (isPullback_map (S.affineCover.f _)) h) ⟨y⟩ ⟨_, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.AffineSpace.isPullback_map, Nonempty.intro, Exists.intro, CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineSpace
Goal:
n_1 : Type v
S_1 : Scheme
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : Nonempty ↥S
hS : ∃ (R : CommRingCat), S = Spec R
obtain :
  ∀ (R : CommRingCat) (h : IsIntegralHom (Y := Spec R) (AffineSpace.{v, u} n (Spec R) ↘ Spec R)),
    Nonempty ↥(Spec R) → IsEmpty n
⊢ IsEmpty n

Tactic:
obtain ⟨R, rfl⟩ := hS

Premises used: rfl
-- 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)
⊢ Nontrivial (↑R : Type (max u v))

Tactic:
have : Nontrivial R := (subsingleton_or_nontrivial R).resolve_left fun H ↦
        not_isEmpty_of_nonempty (Spec R) (inferInstanceAs (IsEmpty (PrimeSpectrum R)))
-- 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 : Nontrivial (↑R : Type (max u v))
false : ∀ (a : n), False
⊢ IsEmpty n

Tactic:
constructor
-- 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 : Nontrivial (↑R : Type (max u v))
i : n
⊢ (RingHom.toMorphismProperty fun {R S : Type (max u v)} [CommRing R] [CommRing S] (f : R →+* S) ↦
      f.IsIntegral).RespectsIso

Tactic:
have := RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.isIntegral_respectsIso.{max u v}