mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case inr
X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f],
    (∃ R, X = Spec R) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hX : ¬∃ R, X = Spec R
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)

pp: X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
hX : ∃ R, X = Spec R
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)

Tactic:
· intro x hx
      have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
      let 𝒰 := X.affineCover.finiteSubcover
      obtain ⟨_, ⟨i, rfl⟩, hx⟩ := (f.iUnion_support_ker_openCover_map_comp 𝒰).ge hx
      have inst : QuasiCompact (𝒰.f i ≫ f) := HasAffineProperty.iff_of_isAffine.mpr
        (inferInstanceAs <| CompactSpace (Spec _))
      exact closure_mono (Set.range_comp_subset_range _ _) (this S (𝒰.f i ≫ f) ⟨_, rfl⟩ hx)

Goal state after:
X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
hX : ∃ R, X = Spec R
⊢ ↑(ker f).support ⊆ closure (Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_1
X : Scheme
I : X.IdealSheafData
x : ↥I.glueData.glued
⊢ I.gluedTo x ∈ ↑I.support

Tactic:
obtain ⟨ix, x : I.glueDataObj ix, rfl⟩ :=
      I.glueData.toGlueData.ι_jointly_surjective forget x

Goal state after:
case refine_1
X : Scheme
I : X.IdealSheafData
ix : I.glueData.J
x : ↥(I.glueDataObj ix)
⊢ I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ix))) x) ∈ ↑I.support
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf : ∀ (U : ↑Y.affineOpens), IsAffine ↑(f ⁻¹ᵁ ↑U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
obtain ⟨hfU, hf⟩ := hf ⟨U, hU⟩
    use hfU
    have hf : Q (Scheme.Hom.app f (((⟨U, hU⟩ : Y.affineOpens) : Y.Opens).ι ''ᵁ ⊤)).hom := hf
    rwa [Scheme.Opens.ι_image_top] at hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case a.inl
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx : x ∈ f ⁻¹ᵁ W
⊢ i ((coprodMk ↑(f ⁻¹ᵁ W) ↑(g ⁻¹ᵁ W)) (Sum.inl ⟨x, hx⟩)) ∈ coprod.desc f g ⁻¹ᵁ W

Tactic:
simpa [← Scheme.Hom.comp_apply, i] using hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case a.inr
X✝ Y Z : Scheme
f✝ : X✝ ⟶ Y
g✝ : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this✝ : IsAffine ↑(f ⁻¹ᵁ W)
this : IsAffine ↑(g ⁻¹ᵁ W)
i : ↑(f ⁻¹ᵁ W) ⨿ ↑(g ⁻¹ᵁ W) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx : x ∈ g ⁻¹ᵁ W
⊢ i ((coprodMk ↑(f ⁻¹ᵁ W) ↑(g ⁻¹ᵁ W)) (Sum.inr ⟨x, hx⟩)) ∈ coprod.desc f g ⁻¹ᵁ W

Tactic:
simpa [← Scheme.Hom.comp_apply, i] using hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ ↑(f ⁻¹ᵁ U')
hVU : ↑(f ⁻¹ᵁ U') ⊆ ↑(f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
hrU' : Y.basicOpen r ≤ U'
hxr : ↑⟨f x, hxV⟩ ∈ Y.basicOpen r
⊢ f ⁻¹ᵁ Y.basicOpen r =
    X.basicOpen
      ((ConcreteCategory.hom (Scheme.Hom.app f U')) ((ConcreteCategory.hom (Y.presheaf.map (homOfLE hU'U).op)) r))

Tactic:
simp only [Scheme.preimage_basicOpen, ← CommRingCat.comp_apply, f.naturality]

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ ↑(f ⁻¹ᵁ U')
hVU : ↑(f ⁻¹ᵁ U') ⊆ ↑(f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
hrU' : Y.basicOpen r ≤ U'
hxr : ↑⟨f x, hxV⟩ ∈ Y.basicOpen r
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r) =
    X.basicOpen
      ((ConcreteCategory.hom (Scheme.Hom.app f U ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE hU'U).op.unop).op))
        r)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ Hom.app f ↑U ≫ e.hom = (ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)

Tactic:
rw [← (Iso.inv_comp_eq _).mpr U.2.isoSpec_inv_appTop, Category.assoc, Iso.eq_inv_comp]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ (↑U).topIso.hom ≫ Hom.app f ↑U ≫ e.hom =
    Hom.appTop (IsAffineOpen.isoSpec ⋯).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
this : Epi (app (ker f).subschemeι ↑U)
⊢ app f ↑U = app f ↑U ≫ 𝟙 Γ(X, (Opens.map (toImage f).base).obj ((Opens.map (imageι f).base).obj ↑U))

Tactic:
exact (Category.comp_id _).symm

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
⊢ FiniteType R S

Tactic:
let := fun r : s => (Localization.awayMap (algebraMap R S) r).toAlgebra

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away ((algebraMap R S) ↑r)) :=
  fun r ↦ (Localization.awayMap (algebraMap R S) ↑r).toAlgebra
⊢ FiniteType R S
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: R S : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FiniteType R S

Tactic:
exact IsLocalization.finiteType_of_monoid_fg (Submonoid.powers r) S

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
this :
  ∀ (q : ↥(Spec (unop (F.obj S)))),
    ∃ f, q ∈ PrimeSpectrum.basicOpen f ∧ Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen f)
⊢ ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))

