mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
ψ : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField :=
  Algebra.TensorProduct.map (Algebra.TensorProduct.map (AlgHom.id A A) B'.val) (AlgHom.id A x.asIdeal.ResidueField)
hψeq :
  ψ =
    (↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
      ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
        ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
          ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
            ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))))
⊢ Injective
    ⇑((↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
        ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
          ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
            ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
              ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField)))))

Tactic:
dsimp

Goal state after:
K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
ψ : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField :=
  Algebra.TensorProduct.map (Algebra.TensorProduct.map (AlgHom.id A A) B'.val) (AlgHom.id A x.asIdeal.ResidueField)
hψeq :
  ψ =
    (↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
      ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
        ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
          ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
            ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))))
⊢ Injective
    (⇑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B)) ∘
      ⇑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm ∘
        ⇑(Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val) ∘
          ⇑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B') ∘
            ⇑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Finite R (R[X] ⧸ Ideal.span {g})

pp: case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Free R (R[X] ⧸ Ideal.span {g})

Tactic:
· exact .of_basis (AdjoinRoot.powerBasis' hg).basis

Goal state after:
case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Free R (R[X] ⧸ Ideal.span {g})
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Free R (R[X] ⧸ Ideal.span {g})

Tactic:
· exact .of_basis (AdjoinRoot.powerBasis' hg).basis

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
⊢ DiscreteTopology ↥X

Tactic:
apply discreteTopology_iff_isOpen_singleton.mpr

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
⊢ ∀ (a : ↥X), IsOpen {a}
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK.a
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U ∩ Set.range ⇑f ⊆ ↑U

Tactic:
· exact Set.inter_subset_left

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK.a
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ ↑↑U

Tactic:
· exact Set.inter_subset_left

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f ((Scheme.SpecToEquivOfField K Y).symm ⟨y, φ⟩)
p : Z ⟶ Scheme.Hom.fiber f y := ⋯
⊢ IsPullback p snd (Scheme.Hom.fiberToSpecResidueField f y) (Spec.map φ)

Tactic:
simp only [Scheme.SpecToEquivOfField, Equiv.coe_fn_symm_mk] at h

Goal state after:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
p : Z ⟶ Scheme.Hom.fiber f y := ⋯
⊢ IsPullback p snd (Scheme.Hom.fiberToSpecResidueField f y) (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : GeometricallyIrreducible f
inst✝ : IrreducibleSpace ↥S
hf : IsOpenMap ⇑f
⊢ IrreducibleSpace ↥X

Tactic:
simpa [irreducibleSpace_def] using
    f.isIrreducible_preimage hf (IrreducibleSpace.isIrreducible_univ _)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ UniversallyClosed f

Tactic:
by
  rw [universallyClosed_eq]
  intro X' Y' i₁ i₂ f' hf
  have hf' : IsClosedImmersion f' :=
    MorphismProperty.of_isPullback hf.flip inferInstance
  exact f'.isClosedEmbedding.isClosedMap

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))ᶜ
⊢ IsOpen (⋃ i, ⇑fT ⁻¹' ↑(Ti i) ∩ ⇑p ⁻¹' ↑(U i))

Tactic:
exact isOpen_iUnion fun i ↦ (fT.continuous.1 _ (Ti i).2).inter (p.continuous.1 _ (U i).2)

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

Goal state before:
pp: ⊢ @IsIntegralHom = @UniversallyClosed ⊓ @IsAffineHom

Tactic:
ext
  exact iff_universallyClosed_and_isAffineHom

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
inst✝ : JacobsonSpace ↥Y
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
wlog hY : ∃ S, Y = Spec S generalizing X Y
  · rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]
    have inst (i) := ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding.injective.subsingleton
    have inst (i) := isReduced_of_isOpenImmersion ((Y.affineCover.pullback₁ f).f i)
    have inst (i) := JacobsonSpace.of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding
    exact forall_congr' fun i ↦ this ⟨_, rfl⟩
  obtain ⟨S, rfl⟩ := hY
  wlog hX : ∃ R, X = Spec R generalizing X
  · rw [← MorphismProperty.cancel_left_of_respectsIso (P := @IsFinite) X.isoSpec.inv,
      ← MorphismProperty.cancel_left_of_respectsIso (P := @LocallyOfFiniteType) X.isoSpec.inv]
    have inst := X.isoSpec.inv.isOpenEmbedding.injective.subsingleton
    refine this ⟨_, rfl⟩
  cases isEmpty_or_nonempty X
  · exact ⟨inferInstance, inferInstance⟩
  have : IrreducibleSpace X := ⟨‹_›⟩
  obtain ⟨R, rfl⟩ := hX
  have : IsDomain R := (affine_isIntegral_iff R).mp (isIntegral_of_irreducibleSpace_of_isReduced _)
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  rw [IsFinite.SpecMap_iff, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]
  have := (PrimeSpectrum.t1Space_iff_isField (R := R)).mp (show T1Space (Spec R) by infer_instance)
  let := this.toField
  let := φ.hom.toAlgebra
  have := PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mpr ‹_›
  change Module.Finite _ _ ↔ Algebra.FiniteType _ _
  exact ⟨fun _ ↦ inferInstance, fun _ ↦ finite_of_finite_type_of_isJacobsonRing _ _⟩

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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp

Goal state after:
n : Type u
S X : Scheme
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Scheme
⊢ { app := reindex ⇑(ConcreteCategory.hom (f ≫ g).unop), naturality := ⋯ }.app x✝ =
    ({ app := reindex ⇑(ConcreteCategory.hom f.unop), naturality := ⋯ } ≫
          { app := reindex ⇑(ConcreteCategory.hom g.unop), naturality := ⋯ }).app
      x✝

Tactic:
dsimp

Goal state after:
n : Type u
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Scheme
⊢ reindex (⇑(ConcreteCategory.hom (g.unop ≫ f.unop))) x✝ =
    reindex (⇑(ConcreteCategory.hom f.unop)) x✝ ≫ reindex (⇑(ConcreteCategory.hom g.unop)) x✝
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ IsAffine (Spec ℤ[n]) ∧ IsIso (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom C)))

Tactic:
← isomorphisms,

Goal state after:
case a
n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ IsAffine (Spec ℤ[n]) ∧ isomorphisms CommRingCat (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom C)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case intro.h₁
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
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV✝ : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
hψ : Function.Injective ⇑ψ
hψ' : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ)
hV : ∀ (i : ι), Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST ⋯ ⋯))
val✝ : Fintype ι
φ : ↑Γ(T, UT) ⊗[↑Γ(S, US)] ((i : ι) → ↑Γ(X, VX i)) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  (RingHom.pi fun i ↦
        (CommRingCat.Hom.hom (pushoutSection H hUST ⋯ ⋯)).comp
          ((CommRingCat.Hom.hom ⋯.isoPushout.hom).comp
            (Pi.evalRingHom (fun i ↦ ↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, VX i)) i))).comp
    (Algebra.TensorProduct.piRight ↑Γ(S, US) ↑Γ(S, US) ↑Γ(T, UT) fun i ↦ ↑Γ(X, VX i)).toRingEquiv.toRingHom
hφ : Function.Injective ⇑φ
e : pushout (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≅
  CommRingCat.of (↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, UX)) :=
  ⋯.isoPushout.symm
H₁ :
  (CommRingCat.Hom.hom e.inv).comp Algebra.TensorProduct.includeLeftRingHom =
    CommRingCat.Hom.hom (pushout.inr (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST))
H₂ :
  ∀ (x : ↑Γ(T, UT)) (j : ι),
    φ (x ⊗ₜ[↑Γ(S, US)] 1) j =
      (ConcreteCategory.hom (pushoutSection H hUST ⋯ ⋯))
        ((ConcreteCategory.hom (pushout.inr (Scheme.Hom.appLE iX US (VX j) ⋯) (Scheme.Hom.appLE f US UT hUST))) x)
