awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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 (↑(CommRingCat.of (ULift.{max u v, 0} ℤ)) : Type (max u v)) (↑ℤ[n] : Type (max u v))
have 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
Tactic: convert! (inferInstance : Algebra.FinitePresentation (ULift ℤ) ℤ[n])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S : Scheme
⊢ IsOpenMap (X := ↥(AffineSpace.{v, u} n S)) (Y := ↥S) ⇑(AffineSpace.{v, u} n S ↘ S)
have change : topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
Tactic: change topologically @IsOpenMap _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S : Scheme
⊢ topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
have 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)
Tactic: wlog hS : ∃ R, S = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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)
⊢ topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
have wlog : ∀ {n : Type v} (S : Scheme) (hS : ∃ (R : CommRingCat), S = Spec R),
  topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
Tactic: wlog hS : ∃ R, S = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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)
have 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)
Tactic: refine (IsZariskiLocalAtTarget.iff_of_openCover
      (P := topologically @IsOpenMap) S.affineCover).mpr ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (hypothesis)
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 (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)
have this₁ : 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⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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)
⊢ 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)
have inr : ∀
  (this :
    topologically (@IsOpenMap)
      (CategoryStruct.comp (Y := pullback (AffineSpace.{v, u} n S ↘ S) (S.affineCover.f i))
        (Iso.hom (IsPullback.isoPullback sorry)) (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)
Tactic: rwa [← (isPullback_map (n := n) (S.affineCover.f i)).isoPullback_hom_snd,
      MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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)
⊢ 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)
have 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)
Tactic: rwa [← (isPullback_map (n := n) (S.affineCover.f i)).isoPullback_hom_snd,
      MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n_1 : Type v
S_1 : Scheme
n : Type v
S : Scheme
hS : ∃ (R : CommRingCat), S = Spec R
⊢ topologically (@IsOpenMap) (AffineSpace.{v, u} n S ↘ S)
have obtain : ∀ (R : CommRingCat), topologically @IsOpenMap (Y := Spec R) (AffineSpace.{v, u} n (Spec R) ↘ Spec R)
Tactic: obtain ⟨R, rfl⟩ := hS
Cleared hypotheses: S, hS
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n_1 : Type v
S : Scheme
n : Type v
R : CommRingCat
⊢ topologically @IsOpenMap (Y := Spec R) (AffineSpace.{v, u} n (Spec R) ↘ Spec R)
have rw : topologically @IsOpenMap (X := Spec (CommRingCat.of (MvPolynomial n (↑R : Type (max u v)))))
  (Spec.map (CommRingCat.ofHom C))
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)
    (SpecIso n R).inv, SpecIso_inv_over]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsEmpty n
⊢ isomorphisms Scheme (Y := ⊤_ Scheme) (terminal.from (Spec ℤ[n]))
have rw : isomorphisms Scheme (X := Spec ℤ[n]) (Y := ⊤_ Scheme)
  (Spec.map (CommRingCat.ofHom C) ≫ terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
Tactic: rw [← terminal.comp_from (Spec.map (CommRingCat.ofHom C))]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsEmpty n
⊢ isomorphisms Scheme (X := Spec ℤ[n]) (Y := ⊤_ Scheme)
    (Spec.map (CommRingCat.ofHom C) ≫ terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
have a : isomorphisms Scheme (X := Spec ℤ[n]) (Spec.map (CommRingCat.ofHom C))
Tactic: apply IsStableUnderComposition.comp_mem
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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))
⊢ isomorphisms Scheme (X := Spec ℤ[n]) (Y := ⊤_ Scheme)
    (Spec.map (CommRingCat.ofHom C) ≫ terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
have a₁ : isomorphisms Scheme (Y := ⊤_ Scheme) (terminal.from (Spec (CommRingCat.of (ULift.{max u v, 0} ℤ))))
Tactic: apply IsStableUnderComposition.comp_mem
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S X : Scheme
inst : X.Over S
inst_1 : IsEmpty n
⊢ isomorphisms Scheme (X := Spec ℤ[n]) (Spec.map (CommRingCat.ofHom C))
have a : IsAffine (Spec ℤ[n]) ∧
  isomorphisms CommRingCat (X := CommRingCat.of (ULift.{max u v, 0} ℤ)) (Y := ℤ[n]) (CommRingCat.ofHom C)
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := isomorphisms _), ← isomorphisms,
      ← arrow_mk_iso_iff (isomorphisms _) (arrowIsoΓSpecOfIsAffine _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S : Scheme
⊢ IsIntegralHom (AffineSpace.{v, u} n S ↘ S) ↔ IsEmpty ↥S ∨ IsEmpty n
have mp : IsIntegralHom (AffineSpace.{v, u} n S ↘ S) → IsEmpty ↥S ∨ IsEmpty n
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S : Scheme
mp : IsIntegralHom (AffineSpace.{v, u} n S ↘ S) → IsEmpty ↥S ∨ IsEmpty n
⊢ IsIntegralHom (AffineSpace.{v, u} n S ↘ S) ↔ IsEmpty ↥S ∨ IsEmpty n
have mpr : IsEmpty ↥S ∨ IsEmpty n → IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
⊢ IsEmpty ↥S ∨ IsEmpty n
have mp : IsEmpty ↥S → IsEmpty ↥S ∨ IsEmpty n
Tactic: cases isEmpty_or_nonempty S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
mp : IsEmpty ↥S → IsEmpty ↥S ∨ IsEmpty n
⊢ IsEmpty ↥S ∨ IsEmpty n
have mp₁ : Nonempty ↥S → IsEmpty ↥S ∨ IsEmpty n
Tactic: cases isEmpty_or_nonempty S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : Nonempty ↥S
⊢ IsEmpty ↥S ∨ IsEmpty n
have mp : IsEmpty n
Tactic: refine .inr ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
Goal:
n : Type v
S : Scheme
h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)
h_1 : Nonempty ↥S
⊢ IsEmpty n
have 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
Tactic: wlog hS : ∃ R, S = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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
⊢ IsEmpty n
have wlog : ∀ {n : Type v} (S : Scheme) (h : IsIntegralHom (AffineSpace.{v, u} n S ↘ S)),
  Nonempty ↥S → ∀ (hS : ∃ (R : CommRingCat), S = Spec R), IsEmpty n
Tactic: wlog hS : ∃ R, S = Spec R
Cleared hypotheses: h, h_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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
⊢ IsEmpty n
have mp : ∀ (x : ↥S), IsEmpty n
Tactic: obtain ⟨x⟩ := ‹Nonempty S›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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
⊢ IsEmpty n
have 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
Tactic: obtain ⟨y, hy⟩ := S.affineCover.covers x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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
⊢ IsEmpty n
have obtain : ∀ (R : CommRingCat) (h : IsIntegralHom (Y := Spec R) (AffineSpace.{v, u} n (Spec R) ↘ Spec R)),
  Nonempty ↥(Spec R) → IsEmpty n
Tactic: obtain ⟨R, rfl⟩ := hS
Cleared hypotheses: S, h, h_1, hS
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (hypothesis)
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)
⊢ IsEmpty n
have this : 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)))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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))
⊢ IsEmpty n
have false : ∀ (a : n), False
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (hypothesis)
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
⊢ False
have this₁ : (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}
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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
have 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
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso @IsIntegralHom (SpecIso n R).inv,
      SpecIso_inv_over, HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom)] at h
Cleared hypotheses: h, h_1, this_1, i, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (goal)
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
have 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
Tactic: obtain ⟨p : Polynomial R, hp, hp'⟩ :=
      (MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
        (arrowIsoΓSpecOfIsAffine _)).mpr h.2 (X i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (hypothesis)
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
⊢ False
have 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)))
Tactic: have : (rename fun _ ↦ i).comp (uniqueAlgEquiv.{_, v} _ PUnit).symm.toAlgHom p = 0 := by
      simp [← hp', ← algebraMap_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (hypothesis)
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)))
⊢ False
have 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)))
Tactic: rw [AlgHom.comp_apply, map_eq_zero_iff _ (rename_injective _ (fun _ _ _ ↦ rfl))] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineSpace (hypothesis)
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)))
⊢ False
have this₁ : p = 0
Tactic: simp only [AlgEquiv.coe_algHom, EmbeddingLike.map_eq_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
⊢ Nonempty.{u + 1} ↥c.pt
have inl : IsEmpty I → Nonempty.{u + 1} ↥c.pt
Tactic: cases isEmpty_or_nonempty I
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inl : IsEmpty I → Nonempty.{u + 1} ↥c.pt
⊢ Nonempty.{u + 1} ↥c.pt
have inr : Nonempty I → Nonempty.{u + 1} ↥c.pt
Tactic: cases isEmpty_or_nonempty I
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), Nonempty.{u + 1} ↥(D.obj i)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
h : IsEmpty I
⊢ Nonempty.{u + 1} ↥c.pt
have inl : ∀ (e : c.pt ≅ Spec (CommRingCat.of (ULift.{u, 0} ℤ))), Nonempty.{u + 1} ↥c.pt
Tactic: have e := (isLimitEquivIsTerminalOfIsEmpty _ _ hc).uniqueUpToIso specULiftZIsTerminal