mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine (Spec R)
x : ↥(Spec S)
hX : IsAffine (Spec S)
φ : R ⟶ S
hf : Q (CommRingCat.Hom.hom φ)
⊢ Q'
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) x).asIdeal x.asIdeal
          (CommRingCat.Hom.hom φ) ⋯)))

Tactic:
apply hQ _ hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ I.ideal V ≤ RingHom.ker (CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V)))

Tactic:
intro x hx
  apply (I.glueDataObj U).IsSheaf.section_ext
  intro p hp
  obtain ⟨f, g, hfg, hf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 (I.glueDataObjι U p).1
      ⟨(I.glueDataObjι U p).2, hp⟩
  refine ⟨(I.glueDataObjι U ⁻¹ᵁ U.1.ι ⁻¹ᵁ X.basicOpen f),
    fun x hx ↦ X.basicOpen_le g (hfg ▸ hx), hf, ?_⟩
  have := Hom.isIso_app (I.glueDataObjMap (X.affineBasicOpen_le f))
    (I.glueDataObjι U ⁻¹ᵁ U.1.ι ⁻¹ᵁ X.basicOpen f) (by rw [opensRange_glueDataObjMap])
  apply ((ConcreteCategory.isIso_iff_bijective _).mp this).1
  simp only [map_zero, ← RingHom.comp_apply,
    ← CommRingCat.hom_comp, Category.assoc]
  simp only [Scheme.Hom.app_eq_appLE, homOfLE_leOfHom, Scheme.Hom.map_appLE,
    Scheme.Hom.appLE_comp_appLE, Category.assoc, glueDataObjMap_glueDataObjι_assoc]
  rw [Scheme.Hom.appLE]
  have H : (X.homOfLE (X.basicOpen_le f) ≫ U.1.ι) ⁻¹ᵁ V.1 = ⊤ := by
    simp only [Scheme.homOfLE_ι, ← top_le_iff]
    exact fun x _ ↦ (hfg.trans_le (X.basicOpen_le g)) x.2
  simp only [Scheme.Hom.comp_app, Scheme.Opens.ι_app, Scheme.homOfLE_app, ← Functor.map_comp_assoc,
    Scheme.Hom.app_eq _ H, Scheme.Opens.toScheme_presheaf_map, ← Functor.map_comp, Category.assoc]
  simp only [CommRingCat.hom_comp, RingHom.comp_apply]
  convert RingHom.map_zero _
  rw [← RingHom.mem_ker, ker_glueDataObjι_appTop, ← Ideal.mem_comap, Ideal.comap_comap,
    ← CommRingCat.hom_comp]
  simp only [homOfLE_leOfHom, Scheme.Hom.comp_base,
    TopologicalSpace.Opens.map_comp_obj, eqToHom_op, eqToHom_unop, ← Functor.map_comp,
    Scheme.Opens.topIso_hom, Category.assoc]
  exact I.ideal_le_comap_ideal (U := X.affineBasicOpen f) (V := V)
    (hfg.trans_le (X.basicOpen_le g)) hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝¹ : Scheme
U : X✝¹.Opens
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
K : Type u
inst✝ : Field K
X : Scheme
f : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ Spec.map (descResidueField (stalkClosedPointTo (Spec.map f.snd ≫ X.fromSpecResidueField f.fst))) =
    Spec.map ((residueFieldCongr ⋯).hom ≫ f.snd)

Tactic:
Spec.map_comp,

Goal state after:
X✝¹ : Scheme
U : X✝¹.Opens
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
K : Type u
inst✝ : Field K
X : Scheme
f : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ Spec.map (descResidueField (stalkClosedPointTo (Spec.map f.snd ≫ X.fromSpecResidueField f.fst))) =
    Spec.map f.snd ≫ Spec.map (residueFieldCongr ⋯).hom
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i))

Tactic:
rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]

Goal state after:
case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ↑i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑V ∩ ↑(X.basicOpen ↑i))

Tactic:
rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]

Goal state after:
case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ↑i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine ↑U
⊢ IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.app f U)

Tactic:
Scheme.Hom.app_eq_appLE

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine ↑U
⊢ IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FiniteType R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
⊢ Algebra.FiniteType R (Localization.Away r)

Tactic:
convert! H ⟨r, hr⟩

Goal state after:
case e'_5
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FiniteType R (Localization.Away ↑r)
algInst✝ : Algebra R S := ⋯
r : S
hr : r ∈ s
e_4✝ : OreLocalization.instSemiring = CommRing.toCommSemiring.toSemiring
⊢ OreLocalization.instAlgebra = ((algebraMap S (Localization.Away ↑⟨r, hr⟩)).comp f).toAlgebra
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_1.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))
⊢ ⨆ i, PrimeSpectrum.basicOpen (f i) = ⊤

pp: case refine_1.refine_2
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))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))

Tactic:
· exact top_le_iff.mp fun x _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨x, hqf _⟩

Goal state after:
case refine_1.refine_2
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))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
⊢ IsSeparated f

Tactic:
IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsSeparated) _
      (iSup_affineOpens_eq_top Y)

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
⊢ ∀ (i : ↑Y.affineOpens), IsSeparated (f ∣_ ↑i)
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FinitePresentation R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
⊢ Algebra.FinitePresentation R (Localization.Away r)

Tactic:
convert! H ⟨r, hr⟩