Tactic:
choose f hqf hf using this

Goal state after:
case refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
⊢ IsClosedImmersion ((Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)))

Tactic:
← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _
    (Over.prodLeftIsoPullback Y Y).hom

Goal state after:
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z
S : Scheme
X Y : Over S
inst✝ : IsSeparated Y.hom
f g : X ⟶ Y
⊢ IsClosedImmersion ((Over.forget S).map (prod.lift (𝟙 Y) (𝟙 Y)) ≫ (Y.prodLeftIsoPullback Y).hom)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
h : IsLocallyNoetherian X
i : 𝒰.I₀
U : X.Opens := Scheme.Hom.opensRange (𝒰.f i)
⊢ IsNoetherianRing ↑Γ(𝒰.X i, ⊤)

Tactic:
have := h.component_noetherian ⟨U, isAffineOpen_opensRange _⟩

Goal state after:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
h : IsLocallyNoetherian X
i : 𝒰.I₀
U : X.Opens := Scheme.Hom.opensRange (𝒰.f i)
this : IsNoetherianRing ↑Γ(X, ↑⟨U, ⋯⟩)
⊢ IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
H : ∀ (i : ι), IsArtinianRing ↑Γ(X, U i)
⊢ ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsLocallyArtinian ((X.openCoverOfIsOpenCover U hU).X i)

Tactic:
have : ∀ i, IsLocallyArtinian (Spec Γ(X, U i)) := by simpa

Goal state after:
X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
H : ∀ (i : ι), IsArtinianRing ↑Γ(X, U i)
this : ∀ (i : ι), IsLocallyArtinian (Spec Γ(X, U i))
⊢ ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsLocallyArtinian ((X.openCoverOfIsOpenCover U hU).X i)
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: case refine_2
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ Spec ((Spec (CommRingCat.of R)).residueField p) ≅ Spec (CommRingCat.of p.asIdeal.ResidueField)

pp: case refine_3
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ (pullbackSymmetry (map (CommRingCat.ofHom (algebraMap R S))) ((Spec (CommRingCat.of R)).fromSpecResidueField p) ≪≫
          (pullback.congrHom ⋯ ⋯ ≪≫
              asIso
                (pullback.map
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv ≫
                    map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R)) p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv) (𝟙 (Spec (CommRingCat.of S)))
                  (𝟙 (Spec (CommRingCat.of R))) ⋯ ⋯)) ≪≫
            pullbackSpecIso R p.asIdeal.ResidueField S).hom ≫
      map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))) =
    Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p ≫ Iso.hom ?refine_2

Tactic:
· exact Scheme.Spec.mapIso (Scheme.Spec.residueFieldIso (.of R) _).symm.op

Goal state after:
case refine_3
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ (pullbackSymmetry (map (CommRingCat.ofHom (algebraMap R S))) ((Spec (CommRingCat.of R)).fromSpecResidueField p) ≪≫
          (pullback.congrHom ⋯ ⋯ ≪≫
              asIso
                (pullback.map
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv ≫
                    map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R)) p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv) (𝟙 (Spec (CommRingCat.of S)))
                  (𝟙 (Spec (CommRingCat.of R))) ⋯ ⋯)) ≪≫
            pullbackSpecIso R p.asIdeal.ResidueField S).hom ≫
      map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))) =
    Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p ≫
      (Scheme.Spec.mapIso (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).symm.op).hom
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝⁴ : IrreducibleSpace ↥(Spec R)
this✝³ : IsDomain ↑R
φ : S ⟶ R
this✝² : IsField ↑R
this✝¹ : Field ↑R := this✝².toField
this✝ : Algebra ↑S ↑R := (CommRingCat.Hom.hom φ).toAlgebra
this : IsJacobsonRing ↑S
⊢ (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType

Tactic:
change Module.Finite _ _ ↔ Algebra.FiniteType _ _

Goal state after:
case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝⁴ : IrreducibleSpace ↥(Spec R)
this✝³ : IsDomain ↑R
φ : S ⟶ R
this✝² : IsField ↑R
this✝¹ : Field ↑R := this✝².toField
this✝ : Algebra ↑S ↑R := (CommRingCat.Hom.hom φ).toAlgebra
this : IsJacobsonRing ↑S
⊢ Module.Finite ↑S ↑R ↔ Algebra.FiniteType ↑S ↑R
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
⊢ X.IsQuasiAffine

Tactic:
by
  have := QuasiCompact.compactSpace_of_compactSpace f
  refine .of_forall_exists_mem_basicOpen _ fun x ↦ ?_
  obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, -⟩ := (IsQuasiAffine.isBasis_basicOpen
    Y).exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
  refine ⟨f.appTop r, ?_⟩
  rw [← preimage_basicOpen_top]
  exact ⟨hr.preimage _, hxr⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case inr
n : Type u
S : Scheme
this✝ : ∀ {n : Type u} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
i : S.affineCover.toPreZeroHypercover.1
this : topologically (@IsOpenMap) (𝔸(n; S.affineCover.X i) ↘ S.affineCover.X i)
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)

Tactic:
← (isPullback_map (n := n) (S.affineCover.f i)).isoPullback_hom_snd,

Goal state after:
case inr
n : Type u
S : Scheme
this✝ : ∀ {n : Type u} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
i : S.affineCover.toPreZeroHypercover.1
this : topologically (@IsOpenMap) (⋯.isoPullback.hom ≫ pullback.snd (𝔸(n; S) ↘ S) (S.affineCover.f i))
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↥(Spec R)
this✝ : Nontrivial ↑R
i : n
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ False

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

Goal state after:
n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↥(Spec R)
this✝ : Nontrivial ↑R
i : n
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
p : Polynomial ↑R
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case mp
n : Type u
S : Scheme
⊢ IsIntegralHom (𝔸(n; S) ↘ S) → IsEmpty ↥S ∨ IsEmpty n

pp: case mpr
n : Type u
S : Scheme
⊢ IsEmpty ↥S ∨ IsEmpty n → IsIntegralHom (𝔸(n; S) ↘ S)

Tactic:
· intro h
    cases isEmpty_or_nonempty S
    · exact .inl ‹_›
    refine .inr ?_
    wlog hS : ∃ R, S = Spec R
    · obtain ⟨x⟩ := ‹Nonempty S›
      obtain ⟨y, hy⟩ := S.affineCover.covers x
      exact this (S.affineCover.X _) (MorphismProperty.IsStableUnderBaseChange.of_isPullback
        (isPullback_map (S.affineCover.f _)) h) ⟨y⟩ ⟨_, rfl⟩
    obtain ⟨R, rfl⟩ := hS
    have : Nontrivial R := (subsingleton_or_nontrivial R).resolve_left fun H ↦
        not_isEmpty_of_nonempty (Spec R) (inferInstanceAs (IsEmpty (PrimeSpectrum R)))
    constructor
    intro i
    have := RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.isIntegral_respectsIso.{u}
    rw [← MorphismProperty.cancel_left_of_respectsIso @IsIntegralHom (SpecIso n R).inv,
      SpecIso_inv_over, HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom)] at h
    obtain ⟨p : Polynomial R, hp, hp'⟩ :=
      (MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
        (arrowIsoΓSpecOfIsAffine _)).mpr h.2 (X i)
    have : (rename fun _ ↦ i).comp (uniqueAlgEquiv.{_, u} _ PUnit).symm.toAlgHom p = 0 := by
      simp [← hp', ← algebraMap_eq]
    rw [AlgHom.comp_apply, map_eq_zero_iff _ (rename_injective _ (fun _ _ _ ↦ rfl))] at this
    simp only [AlgEquiv.coe_toAlgHom, EmbeddingLike.map_eq_zero_iff] at this
    simp [this] at hp

Goal state after:
case mpr
n : Type u
S : Scheme
⊢ IsEmpty ↥S ∨ IsEmpty n → IsIntegralHom (𝔸(n; S) ↘ S)
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case mpr
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
hx : x ∈ {x | D x = 0}ᶜ ∩ U
⊢ x ∈ D.support

Tactic:
rw [mem_inter_iff, mem_compl_iff, mem_ofPred_eq] at hx

Goal state after:
case mpr
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
hx : ¬D x = 0 ∧ x ∈ U
⊢ x ∈ D.support
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case mp
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
hx : x ∈ D.support
⊢ x ∈ U \ {x | (fun x ↦ D x = 0 x) x}

pp: case mpr
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
hx : x ∈ U \ {x | (fun x ↦ D x = 0 x) x}
⊢ x ∈ D.support

Tactic:
· simp_all [D.supportWithinDomain hx]

Goal state after:
case mpr
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
hx : x ∈ U \ {x | (fun x ↦ D x = 0 x) x}
⊢ x ∈ D.support
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝¹ : IrreducibleSpace ↥X
U : X.Opens
x : ↥U
inst✝ : Nonempty ↥↑U
⊢ CommRingCat.Hom.hom (X.germToFunctionField U) =
    CommRingCat.Hom.hom (X.presheaf.germ U ↑x ⋯ ≫ X.presheaf.stalkSpecializes ⋯)

Tactic:
X.presheaf.germ_stalkSpecializes

Goal state after:
X : Scheme
inst✝¹ : IrreducibleSpace ↥X
U : X.Opens
x : ↥U
inst✝ : Nonempty ↥↑U
⊢ CommRingCat.Hom.hom (X.germToFunctionField U) = CommRingCat.Hom.hom (X.presheaf.germ U (genericPoint ↥X) ⋯)
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case e'_2
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
e_1✝ : (↑((g x).domain ⊓ (g y).domain) ⟶ Y) = (↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain ⟶ Y)
⊢ (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g x).hom =
    ((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

pp: case e'_3
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
e_1✝ : (↑((g x).domain ⊓ (g y).domain) ⟶ Y) = (↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain ⟶ Y)
⊢ (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g y).hom =
    ((g y).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (g x).equiv (g y)

Tactic:
· dsimp; congr 1; simp [g, ← cancel_mono (Opens.ι _)]

Goal state after:
case e'_3
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
e_1✝ : (↑((g x).domain ⊓ (g y).domain) ⟶ Y) = (↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain ⟶ Y)
⊢ (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g y).hom =
    ((g y).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (g x).equiv (g y)
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case e'_3
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
e_1✝ : (↑((g x).domain ⊓ (g y).domain) ⟶ Y) = (↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain ⟶ Y)
⊢ (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g y).hom =
    ((g y).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (g x).equiv (g y)

Tactic:
· dsimp; congr 1; simp [g, ← cancel_mono (Opens.ι _)]

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (g x).equiv (g y)