x : ↑Γ(T, UT)
j : ι
⊢ (ψY.comp
        ((CommRingCat.Hom.hom (pushoutSection H hUST hUSX hUY)).comp
          (CommRingCat.Hom.hom (pushout.inr (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST)))))
      x j =
    (φ.comp
        ((Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ).comp Algebra.TensorProduct.includeLeftRingHom))
      x j

Tactic:
simp [ψY, H₂, ← CategoryTheory.comp_apply, pushoutSection]

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

Goal state before:
pp: case refine_1
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
j : Fin n
⊢ (fun i ↦ (e₂.val i).degree.succ) j ≤ (fun i ↦ (e.val i).degree.succ) j

Tactic:
dsimp

Goal state after:
case refine_1
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
j : Fin n
⊢ (e₂.val j).degree.succ ≤ (e.val j).degree.succ
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 }
degBound_e₁_le : e₁.degBound ≤ e.degBound
⊢ ↑q₂ (e.val i).leadingCoeff = 0

Tactic:
simp [q₂, ← hi]

Goal state after:
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)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
⊢ ∃ V, ∃ (hxV : x ∈ V), V ≤ U ∧ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range

Tactic:
refine ⟨s.inf W ⊓ U, H, inf_le_right, ?_⟩

Goal state after:
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)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
⊢ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H)).range
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: case mpr
X Y : Scheme
g : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
⊢ (∃ (e : { domain := U, dense_domain := hU, hom := f }.domain = g.domain),
      { domain := U, dense_domain := hU, hom := f }.hom = (X.isoOfEq e).hom ≫ g.hom) →
    { domain := U, dense_domain := hU, hom := f } = g

Tactic:
obtain ⟨V, hV, g⟩ := g

Goal state after:
case mpr
X Y : Scheme
U : X.Opens
hU : Dense ↑U
f : ↑U ⟶ Y
V : X.Opens
hV : Dense ↑V
g : ↑V ⟶ Y
⊢ (∃ (e : { domain := U, dense_domain := hU, hom := f }.domain = { domain := V, dense_domain := hV, hom := g }.domain),
      { domain := U, dense_domain := hU, hom := f }.hom =
        (X.isoOfEq e).hom ≫ { domain := V, dense_domain := hV, hom := g }.hom) →
    { domain := U, dense_domain := hU, hom := f } = { domain := V, dense_domain := hV, hom := g }
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⟶ Y
inst✝ : IsDominant f
⊢ IsDominant (Hom.toPartialMap f).hom

Tactic:
dsimp

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⟶ Y
inst✝ : IsDominant f
⊢ IsDominant (⊤.ι ≫ f)
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
⊢ (f.restrict U hU hU').fromSpecStalkOfMem hx = f.fromSpecStalkOfMem ⋯

Tactic:
dsimp only [fromSpecStalkOfMem, restrict, Scheme.Opens.fromSpecStalkOfMem]

Goal state after:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
⊢ (Spec.map (inv (Hom.stalkMap U.ι ⟨x, hx⟩)) ≫ (↑U).fromSpecStalk ⟨x, hx⟩) ≫ X.homOfLE hU' ≫ f.hom =
    (Spec.map (inv (Hom.stalkMap f.domain.ι ⟨x, ⋯⟩)) ≫ (↑f.domain).fromSpecStalk ⟨x, ⋯⟩) ≫ f.hom
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  j ∈ insert i (Finset.image i' Finset.univ) →
    (IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ) ⟶
      j) :=
  fun j ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ)
j : 𝒰.I₀
⊢ D.map (g i ⋯) ≫ 𝟙 (D.obj i) = D.map (g (i' j) ⋯) ≫ D.map (f j)

Tactic:
← D.map_comp,

Goal state after:
I : Type u
inst✝⁴ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  j ∈ insert i (Finset.image i' Finset.univ) →
    (IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ) ⟶
      j) :=
  fun j ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ)
j : 𝒰.I₀
⊢ D.map (g i ⋯) ≫ 𝟙 (D.obj i) = D.map (g (i' j) ⋯ ≫ f j)
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

Tactic:
dsimp

Goal state after:
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 := 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) ≫ (g x).hom =
    ((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom
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

Tactic:
dsimp

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 := 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) ≫ (g y).hom =
    ((g y).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom