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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (F ≫ X.homOfLE ⋯) ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V

Tactic:
rw [← Scheme.Hom.comp_preimage, Category.assoc, X.homOfLE_ι]

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (F ≫ (↑U ⊓ ↑V).ι) ⁻¹ᵁ ↑V
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case refine_2
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
⊢ ↑⟨x, ⟨f, hf⟩⟩.snd =
    (X.presheaf.stalkCongr ⋯).hom ≫
      ↑((fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
            ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩)).snd

Tactic:
· refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_
      simp only [Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk,
        TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes_assoc]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueDataObjι V =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
refine (pullback.lift_fst_assoc _ _ _ _).trans ?_
  conv_lhs => enter [2]; rw [glueDataObjι]
  rw [Scheme.Hom.liftQuotient_comp_assoc, Category.assoc, Category.assoc, Iso.hom_inv_id,
    Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
    (ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial ≫ (Spec R).residue x

Tactic:
by
  rw [← Spec.algebraMap_stalkIso_inv_assoc]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: case mpr
K : Type u_1
inst✝ : Field K
X : Scheme
f : ↥X
snd✝¹ snd✝ : X.residueField f ⟶ CommRingCat.of K
h : ⟨f, snd✝¹⟩.snd = (residueFieldCongr ⋯).hom ≫ ⟨f, snd✝⟩.snd
⊢ ⟨f, snd✝¹⟩ = ⟨f, snd✝⟩

Tactic:
simpa

Goal state after:
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)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ PrimeSpectrum.basicOpen ↑i ∈ (Spec Γ(X, ⊤)).affineOpens

Tactic:
change IsAffineOpen _

Goal state after:
case refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ IsAffineOpen (PrimeSpectrum.basicOpen ↑i)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ ↑U ≤ ↑U ⊓ ↑V

Tactic:
simpa

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this : IsIso (X.homOfLE ⋯)
⊢ ↑U ≤ ↑U ⊓ ↑V

Tactic:
simpa

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueData.ι V = 𝟙 (I.glueData.U U) ≫ I.glueData.ι U

Tactic:
← this

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueData.ι V =
    𝟙 (I.glueData.U U) ≫
      inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
        I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case to_basicOpen
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H this : IsAffine X
⊢ IsAffine ↑(f ⁻¹ᵁ Y.basicOpen r)

Tactic:
change IsAffineOpen _

Goal state after:
case to_basicOpen
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H this : IsAffine X
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case of_basicOpenCover
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ → (∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → IsAffine X

Tactic:
intro X Y _ f S hS hS'
      apply_fun Ideal.map (f.appTop).hom at hS
      rw [Ideal.map_span, Ideal.map_top] at hS
      apply isAffine_of_isAffineOpen_basicOpen _ hS
      have : ∀ i : S, IsAffineOpen (f ⁻¹ᵁ Y.basicOpen i.1) := hS'
      simpa [Scheme.preimage_basicOpen] using! this

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : ↑X.affineOpens
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv

Tactic:
← CommRingCat.ofHom_comp,

Goal state after:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : ↑X.affineOpens
⊢ Spec.map (CommRingCat.ofHom ((Ideal.Quotient.factor ⋯).comp (Ideal.Quotient.mk (I.ideal U)))) ≫
      (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv
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.appLE (pullback.snd f (↑U).ι ≫ (↑U).ι) ((↑U).ι ''ᵁ ⊤) ⊤ ⋯ = Hom.appLE (pullback.snd f (↑U).ι ≫ 𝟙 ↑↑U) ⊤ ⊤ ⋯

Tactic:
Hom.comp_appLE,

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).ι) ⊤
⊢ Hom.app (↑U).ι ((↑U).ι ''ᵁ ⊤) ≫ Hom.appLE (pullback.snd f (↑U).ι) ((↑U).ι ⁻¹ᵁ (↑U).ι ''ᵁ ⊤) ⊤ ⋯ =
    Hom.appLE (pullback.snd f (↑U).ι ≫ 𝟙 ↑↑U) ⊤ ⊤ ⋯
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ QuasiCompact (Hom.toImage f ≫ Hom.imageι f)

Tactic:
simpa

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

Goal state before:
pp: Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hP' : HasAffineProperty P' (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q')
hQQ' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f
⊢ P ≤ P'

Tactic:
by
  rw [HasAffineProperty.eq_targetAffineLocally (P := P),
    HasAffineProperty.eq_targetAffineLocally (P := P')]
  exact targetAffineLocally_affineAnd_le hQQ'

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

Goal state before:
pp: X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ Hom.ker (pullback.fst f i) =
    Hom.ker (pullback.map f i f (Hom.imageι i) (𝟙 X) (Hom.toImage i) (𝟙 Y) ⋯ ⋯ ≫ pullback.fst f (Hom.ker i).subschemeι)

Tactic:
pullback.lift_fst,

Goal state after:
X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ Hom.ker (pullback.fst f i) = Hom.ker (pullback.fst f i ≫ 𝟙 X)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

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

Tactic:
← this

Goal state after:
case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ Hom.ker J.subschemeι ≤ Hom.ker ((inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
⊢ x ∈ U.carrier ∧ f x = f x

Tactic:
simpa

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
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : ↥t), FinitePresentation R (Localization.Away (f ↑g))
⊢ FinitePresentation R S

Tactic:
apply Algebra.FinitePresentation.of_surjective hf

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : ↥t), FinitePresentation R (Localization.Away (f ↑g))
⊢ (RingHom.ker f.toRingHom).FG
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsImmersion (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f)

Tactic:
simpa

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

Goal state before:
pp: X Y Z : Scheme
⊢ MorphismProperty.IsStableUnderBaseChange @IsClosedImmersion

Tactic:
by
  apply HasAffineProperty.isStableUnderBaseChange
  have := HasAffineProperty.isLocal_affineProperty @IsClosedImmersion
  apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
  intro X Y S _ _ f g ⟨ha, hsurj⟩
  exact ⟨inferInstance, RingHom.surjective_isStableUnderBaseChange.pullback_fst_appTop _
    RingHom.surjective_respectsIso f _ hsurj⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ comap (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) { asIdeal := q, isPrime := hq } ∉ zeroLocus {f}

Tactic:
simpa

Goal state after:
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 : ι), IsLocallyArtinian (Spec Γ(X, U i))

Tactic:
simpa

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

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
z : ↥(pullback f q)
hz : z ∈ Z
hzt : fT z = t
this : ∃ i, fT z ∈ Ti i ∧ p z ∈ U i
⊢ z ∈ ↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i)

Tactic:
simpa

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

Goal state before:
pp: case mpr
X : Scheme
inst✝ : JacobsonSpace ↥X
x : ↥X
⊢ LocallyOfFiniteType (X.fromSpecResidueField x) → IsClosed {x}

Tactic:
intro H
    simpa using (X.fromSpecResidueField x).closePoints_subset_preimage_closedPoints
      (IsLocalRing.isClosed_singleton_closedPoint _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ 𝔸(n; S).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom C ≫
            CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S))) ≫
        S.isoSpec.inv =
    𝔸(n; S) ↘ S

Tactic:
← CommRingCat.ofHom_comp,

Goal state after:
case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ 𝔸(n; S).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom ((eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)).comp C)) ≫
        S.isoSpec.inv =
    𝔸(n; S) ↘ S
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤)).comp
      C =
    (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv).comp C

pp: case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ∀ (i : n),
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤))
        (X i) =
      (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)

Tactic:
· change _ = (CommRingCat.ofHom C ≫ _).hom
          rw [CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_ofHom, eval₂Hom_comp_C,
            ← CommRingCat.hom_comp, ← CommRingCat.hom_ext_iff,
            ← cancel_mono (Scheme.ΓSpecIso _).hom]
          rw [← Scheme.Hom.comp_appTop, homOfVector_over, Scheme.Hom.comp_appTop]
          simp only [Category.assoc, Scheme.ΓSpecIso_naturality, CommRingCat.of_carrier,
            ← Scheme.toSpecΓ_appTop]
          rw [← Scheme.Hom.comp_appTop_assoc, Scheme.isoSpec, asIso_inv, IsIso.hom_inv_id]
          simp

Goal state after:
case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ∀ (i : n),
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤))
        (X i) =
      (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
this : D.support = U \ {x | D x = 0 x}
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ {x | (fun x ↦ D x = 0 x) x})).Finite

Tactic:
← this

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
this : D.support = U \ {x | D x = 0 x}
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ D.support).Finite
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
x : ↥X
inst✝¹ : X.IsGermInjectiveAt x
inst✝ : IsOpenImmersion f
U : X.Opens
hxU : x ∈ U
hU : IsAffineOpen U
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
⊢ MorphismProperty.injective CommRingCat
    ((Scheme.Hom.appIso f U).inv ≫ Y.presheaf.germ (f ''ᵁ U) (f x) ⋯ ≫ Scheme.Hom.stalkMap f x)

Tactic:
simpa

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt (f x)
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↥X
hy : y ∈ ↑↑V
e : f y = f x
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) (f x) ⋯))
⊢ X.IsGermInjectiveAt x

Tactic:
obtain rfl := f.isOpenEmbedding.injective e

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↥X
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt (f y)
e : f y = f y
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) (f y) ⋯))
⊢ X.IsGermInjectiveAt y
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
⊢ ↑s ⊆ ↑(↑R ∙ ↑(∏ x ∈ s.attach, f ↑x ⋯)).annihilator

Tactic:
intro i hi

Goal state after:
X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
i : ↑R
hi : i ∈ ↑s
⊢ i ∈ ↑(↑R ∙ ↑(∏ x ∈ s.attach, f ↑x ⋯)).annihilator
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
⊢ ∃ V, ∃ (hxV : x ∈ V), V ≤ U ∧ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range

Tactic:
let := φRA.hom.toAlgebra
  obtain ⟨s, hs⟩ := hφRA
  choose W hxW f hf using fun t ↦ X.presheaf.exists_germ_eq (φ t)
  have H : x ∈ s.inf W ⊓ U := by
    rw [← SetLike.mem_coe, TopologicalSpace.Opens.coe_inf, TopologicalSpace.Opens.coe_finset_inf]
    exact ⟨by simpa using fun x _ ↦ hxW x, hxU⟩
  refine ⟨s.inf W ⊓ U, H, inf_le_right, ?_⟩
  let := φRX.hom.toAlgebra
  let := (φRX ≫ X.presheaf.germ U x hxU).hom.toAlgebra
  let := (φRX ≫ X.presheaf.map (homOfLE (inf_le_right (a := s.inf W))).op).hom.toAlgebra
  let φ' : A →ₐ[R] X.presheaf.stalk x :=
    { φ.hom with commutes' := DFunLike.congr_fun (congr_arg CommRingCat.Hom.hom e) }
  let ψ : Γ(X, s.inf W ⊓ U) →ₐ[R] X.presheaf.stalk x :=
    { (X.presheaf.germ _ x H).hom with commutes' := fun x ↦ X.presheaf.germ_res_apply _ _ _ _ }
  change AlgHom.range φ' ≤ AlgHom.range ψ
  rw [← Algebra.map_top, ← hs, AlgHom.map_adjoin, Algebra.adjoin_le_iff]
  rintro _ ⟨i, hi, rfl : φ i = _⟩
  refine ⟨X.presheaf.map (homOfLE (inf_le_left.trans (Finset.inf_le hi))).op (f i), ?_⟩
  exact (X.presheaf.germ_res_apply _ _ _ _).trans (hf _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
U : Opens ↥X
hU : genericPoint ↥X ∈ U
g : ToType (X.presheaf.obj (op U))
hg : (ConcreteCategory.hom (X.presheaf.germ U (genericPoint ↥X) hU)) g = f
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'

Tactic:
obtain ⟨_, ⟨A, hA, rfl⟩, hxA, hAU⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open hU U.isOpen

Goal state after:
X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
U : Opens ↥X
hU : genericPoint ↥X ∈ U
g : ToType (X.presheaf.obj (op U))
hg : (ConcreteCategory.hom (X.presheaf.germ U (genericPoint ↥X) hU)) g = f
A : Opens ↥X
hA : A ∈ X.affineOpens
hxA : genericPoint ↥X ∈ ↑A
hAU : ↑A ⊆ ↑U
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
U : Opens ↥X
hU : genericPoint ↥X ∈ U
g : ToType (X.presheaf.obj (op U))
hg : (ConcreteCategory.hom (X.presheaf.germ U (genericPoint ↥X) hU)) g = f
A : Opens ↥X
hA : A ∈ X.affineOpens
hxA : genericPoint ↥X ∈ ↑A
hAU : ↑A ⊆ ↑U
this : Nonempty ↥↑A
gA : ↑Γ(X, A) := (ConcreteCategory.hom (X.presheaf.map (homOfLE hAU).op)) g
h_germ_gA : (ConcreteCategory.hom (X.presheaf.germ A (genericPoint ↥X) hxA)) gA = f
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'

Tactic:
have hxV : genericPoint X ∈ X.basicOpen gA := by
    rwa [Scheme.mem_basicOpen X gA (genericPoint X) hxA, h_germ_gA, isUnit_iff_ne_zero]

Goal state after:
X : Scheme
inst✝ : IsIntegral X
f : ↑X.functionField
hf : f ≠ 0
U : Opens ↥X
hU : genericPoint ↥X ∈ U
g : ToType (X.presheaf.obj (op U))
hg : (ConcreteCategory.hom (X.presheaf.germ U (genericPoint ↥X) hU)) g = f
A : Opens ↥X
hA : A ∈ X.affineOpens
hxA : genericPoint ↥X ∈ ↑A
hAU : ↑A ⊆ ↑U
this : Nonempty ↥↑A
gA : ↑Γ(X, A) := (ConcreteCategory.hom (X.presheaf.map (homOfLE hAU).op)) g
h_germ_gA : (ConcreteCategory.hom (X.presheaf.germ A (genericPoint ↥X) hxA)) gA = f
hxV : genericPoint ↥X ∈ X.basicOpen gA
⊢ ∃ U ∈ X.affineOpens, ∃ f', ∃ (x : Nonempty ↥↑U), (ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f : X ⤏ Y
inst✝¹ : f.IsDominant
g : Y ⤏ Z
inst✝ : g.IsDominant
⊢ (f.comp g).IsDominant

Tactic:
rw [← g.toRationalMap_representative, RationalMap.comp_def]
  infer_instance

Goal state after: