mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
⊢ etaleLocus R A = Set.univ ↔ Etale R A

Tactic:
by
  rw [etaleLocus_eq_univ_iff]
  refine ⟨fun H ↦ ⟨H, inferInstance⟩, fun _ ↦ inferInstance⟩

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
⊢ ∃ a, (map I f) a = y

Tactic:
suffices h : ∃ x : ℕ → M, ∀ n, x n ≡ x (n + 1) [SMOD (I ^ n • ⊤ : Submodule R M)] ∧
      Submodule.Quotient.mk (f (x n)) = eval I _ n y by
    obtain ⟨x, hx⟩ := h
    use AdicCompletion.mk I M ⟨x, fun h ↦
        eq_factor_of_eq_factor_succ (fun _ _ ↦ pow_smul_top_le I M) _ (fun n ↦ (hx n).1) h⟩
    ext n
    simp [hx n]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
⊢ ∃ x, ∀ (n : ℕ), x n ≡ x (n + 1) [SMOD I ^ n • ⊤] ∧ Submodule.Quotient.mk (f (x n)) = (eval I N n) y
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
⊢ P.jacobian = LinearMap.det P.aevalDifferential

Tactic:
by
  classical
  cases nonempty_fintype σ
  simp [← LinearMap.det_toMatrix', P.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix,
    jacobian_eq_jacobiMatrix_det, RingHom.map_det, P.algebraMap_eq]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
x : σ
⊢ P.relation x ∈ Set.range ⇑(MvPolynomial.map (algebraMap R₀ R))

Tactic:
MvPolynomial.mem_range_map_iff_coeffs_subset

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
x : σ
⊢ ↑(MvPolynomial.coeffs (P.relation x)) ⊆ Set.range ⇑(algebraMap R₀ R)
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ Ideal.span {C g * X () - 1} = Ideal.span {C g * Sum.elim X (⇑C ∘ P.val) (Sum.inl ()) - 1}

Tactic:
Sum.elim_inl

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ Ideal.span {C g * X () - 1} = Ideal.span {C g * X () - 1}
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.dblY P = W.dblU P

Tactic:
by
  rw [dblU, ← dblY_of_Y_eq' hP hPz hQz hx hy hy', mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a.a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ P.ker * P.ker ≤
    Ideal.comap ((localizationAway T g).toComp P).toAlgHom (RingHom.ker (compLocalizationAwayAlgHom T g P))

Tactic:
← sq

Goal state after:
case a.a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
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
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ P.ker ^ 2 ≤ Ideal.comap ((localizationAway T g).toComp P).toAlgHom (RingHom.ker (compLocalizationAwayAlgHom T g P))
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
let e : (κ →₀ S) →ₗ[S] Ω[S⁄R] :=
    Finsupp.linearCombination S fun i : κ ↦ D R S (a i)

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
⊢ (algebraMap S (S ⊗[R] T)).IsStandardSmooth

Tactic:
rw [RingHom.IsStandardSmooth]

Goal state after:
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
⊢ Algebra.IsStandardSmooth S (S ⊗[R] T)
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsStandardSmooth R S
⊢ f.Smooth

Tactic:
rw [RingHom.Smooth]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsStandardSmooth R S
⊢ Algebra.Smooth R S
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
⊢ ∃ P' b,
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
cases subsingleton_or_nontrivial S
  · let P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
      { toGenerators := .ofSurjective (fun i : Unit ⊕ α ↦ 0) (Function.surjective_to_subsingleton _)
        relation _ := 1
        span_range_relation_eq_ker := by simpa using! (RingHom.ker_eq_top_of_subsingleton _).symm }
    have : Subsingleton P'.toExtension.Cotangent := Module.subsingleton S _
    exact ⟨P', default, by subsingleton, by subsingleton⟩
  have : Module.Finite S P.toExtension.Cotangent :=
    Algebra.Extension.Cotangent.finite P.fg_ker_of_finitePresentation
  exact exists_presentation_of_basis_cotangent _ <| Module.finBasis S P.toExtension.Cotangent

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

Goal state before:
pp: n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
U₂ : Z.Opens
hU₂ : IsAffineOpen U₂
V₂ : Y.Opens
hV₂ : IsAffineOpen V₂
hfx₂ : f x ∈ V₂
e₂ : V₂ ≤ g ⁻¹ᵁ U₂
hf₂ : IsStandardSmoothOfRelativeDimension m (CommRingCat.Hom.hom (Scheme.Hom.appLE g U₂ V₂ e₂))
U₁' : Y.Opens
hU₁' : IsAffineOpen U₁'
V₁' : X.Opens
hV₁' : IsAffineOpen V₁'
hx₁' : x ∈ V₁'
e₁' : V₁' ≤ f ⁻¹ᵁ U₁'
hf₁' : IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U₁' V₁' e₁'))
r : ↑Γ(Y, ↑⟨V₂, hV₂⟩)
s : ↑Γ(X, ↑⟨V₁', hV₁'⟩)
hx₁ : x ∈ X.basicOpen s
e₁ : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
hf₁ :
  IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V,
        ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (f ≫ g) ⁻¹ᵁ U),
          IsStandardSmoothOfRelativeDimension (n + m) (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) U V e))

Tactic:
have e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂ :=
      le_trans e₁ <| f.preimage_mono <| le_trans (Y.basicOpen_le r) e₂

Goal state after:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
U₂ : Z.Opens
hU₂ : IsAffineOpen U₂
V₂ : Y.Opens
hV₂ : IsAffineOpen V₂
hfx₂ : f x ∈ V₂
e₂ : V₂ ≤ g ⁻¹ᵁ U₂
hf₂ : IsStandardSmoothOfRelativeDimension m (CommRingCat.Hom.hom (Scheme.Hom.appLE g U₂ V₂ e₂))
U₁' : Y.Opens
hU₁' : IsAffineOpen U₁'
V₁' : X.Opens
hV₁' : IsAffineOpen V₁'
hx₁' : x ∈ V₁'
e₁' : V₁' ≤ f ⁻¹ᵁ U₁'
hf₁' : IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U₁' V₁' e₁'))
r : ↑Γ(Y, ↑⟨V₂, hV₂⟩)
s : ↑Γ(X, ↑⟨V₁', hV₁'⟩)
hx₁ : x ∈ X.basicOpen s
e₁ : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
hf₁ :
  IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))
e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V,
        ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (f ≫ g) ⁻¹ᵁ U),
          IsStandardSmoothOfRelativeDimension (n + m) (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) U V e))
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F)) = Ideal.span {e}
x : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
hx : e * x ∈ KaehlerDifferential.ideal ↑R ↑S
⊢ e * x ∈ KaehlerDifferential.ideal ↑R ↑S * KaehlerDifferential.ideal ↑R ↑S

Tactic:
← he,

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F)) = Ideal.span {e}
x : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
hx : e * x ∈ KaehlerDifferential.ideal ↑R ↑S
⊢ e * e * x ∈ KaehlerDifferential.ideal ↑R ↑S * KaehlerDifferential.ideal ↑R ↑S
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).negDblY (⇑f ∘ P) = f (W'.negDblY P)

Tactic:
by
  simp only [negDblY]
  map_simp

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

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : P'.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), P' f → P (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
h : P' f
hf : P (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    P' f → P (pullback.fst f g) → (∃ R, Z = Spec R) → P g
hZ : ¬∃ R, Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (pullback.snd f ι) (pullback.snd g ι) ≅ pullback (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫
      (pullbackAssoc f g g ι).symm ≪≫ pullback.congrHom ⋯ ⋯ ≪≫ (pullbackRightPullbackFstIso f ι (pullback.fst f g)).symm
⊢ e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)

Tactic:
apply pullback.hom_ext <;> simp [e, pullback.condition]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_4
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
h : IsStandardOpenImmersion R S
⊢ IsStandardOpenImmersion R T

Tactic:
by
  rw [Algebra.isStandardOpenImmersion_iff] at *
  obtain ⟨r, hr⟩ := h
  use r
  exact IsLocalization.isLocalization_of_algEquiv _ e

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).QuasiFinite ↔ Algebra.QuasiFinite R S

Tactic:
rw [RingHom.QuasiFinite, toAlgebra_algebraMap]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this✝ : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx : x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p)
a : S
ha : x • a ∈ Ideal.map (algebraMap R S) p
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : (aeval (x • a)) f = 0
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ (minpoly R a).natDegree
hip : (minpoly R a).coeff i ∉ p
hx0 : ¬x = 0
this :
  ∀ (i : ℕ),
    i ≠ (minpoly R a).natDegree →
      ∀ (p : Submodule R R),
        Ideal.span {x | ∃ i < f.natDegree, f.coeff i = x} ≤ p →
          Ideal.IsPrime p → (minpoly R a).coeff i * x ^ ((minpoly R a).natDegree - i) ∈ p
⊢ Ideal.span {x | ∃ i < f.natDegree, f.coeff i = x} ≤ p

Tactic:
simp +contextual [Ideal.span_le, Set.subset_def, LT.lt.ne, hf]

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

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
q : ↥K[X]⁰
⊢ RatFunc.mk p ↑q = { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p q }

Tactic:
by
  simp only [mk_eq_div', ← Localization.mk_eq_mk', FractionRing.mk_eq_div]

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
⊢ Ideal.map (algebraMap R ↥R[x]) I ≤ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)

Tactic:
rw [IsScalarTower.algebraMap_eq R R<x> S, ← Ideal.map_map]
    apply Ideal.le_comap_map

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
hx : (algebraMap R S) 1 ∈ Ideal.map (algebraMap R S) (comap (algebraMap R S) (conductor R x) ⊔ I)
⊢ 1 ∈ conductor R x ⊔ Ideal.map (algebraMap R S) I

Tactic:
rw [Ideal.map_sup, map_one] at hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
hx : 1 ∈ Ideal.map (algebraMap R S) (comap (algebraMap R S) (conductor R x)) ⊔ Ideal.map (algebraMap R S) I
⊢ 1 ∈ conductor R x ⊔ Ideal.map (algebraMap R S) I
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
f : K⟮X⟯
a : K
ha : Polynomial.C a = f.num
b : K
hb : Polynomial.C b = f.denom
⊢ (algebraMap K[X] K⟮X⟯) (Polynomial.C a) / (algebraMap K[X] K⟮X⟯) f.denom = C (a / b)

Tactic:
← hb,

Goal state after:
case h
K : Type u
inst✝ : Field K
f : K⟮X⟯
a : K
ha : Polynomial.C a = f.num
b : K
hb : Polynomial.C b = f.denom
⊢ (algebraMap K[X] K⟮X⟯) (Polynomial.C a) / (algebraMap K[X] K⟮X⟯) (Polynomial.C b) = C (a / b)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
⊢ IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)

Tactic:
refine ⟨fun H n ↦ ?mp, fun H ↦ ?mpr⟩

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : IsIntegral (MvPolynomial σ R) f
n : σ →₀ ℕ
⊢ IsIntegral R (coeff n f)

case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algInst✝ : Algebra ↑(Y.presheaf.obj (Opposite.op U)) ↑(Y.presheaf.stalk (f x)) :=
  (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).toAlgebra
this : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
⊢ (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).QuasiFinite

Tactic:
← (Y.presheaf.germ U _ (hVU hxV)).hom.algebraMap_toAlgebra,

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algInst✝ : Algebra ↑(Y.presheaf.obj (Opposite.op U)) ↑(Y.presheaf.stalk (f x)) :=
  (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).toAlgebra
this : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
⊢ (algebraMap ↑(Y.presheaf.obj (Opposite.op U)) ↑(Y.presheaf.stalk (f x))).QuasiFinite
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
⊢ (CommRingCat.Hom.hom (appLE f U V hVU)).QuasiFiniteAt (hV.primeIdealOf ⟨x, hxV⟩).asIdeal

Tactic:
by
  algebraize [(f.appLE U V hVU).hom]
  have H : (Y.presheaf.germ U _ (hVU hxV)).hom.QuasiFinite := by
    algebraize [(Y.presheaf.germ U _ (hVU hxV)).hom]
    have := hU.isLocalization_stalk ⟨f x, (hVU hxV)⟩
    rw [← (Y.presheaf.germ U _ (hVU hxV)).hom.algebraMap_toAlgebra,
      RingHom.quasiFinite_algebraMap]
    exact .of_isLocalization (hU.primeIdealOf ⟨_, hVU hxV⟩).asIdeal.primeCompl
  algebraize [(X.presheaf.germ V x hxV).hom]
  have := hV.isLocalization_stalk ⟨x, hxV⟩
  let e := IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hxV⟩).asIdeal.primeCompl
    (X.presheaf.stalk (⟨x, hxV⟩ : V.1)) (Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal)
  rw [RingHom.QuasiFiniteAt, Algebra.QuasiFiniteAt, ← RingHom.quasiFinite_algebraMap]
  convert! (RingHom.QuasiFinite.of_finite e.finite).comp (hx.comp H)
  rw [← CommRingCat.hom_comp, f.germ_stalkMap, ← X.presheaf.germ_res (homOfLE hVU) _ hxV,
    Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map_assoc, CommRingCat.hom_comp, ← RingHom.comp_assoc,
    IsScalarTower.algebraMap_eq Γ(Y, U) Γ(X, V), e.toAlgHom.comp_algebraMap.symm]
  rfl

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
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
⊢ c • RatFunc.mk p q = c • ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q)

Tactic:
mk_eq_div

Goal state after:
K : Type u
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
R : Type u_1
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p q : K[X]
⊢ c • ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) = c • ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
⊢ (C a.leadingCoeff⁻¹).degree + (gcd p q).degree ≤ q.degree

Tactic:
Polynomial.degree_C hainv,

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
⊢ 0 + (gcd p q).degree ≤ q.degree
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ Associated x⁻¹.denom x.num

Tactic:
by
  apply Associated.symm
  convert! associated_num_inv (inv_ne_zero hx)
  rw [inv_inv]

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
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
⊢ IsStandardEtale R Sₛ

Tactic:
obtain ⟨p, n, hp⟩ := P.exists_mul_aeval_x_g_pow_eq_aeval_x s

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * (aeval P.x) P.g ^ n = (aeval P.x) p
⊢ IsStandardEtale R Sₛ