Goal state after:
case e'_5
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FinitePresentation R (Localization.Away ↑r)
algInst✝ : Algebra R S := ⋯
r : S
hr : r ∈ s
e_4✝ : OreLocalization.instSemiring = CommRing.toCommSemiring.toSemiring
⊢ OreLocalization.instAlgebra = ((algebraMap S (Localization.Away ↑⟨r, hr⟩)).comp f).toAlgebra
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ x ∈ comap (algebraMap R A) '' (zeroLocus ∅ \ zeroLocus {f})

Tactic:
zeroLocus_empty,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ x ∈ comap (algebraMap R A) '' (Set.univ \ zeroLocus {f})
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
⊢ geometrically P f ↔ ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)

Tactic:
refine ⟨fun hf y ↦ (geometrically P).pullback_snd _ _ hf, fun H ↦ ?_⟩

Goal state after:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
⊢ geometrically P f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), topologically (@IsOpenMap) (f ∣_ U i)
⊢ topologically (@IsOpenMap) f

Tactic:
simp_rw [topologically, morphismRestrict_base] at H

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage ⇑f)
⊢ topologically (@IsOpenMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource @UniversallyOpen

Tactic:
by
  rw [eq]
  exact universally_isZariskiLocalAtSource _

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), topologically (@IsClosedMap) (f ∣_ U i)
⊢ topologically (@IsClosedMap) f

Tactic:
simp_rw [topologically, morphismRestrict_base] at H

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage ⇑f)
⊢ topologically (@IsClosedMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1),
      IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i) ∧
        LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
forall_and

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1),
      IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i) ∧ Mono (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.toPreZeroHypercover.1), monomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
forall_and

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
coe_eval₂Hom,

Goal state after:
n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.app (Spec.map (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv)
          ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (isoOfIsAffine n (Spec R)).inv ⊤)) (coord (Spec R) i)) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Tactic:
rw [isoOfIsAffine_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality,
      CommRingCat.comp_apply]

Goal state after:
n : Type u
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv)
      ((ConcreteCategory.hom (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv)
        (X i)) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case inr
n : Type u
S : Scheme
h : IsReduced S
this : ∀ {n : Type u} (S : Scheme) [h : IsReduced S], (∃ R, S = Spec R) → IsReduced 𝔸(n; S)
hS : ¬∃ R, S = Spec R
⊢ IsReduced 𝔸(n; S)

Tactic:
rw [IsReduced.iff_of_openCover _ (S.affineCover.pullback₁ (𝔸(n; S) ↘ S))]

Goal state after:
case inr
n : Type u
S : Scheme
h : IsReduced S
this : ∀ {n : Type u} (S : Scheme) [h : IsReduced S], (∃ R, S = Spec R) → IsReduced 𝔸(n; S)
hS : ¬∃ R, S = Spec R
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).I₀),
    IsReduced ((Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).X i)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
⊢ Statement R₀ (Localization.Away c) n
      {
        val :=
          Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Localization.Away c))) ∘ e.val } →
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } →
      Statement R₀ R n e

Tactic:
have degBound_e₁_le : e₁.degBound ≤ e.degBound := by
    unfold degBound
    gcongr with j
    exact (degree_mul_le _ _).trans <| (add_le_of_nonpos_left degree_C_le).trans degree_map_le

Goal state after:
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
⊢ Statement R₀ (Localization.Away c) n
      {
        val :=
          Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Localization.Away c))) ∘ e.val } →
    Statement R₀ (R ⧸ Ideal.span {c}) n { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } →
      Statement R₀ R n e
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
Y : Type u_2
inst✝² : DecidableEq X
inst✝¹ : Zero Y
inst✝ : Preorder Y
x : X
y : Y
⊢ 0 < single x y ↔ 0 < y

Tactic:
lt_def,

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
Y : Type u_2
inst✝² : DecidableEq X
inst✝¹ : Zero Y
inst✝ : Preorder Y
x : X
y : Y
⊢ ⇑0 < ⇑(single x y) ↔ 0 < y
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ Spec.map φ ≫ Y.fromSpecStalk y = Spec.map (Y.presheaf.germ V y hyV ≫ φ) ≫ IsAffineOpen.fromSpec hV

Tactic:
Spec.map_comp,

Goal state after:
case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ Spec.map φ ≫ Y.fromSpecStalk y = (Spec.map φ ≫ Spec.map (Y.presheaf.germ V y hyV)) ≫ IsAffineOpen.fromSpec hV
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case e'_2.e_a
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
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 = X.homOfLE ⋯

Tactic:
simp [g, ← cancel_mono (Opens.ι _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case e'_3.e_a
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
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 = X.homOfLE ⋯

Tactic:
simp [g, ← cancel_mono (Opens.ι _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
⊢ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ Scheme.Hom.opensRange (D.map j.hom ⁻¹ᵁ U).ι

Tactic:
simp only [opensDiagram_obj, Scheme.Opens.opensRange_ι]

Goal state after:
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
⊢ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V ≤ D.map j.hom ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X ⤏ Y
⊢ (id X).comp f = f

Tactic:
← f.toRationalMap_representative,

Goal state after:
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X ⤏ Y
⊢ (id X).comp f.representative.toRationalMap = f.representative.toRationalMap
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case e'_2
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ zeroLocus (Set.range { val := 0 }.val) \ zeroLocus {f} = ↑(basicOpen f)

Tactic:
simp only [basicOpen_eq_zeroLocus_compl, Set.compl_eq_univ_sdiff]
        congr 1
        rw [← Set.univ_subset_iff]
        rintro x _ _ ⟨_, rfl⟩
        exact zero_mem x.asIdeal

Goal state after: