mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hb0 : (Ideal.Quotient.mk I) s ∈ (R ⧸ I)⁰
hb :
  map (algebraMap (R ⧸ I) I.ResidueField) (IsLocalization.integerNormalization (R ⧸ I)⁰ x) = (Ideal.Quotient.mk I) s • x
⊢ ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x

Tactic:
refine ⟨s, by simpa [Ideal.Quotient.eq_zero_iff_mem] using! hb0, ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hb0 : (Ideal.Quotient.mk I) s ∈ (R ⧸ I)⁰
hb :
  map (algebraMap (R ⧸ I) I.ResidueField) (IsLocalization.integerNormalization (R ⧸ I)⁰ x) = (Ideal.Quotient.mk I) s • x
⊢ map (algebraMap R I.ResidueField) r = s • x
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
p✝ : Ideal R
q : Ideal S
inst✝² : q.IsPrime
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : T ≃ₐ[R] S
x✝ : S
⊢ x✝ ∈ p ↔ x✝ ∈ Ideal.comap (↑f.symm) (Ideal.comap f.toRingEquiv.toRingHom p)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
⊢ (residueFieldMapCAlgEquiv I J hJ) ((residueFieldMapCAlgEquiv I J hJ).symm RatFunc.X) =
    (residueFieldMapCAlgEquiv I J hJ) ((algebraMap R[X] J.ResidueField) X)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
I : Ideal R
inst✝⁵ : I.IsPrime
J : Ideal R[X]
inst✝⁴ : J.IsPrime
inst✝³ : J.LiesOver I
inst✝² : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra I J
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
⊢ ((AlgHom.restrictScalars R (aeval (1 ⊗ₜ[R] f X))).comp (mapAlgHom (Algebra.ofId R p.ResidueField))) X =
    (Algebra.TensorProduct.includeRight.comp f) X

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
I : Ideal R
inst✝⁵ : I.IsPrime
J : Ideal R[X]
inst✝⁴ : J.IsPrime
inst✝³ : J.LiesOver I
inst✝² : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra I J
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
⊢ (((Algebra.TensorProduct.lift
                (Algebra.ofId p.ResidueField
                  (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
                (f.liftOfSurjective hf
                  ((Ideal.Quotient.mkₐ R (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
                    (mapAlgHom (Algebra.ofId R p.ResidueField)))
                  ⋯)
                ⋯).comp
            (Ideal.Quotient.liftₐ (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))
              (aeval (1 ⊗ₜ[R] f X)) ⋯)).comp
        (Ideal.Quotient.mkₐ p.ResidueField (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))))
      X =
    ((AlgHom.id p.ResidueField
            (p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
        (Ideal.Quotient.mkₐ p.ResidueField (Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))))
      X

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal T
inst✝¹ : q.IsPrime
inst✝ : WeaklyQuasiFiniteAt R q
this : QuasiFiniteAt S (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))) q)
H : Ideal.map (algebraMap R T) (Ideal.under R q) ≤ Ideal.map (algebraMap S T) (Ideal.under S q)
⊢ q ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))) ⊥ =
    Ideal.comap
      ((Ideal.quotientMapₐ (Ideal.map (algebraMap S T) (Ideal.under S q)) (AlgHom.id S T) H).comp
        (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))))
      (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap S T) (Ideal.under S q))) q)

Tactic:
refine .trans ?_ (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal T
inst✝¹ : q.IsPrime
inst✝ : WeaklyQuasiFiniteAt R q
this : QuasiFiniteAt S (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))) q)
H : Ideal.map (algebraMap R T) (Ideal.under R q) ≤ Ideal.map (algebraMap S T) (Ideal.under S q)
⊢ q ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))) ⊥ =
    q ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap S T) (Ideal.under S q))) ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
⊢ id (IsLocallyArtinian X)

Tactic:
wlog hY : ∃ R, Y = Spec R

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y],
    (∃ R, Y = Spec R) → id (IsLocallyArtinian X)
hY : ¬∃ R, Y = Spec R
⊢ id (IsLocallyArtinian X)

X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
⊢ id (IsLocallyArtinian X)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
⊢ IsLocallyArtinian X

Tactic:
by
  change id _ -- avoid typeclass synthesis from getting stuck on the wlog hypothesis.
  wlog hY : ∃ R, Y = Spec R
  · exact (isLocallyArtinian_iff_openCover (Y.affineCover.pullback₁ f)).mpr fun i ↦
      this (pullback.snd _ _) ⟨_, rfl⟩
  wlog hX : ∃ S, X = Spec S
  · exact (isLocallyArtinian_iff_openCover X.affineCover).mpr fun i ↦
      this (X.affineCover.f i ≫ f) hY ⟨_, rfl⟩
  obtain ⟨R, rfl⟩ := hY
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  simp only [isLocallyArtinianScheme_Spec, HasRingHomProperty.Spec_iff, id_eq] at *
  algebraize [φ.hom]
  have : Module.Finite R S := .of_quasiFinite
  exact .of_finite R S

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian Y
⊢ id (IsFinite f)

Tactic:
wlog hY : ∃ R, Y = Spec R

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian Y],
    (∃ R, Y = Spec R) → id (IsFinite f)
hY : ¬∃ R, Y = Spec R
⊢ id (IsFinite f)

X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
⊢ id (IsFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
⊢ id (LocallyQuasiFinite f)

Tactic:
wlog hY : ∃ R, Y = Spec R

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    (∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
⊢ id (LocallyQuasiFinite f)

X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
hY : ∃ R, Y = Spec R
⊢ id (LocallyQuasiFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this✝ :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    (∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
this : ∀ (x : ↥Y), IsLocallyArtinian (Hom.fiber f x)
⊢ (Y.affineCover.X i).fromSpecResidueField x ≫ Y.affineCover.f i =
    Spec.map (Hom.residueFieldMap (Y.affineCover.f i) x) ≫ Y.fromSpecResidueField ((Y.affineCover.f i) x)

Tactic:
simp

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

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this✝ :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R),
    (∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) →
      (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
this : ∀ (x : ↥(Spec R)), IsLocallyArtinian (Hom.fiber f x)
⊢ (X.affineCover.f i ≫ f) ≫ 𝟙 (Spec R) = X.affineCover.f i ≫ f

Tactic:
simp

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

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this✝ :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R),
    (∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) →
      (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(Spec R)
this : ∀ (x : ↥(Spec R)), IsLocallyArtinian (Hom.fiber f x)
⊢ (Spec R).fromSpecResidueField x ≫ 𝟙 (Spec R) = 𝟙 (Spec ((Spec R).residueField x)) ≫ (Spec R).fromSpecResidueField x

Tactic:
simp

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

Goal state before:
pp: case refine_1.refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))

Tactic:
simp

Goal state after:
case refine_1.refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Spec.map φ = Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})
⊢ id (LocallyQuasiFinite f)

Tactic:
wlog hY : ∃ R, Y = Spec R

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f],
    (∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
⊢ id (LocallyQuasiFinite f)

X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})
hY : ∃ R, Y = Spec R
⊢ id (LocallyQuasiFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite
⊢ id (LocallyQuasiFinite f)

Tactic:
wlog hY : ∃ R, Y = Spec R

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f],
    (∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
⊢ id (LocallyQuasiFinite f)

X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite
hY : ∃ R, Y = Spec R
⊢ id (LocallyQuasiFinite f)
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : X.AffineZariskiSite
f : U ⟶ V
⊢ ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case e'_2.e'_1.e'_6
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := ⋯
F : (directedCover X).I₀ ⥤ Scheme := ⋯
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
e_1✝ : (cocone X).pt.Opens = X.Opens
⊢ ↑U = Hom.opensRange ((directedCover X).f U)

Tactic:
simp

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

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
inst✝² : LocallyQuasiFinite f✝
x : ↥X
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
x✝¹ : J.IsPrime
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.QuasiFinite R S
x✝ : R
⊢ ((Localization.localRingHom (Ideal.comap f J) J f ⋯).comp (algebraMap R (Localization.AtPrime (Ideal.comap f J))))
      x✝ =
    (algebraMap R (Localization.AtPrime J)) x✝

Tactic:
simp

Goal state after:
X Y : Scheme
f✝ : X ⟶ Y
inst✝² : LocallyQuasiFinite f✝
x : ↥X
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
x✝¹ : J.IsPrime
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.QuasiFinite R S
x✝ : R
⊢ (algebraMap S (Localization.AtPrime J)) (f x✝) = (algebraMap R (Localization.AtPrime J)) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
x : ↥X
⊢ QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩}

Tactic:
wlog hY : ∃ R, Y = Spec R

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
x : ↥X
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
⊢ QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩}

X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
x : ↥X
hY : ∃ R, Y = Spec R
⊢ QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩}
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: L : Type u_2
R : Type u_3
inst✝¹ : Field L
inst✝ : CommRing R
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
x : R[X]
⊢ φ x / φ ↑1 = φ x

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
⊢ 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f
K✝ : Type u
inst✝¹¹ : CommRing K✝
inst✝¹⁰ : IsDomain K✝
A : Type u_1
k : Type u_2
K : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A[X] k
inst✝⁴ : Algebra A[X] K
inst✝³ : SMul k K
inst✝² : FaithfulSMul A[X] k
inst✝¹ : FaithfulSMul A[X] K
inst✝ : IsScalarTower A[X] k K
b : k
c : K
p q : A[X]
hq : q ≠ 0
⊢ ((algebraMap A[X] A⟮X⟯) p • b) • c = (algebraMap A[X] A⟮X⟯) p • b • c

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
⊢ (P.lift P.X ⋯) P.X = (AlgHom.id R P.Ring) P.X

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
f : P.Ring →ₐ[R] S
⊢ ((fun x ↦ P.lift ↑x ⋯) ((fun f ↦ ⟨f P.X, ⋯⟩) f)) P.X = f P.X

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
x : { x // P.HasMap x }
⊢ (fun f ↦ ⟨f P.X, ⋯⟩) ((fun x ↦ P.lift ↑x ⋯) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (0, 1) =
    have r := gcd 0 1;
    (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_2
K : Type u
inst✝ : Field K
⊢ 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_3
K : Type u
inst✝ : Field K
⊢ 0 = C (1 / gcd 0 1).leadingCoeff⁻¹ * (0 / gcd 0 1)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_2
K : Type u
inst✝ : Field K
⊢ 1 = (algebraMap K[X] K⟮X⟯) 1 / (algebraMap K[X] K⟮X⟯) 1

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_3
K : Type u
inst✝ : Field K
⊢ 1 = C (1 / gcd 1 1).leadingCoeff⁻¹ * (1 / gcd 1 1)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_2
K : Type u
inst✝ : Field K
p : K[X]
⊢ (algebraMap K[X] K⟮X⟯) p = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 1

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_3
K : Type u
inst✝ : Field K
p : K[X]
⊢ p = C (1 / gcd p 1).leadingCoeff⁻¹ * (p / gcd p 1)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_3
K : Type u
inst✝ : Field K
⊢ 1 = C (1 / gcd 0 1).leadingCoeff⁻¹ * (1 / gcd 0 1)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case e'_3
K : Type u
inst✝ : Field K
p : K[X]
⊢ 1 = C (1 / gcd p 1).leadingCoeff⁻¹ * (1 / gcd p 1)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ {C P.f, Y * C P.g - 1}.Finite

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ ((IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯).comp
        (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯))
      P.X =
    (AlgHom.id R P.Ring) P.X

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case e'_3.e'_8.h₁
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
e : P.Fiber S ≃ₐ[P.ResidueField] P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I :=
  fiberEquivQuotient (aeval x) hx' P
a : R
⊢ e ((aeval (1 ⊗ₜ[R] x)) (C ((algebraMap R P.ResidueField) a))) =
    (Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker ↑(aeval x))))
      (C ((algebraMap R P.ResidueField) a))

Tactic:
rw [aeval_C, AlgEquiv.commutes]

Goal state after:
case e'_3.e'_8.h₁
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
e : P.Fiber S ≃ₐ[P.ResidueField] P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I :=
  fiberEquivQuotient (aeval x) hx' P
a : R
⊢ (algebraMap P.ResidueField (P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I))
      ((algebraMap R P.ResidueField) a) =
    (Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker ↑(aeval x))))
      (C ((algebraMap R P.ResidueField) a))
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
B✝ : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
B : Type u_4
inst✝¹ : CommRing B
inst✝ : Algebra R B
⊢ (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R B).val) 0 ∈ integralClosure S (S ⊗[R] B)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
p : R[X]
⊢ (((MvPolynomial.aeval P.toPresentation.val).comp ↑(Bivariate.equivMvPolynomial R)).comp CAlgHom) X = (aeval P.x) X

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
e : S ≃ₐ[R] T
⊢ (P.lift (e P.x) ⋯) P.X = ((↑e).comp (P.lift P.x ⋯)) P.X

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ X.Monic

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ derivative X * 1 + X * 0 = 1 ^ 0

Tactic:
simp

Goal state after: