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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
H : I.support = ⊥
U : ↑X.affineOpens
⊢ ⊤.ideal U ≤ I.ideal U

Tactic:
have := (U.2.fromSpec_image_zeroLocus _).trans_subset
    ((zeroLocus_inter_subset_supportSet I U).trans H.le)

Goal state after:
X : Scheme
I : X.IdealSheafData
H : I.support = ⊥
U : ↑X.affineOpens
this : ⇑(IsAffineOpen.fromSpec ⋯) '' PrimeSpectrum.zeroLocus ↑(I.ideal U) ⊆ ↑⊥
⊢ ⊤.ideal U ≤ I.ideal U
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)
⊢ (fun f ↦ ⟨f (closedPoint ↑(CommRingCat.of K)), descResidueField (stalkClosedPointTo f)⟩)
      ((fun xf ↦ Spec.map xf.snd ≫ X.fromSpecResidueField xf.fst) f) =
    f

Tactic:
SpecToEquivOfField_eq_iff

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)
⊢ ∃ (e :
    ((fun f ↦ ⟨f (closedPoint ↑(CommRingCat.of K)), descResidueField (stalkClosedPointTo f)⟩)
          ((fun xf ↦ Spec.map xf.snd ≫ X.fromSpecResidueField xf.fst) f)).fst =
      f.fst),
    ((fun f ↦ ⟨f (closedPoint ↑(CommRingCat.of K)), descResidueField (stalkClosedPointTo f)⟩)
          ((fun xf ↦ Spec.map xf.snd ≫ X.fromSpecResidueField xf.fst) f)).snd =
      (residueFieldCongr e).hom ≫ f.snd
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀.h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((((pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
              pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
                pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
            pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
          pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
        I.glueDataObjι i) ≫
      (↑i).ι =
    (((𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
            pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
          pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
        I.glueDataObjι i) ≫
      (↑i).ι

Tactic:
simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          glueDataT'Aux_fst, limit.lift_π_assoc, cospan_left, glueDataT_fst, Scheme.homOfLE_ι,
          glueDataT'Aux_snd_ι, glueDataT'Aux_fst_assoc, glueDataT_fst_assoc, Category.id_comp]

Goal state after:
case h₀.h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ (↑i ⊓ ↑j).ι =
    pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i).ι
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₁.h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((((pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
              pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
                pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
            pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
          pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
        I.glueDataObjι i) ≫
      (↑i).ι =
    (((𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
            pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
          pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
        I.glueDataObjι i) ≫
      (↑i).ι

Tactic:
simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          glueDataT'Aux_fst, limit.lift_π_assoc, cospan_left, glueDataT_fst, Scheme.homOfLE_ι,
          glueDataT'Aux_snd_ι, glueDataT'Aux_fst_assoc, glueDataT_fst_assoc, Category.id_comp]

Goal state after:
case h₁.h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ (↑i ⊓ ↑j).ι =
    pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i).ι
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mp.left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
t : ↥(pullback f g)
⊢ (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t ∈ ⇑(pullback.fst f' g') ⁻¹' Set.range ⇑i₁

Tactic:
use pullback.fst f g t
      rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]
      simp

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

Goal state before:
pp: case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
⊢ P (f ≫ g)

Tactic:
IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)

Goal state after:
case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
⊢ ∀ (i : ↑Z.affineOpens), P ((f ≫ g) ∣_ ↑i)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X : Scheme
X✝ Y✝ Z✝ : X.IdealSheafData
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op.unop =
    ((MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op ≫
        (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op).unop

Tactic:
ext1; simp

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

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
⊢ (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f

Tactic:
simp [← pullback.condition]

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

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ (vanishingIdeal Z).map f ≤ vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))

Tactic:
rw [map, ← le_support_iff_le_vanishingIdeal, TopologicalSpace.Closeds.closure_le]

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
Z : TopologicalSpace.Closeds ↥X
⊢ ⇑f '' ↑Z ⊆ ↑(Hom.ker ((vanishingIdeal Z).subschemeι ≫ f)).support
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
⊢ IsIso f

Tactic:
let f' : MorphismProperty.Over.mk ⊤ i₁ ‹_› ⟶ .mk ⊤ i₂ ‹_› := MorphismProperty.Over.homMk f h
  suffices h : IsIso f'.op by
    rwa [isIso_op_iff, ← isIso_iff_of_reflects_iso _ (MorphismProperty.Over.forget ..),
      ← isIso_iff_of_reflects_iso _ (Over.forget _)] at h
  rw [← isIso_iff_of_reflects_iso _ (IsClosedImmersion.overEquivIdealSheafData X).functor]
  simpa [IsClosedImmersion.overEquivIdealSheafData] using ⟨homOfLE h'.le, by simp, by simp⟩

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

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ ((I.comapIso f).hom ≫ pullback.snd f I.subschemeι) ≫ I.subschemeι = (I.comap f).subschemeMap I f ⋯ ≫ I.subschemeι

Tactic:
simp [← pullback.condition]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ (∑ x ∈ s.attach, ↑x * l x - 1) * f q = 0

Tactic:
Finsupp.linearCombination_apply_of_mem_supported (α := (s : Set S)) S (s := s.attach)

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : ∑ i ∈ s.attach, l i • ↑i = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ (∑ x ∈ s.attach, ↑x * l x - 1) * f q = 0

R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ l ∈ Finsupp.supported S S ↑s.attach
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
n : ℕ
hn : N ≤ n
⊢ ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) (I N)) =
    ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) (I n))

Tactic:
iInf_subtype',

Goal state after:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
n : ℕ
hn : N ≤ n
⊢ ⨅ x, Ideal.under R (Ideal.map (algebraMap R (Localization.Away ↑x)) (I N)) =
    ⨅ f ∈ S, Ideal.under R (Ideal.map (algebraMap R (Localization.Away f)) (I n))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case f
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ A ≃ₐ[A] A ⧸ ⊥

Tactic:
exact { __ := (RingEquiv.quotientBot A).symm, __ := Algebra.ofId _ _ }

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case inr
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
this : ∀ {X : Scheme} [DiscreteTopology ↥X] [IsReduced X], Subsingleton ↥X → IsLocallyArtinian X
hX : ¬Subsingleton ↥X
⊢ IsLocallyArtinian X

pp: X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
hX : Subsingleton ↥X
⊢ IsLocallyArtinian X

Tactic:
· let 𝒰 : X.OpenCover := X.openCoverOfIsOpenCover
      (fun x : X ↦ ⟨{x}, isOpen_discrete _⟩) (.mk (by ext; simp))
    have inst (i : _) : DiscreteTopology (𝒰.X i) := (𝒰.f i).isOpenEmbedding.discreteTopology
    have inst (i : _) : IsReduced (𝒰.X i) := isReduced_of_isOpenImmersion (𝒰.f i)
    exact (isLocallyArtinian_iff_openCover 𝒰).mpr
      fun i ↦ this (inferInstanceAs (Subsingleton ({i} : Set X)))

Goal state after:
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
hX : Subsingleton ↥X
⊢ IsLocallyArtinian X
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: ⊢ @GeometricallyReduced = geometrically IsReduced

Tactic:
by
  ext; exact geometricallyReduced_iff _

Goal state after:
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
hp' : ∃ m, ↑m * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) p = 0
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
obtain ⟨⟨x, m, (rfl : algebraMap R S t ^ m = x)⟩, e⟩ := hp'

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) p = 0
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: ⊢ HasAffineProperty (@IsFinite) (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Finite)

Tactic:
HasAffineProperty.affineAnd_iff _ RingHom.finite_respectsIso
    RingHom.finite_localizationPreserves.away RingHom.finite_ofLocalizationSpan

Goal state after:
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    IsFinite f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).Finite
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this✝¹ : IsAffine ↑US
this✝ : IsAffine ↑UT
this : IsAffine ↑UX
⊢ IsPullback (Scheme.Spec.map (op (Scheme.Hom.app iY UT ≫ Y.presheaf.map (homOfLE ⋯).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app g UX ≫ Y.presheaf.map (homOfLE ⋯).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app f US ≫ T.presheaf.map (homOfLE hUST).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app iX US ≫ X.presheaf.map (homOfLE hUSX).op)))

Tactic:
have hUY' : IsAffineOpen UY :=
    .of_isIso (Scheme.Hom.isPullback_resLE H hUST hUSX hUY).isoPullback.hom

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this✝¹ : IsAffine ↑US
this✝ : IsAffine ↑UT
this : IsAffine ↑UX
hUY' : IsAffineOpen UY
⊢ IsPullback (Scheme.Spec.map (op (Scheme.Hom.app iY UT ≫ Y.presheaf.map (homOfLE ⋯).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app g UX ≫ Y.presheaf.map (homOfLE ⋯).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app f US ≫ T.presheaf.map (homOfLE hUST).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app iX US ≫ X.presheaf.map (homOfLE hUSX).op)))
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hX
n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
i✝ : n
⊢ ((CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom) (X i✝) =
    ((CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom) (X i✝)

Tactic:
simpa using! h _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (Scheme.Hom.appTop S.isoSpec.inv ≫ Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom C))) ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom =
    (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom

Tactic:
simp only [Category.assoc, Scheme.ΓSpecIso_naturality, CommRingCat.of_carrier,
            ← Scheme.toSpecΓ_appTop]

Goal state after:
case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ Scheme.Hom.appTop S.isoSpec.inv ≫ Scheme.Hom.appTop S.toSpecΓ ≫ CommRingCat.ofHom C =
    CommRingCat.ofHom C ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv ≫
        (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom
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
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

pp: n✝ : Type u
S✝ : Scheme
n : Type u
S : Scheme
hS : ∃ R, S = Spec R
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

Tactic:
· refine (IsZariskiLocalAtTarget.iff_of_openCover
      (P := topologically @IsOpenMap) S.affineCover).mpr ?_
    intro i
    have := this (n := n) (S.affineCover.X i) ⟨_, rfl⟩
    rwa [← (isPullback_map (n := n) (S.affineCover.f i)).isoPullback_hom_snd,
      MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)] at this

Goal state after:
n✝ : Type u
S✝ : Scheme
n : Type u
S : Scheme
hS : ∃ R, S = Spec R
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: 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 ≫ φ'
⊢ ∃ U, ∃ (hxU : x ∈ U), ∃ f, Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
refine ⟨W, hxW, W.toSpecΓ ≫ Spec.map φ' ≫ hV.fromSpec, ?_, ?_⟩

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 = W.fromSpecStalkOfMem x hxW ≫ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV

case refine_2
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 ≫ φ'
⊢ (W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV) ≫ sY = W.ι ≫ sX
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
← isIso_comp_left_iff (pushoutSymmetry _ _).hom

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso
    ((pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)).hom ≫
      pushoutSection H hUST hUSX hUY)