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
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ (Module.support A Ω[A⁄R])ᶜ ∩ (Module.support A (H1Cotangent R A))ᶜ ↔
    FormallyEtale R (Localization.Away f)

Tactic:
Set.subset_inter_iff,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ (Module.support A Ω[A⁄R])ᶜ ∧
      ↑(PrimeSpectrum.basicOpen f) ⊆ (Module.support A (H1Cotangent R A))ᶜ ↔
    FormallyEtale R (Localization.Away f)
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
x✝ : ℕ
d : N := ⋯.choose
y : M := ⋯.choose
hdy : f y = ↑x (k + 0) - d
hdmem : ⋯.choose ∈ I ^ (k + 0) • ⊤
⊢ y ∈ {a | f a - ↑x (k + Nat.zero) ∈ I ^ (k + Nat.zero) • ⊤}

Tactic:
by simpa [hdy]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
x : M
hy : x ∈ Submodule.span R (Set.range (v ∘ a))
⊢ s x = 0

Tactic:
induction hy using Submodule.span_induction with

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
⊢ ⊤ ≤ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

Tactic:
rintro p -

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
p : P
⊢ p ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
⊢ Function.Surjective ⇑(p.projectionOnto q hpq ∘ₗ f)

Tactic:
by
  rw [← Set.surjOn_univ, LinearMap.coe_comp, Set.surjOn_comp_iff, Set.image_univ]
  rw [← LinearMap.coe_range, ← Submodule.top_coe (R := R), surjOn_iff_le_map,
    ← hfg.linearMap_ker_eq]
  intro x triv
  obtain ⟨a, haq, ha⟩ : g x.val ∈ q.map g := by rwa [hmap]
  exact ⟨x - a, by simp [← ha], by simpa⟩

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
inst✝⁵ : Finite σ
P : SubmersivePresentation 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₀
⊢ (MvPolynomial.aeval P.val) (P.invJacobianOfHasCoeffs R₀) = ↑⋯.unit⁻¹

Tactic:
simpa [-map_invJacobianOfHasCoeffs, MvPolynomial.aeval_map_algebraMap] using
    congr(MvPolynomial.aeval P.val $(P.map_invJacobianOfHasCoeffs R₀))

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 ι σ
inst✝⁶ : Finite σ
P : SubmersivePresentation 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₀
inst✝ : FaithfulSMul R₀ R
this✝ : Fintype σ := Fintype.ofFinite σ
this :
  (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀) *
      (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.invJacobianOfHasCoeffs R₀) =
    1
⊢ (P.ofHasCoeffs R₀).jacobian =
    (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀)

Tactic:
rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]

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 ι σ
inst✝⁶ : Finite σ
P : SubmersivePresentation 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₀
inst✝ : FaithfulSMul R₀ R
this✝ : Fintype σ := Fintype.ofFinite σ
this :
  (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀) *
      (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.invJacobianOfHasCoeffs R₀) =
    1
⊢ (algebraMap (P.ofHasCoeffs R₀).Ring (Presentation.ModelOfHasCoeffs R₀)) (P.ofHasCoeffs R₀).jacobiMatrix.det =
    (Ideal.Quotient.mk (Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))) (P.jacobianOfHasCoeffs R₀)
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

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
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
j : σ
⊢ ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map j)) (P.relation x)) = 0

Tactic:
apply heq

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] := P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm
⊢ Function.Bijective
    ⇑(LinearMap.linearProjOfIsCompl (Submodule.span S (Set.range fun x ↦ Finsupp.single (v x) 1))
          (Finsupp.lmapDomain S S u) ⋯ ⋯ ∘ₗ
        f)

Tactic:
have hfg : Function.Exact f g := by
    simp only [f, g, LinearEquiv.conj_exact_iff_exact]
    exact Extension.exact_cotangentComplex_toKaehler

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] := P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm
hfg : Function.Exact ⇑f ⇑g
⊢ Function.Bijective
    ⇑(LinearMap.linearProjOfIsCompl (Submodule.span S (Set.range fun x ↦ Finsupp.single (v x) 1))
          (Finsupp.lmapDomain S S u) ⋯ ⋯ ∘ₗ
        f)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension n (f.comp e.toRingHom)

Tactic:
by
    rw [← add_zero n]
    exact hf.comp (IsStandardSmoothOfRelativeDimension.equiv e)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
⊢ x ∈ smoothLocus f

Tactic:
have := f.smooth_appLE hU hV hVU

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
⊢ x ∈ smoothLocus f
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case inr
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this✝ : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id ↑s
⊢ LinearIndepOn k (fun x ↦ x ^ p) ↑s

Tactic:
apply hs.map_of_injective_injective (frobeniusEquiv k p).symm (frobenius K p).toAddMonoidHom <;>
    simp [frobenius, Algebra.smul_def, mul_pow, ← map_pow, frobeniusEquiv_symm_pow]

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

Goal state before:
pp: case a
P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P' ((T.isoSpec.inv ≫ p) ≫ f)

pp: case a
P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P (pullback.fst ((T.isoSpec.inv ≫ p) ≫ f) g)

Tactic:
· rw [Category.assoc, P'.cancel_left_of_respectsIso]
    exact P'.comp_mem _ _ hp h

Goal state after:
case a
P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P (pullback.fst ((T.isoSpec.inv ≫ p) ≫ f) g)
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ IsStandardOpenImmersion

Tactic:
by
  refine .mk respectsIso ?_
  introv h
  rw [isStandardOpenImmersion_algebraMap] at h ⊢
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x✝ : S
A : Subalgebra R R[X] := Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}
this : Algebra R[X] S[X] := algebra R S
x y : S
hx✝ : x ∈ Submodule.span S (⇑(algebraMap R S) '' ↑I)
hy✝ : y ∈ Submodule.span S (⇑(algebraMap R S) '' ↑I)
hx : IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C x * X)
hy : IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C y * X)
⊢ IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C (x + y) * X)

Tactic:
simpa [add_mul] using hx.add hy

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
s : S
inst✝ : IsNoetherianRing R
H' : R⁰ ≤ Submonoid.comap (algebraMap R S) S⁰
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • s ^ n ∈ (algebraMap R S).range
⊢ Subalgebra.toSubmodule R[s] ≤
    Submodule.comap (IsScalarTower.toAlgHom R S (Localization.Away ((algebraMap R S) r))).toLinearMap
      (R ∙ Localization.Away.invSelf ((algebraMap R S) r))

Tactic:
Algebra.adjoin_eq_span,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
s : S
inst✝ : IsNoetherianRing R
H' : R⁰ ≤ Submonoid.comap (algebraMap R S) S⁰
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • s ^ n ∈ (algebraMap R S).range
⊢ Submodule.span R ↑(Submonoid.closure {s}) ≤
    Submodule.comap (IsScalarTower.toAlgHom R S (Localization.Away ((algebraMap R S) r))).toLinearMap
      (R ∙ Localization.Away.invSelf ((algebraMap R S) r))
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
⊢ f = C (a / b)

Tactic:
← num_div_denom f,

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⟯) f.num / (algebraMap K[X] K⟮X⟯) f.denom = C (a / b)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L
h : Transcendental K f
⊢ (algEquivOfTranscendental f h).symm (AdjoinSimple.gen K f) = X

Tactic:
by
  simp [algEquivOfTranscendental, ← algebraMap_eq_gen_self]

Goal state after:
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
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
p : S[X]
hp : IsAlmostIntegral R[X] p
i : ℕ
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
by
  have H {q : S[X]} (hq : IsAlmostIntegral R[X] q) : IsAlmostIntegral R q.leadingCoeff := by
    obtain ⟨p, hp, hp'⟩ := hq
    refine ⟨p.leadingCoeff, by simpa using hp, fun n ↦ ?_⟩
    obtain ⟨r, hr⟩ := hp' n
    simp only [Algebra.smul_def, algebraMap_def, coe_mapRingHom] at hr ⊢
    by_cases h : algebraMap R S p.leadingCoeff * q.leadingCoeff ^ n = 0
    · simp [h]
    have h' : q.leadingCoeff ^ n ≠ 0 := by aesop
    use r.leadingCoeff
    simp only [← leadingCoeff_map_of_injective (FaithfulSMul.algebraMap_injective R S), hr] at h ⊢
    rw [← leadingCoeff_pow' h'] at h ⊢
    rw [leadingCoeff_mul' h]
  induction hn : p.natDegree using Nat.strong_induction_on generalizing p with | h n IH =>
  by_cases hp' : p.natDegree = 0
  · obtain ⟨p, rfl⟩ := natDegree_eq_zero.mp hp'
    simp only [coeff_C]
    split_ifs with h
    · simpa using H hp
    · exact (completeIntegralClosure R S).zero_mem
  by_cases hi : i = p.natDegree
  · simp [hi, H hp]
  have : IsAlmostIntegral R[X] p.eraseLead := by
    rw [← self_sub_monomial_natDegree_leadingCoeff, ← mem_completeIntegralClosure,
      ← C_mul_X_pow_eq_monomial, ← map_X (algebraMap R S), ← Polynomial.map_pow]
    refine sub_mem hp (mul_mem ?_ (algebraMap_mem (R := R[X]) _ _))
    obtain ⟨r, hr, hr'⟩ := H hp
    refine ⟨C r, by simpa using hr, fun n ↦ ?_⟩
    obtain ⟨s, hs⟩ := hr' n
    exact ⟨C s, by simp [Algebra.smul_def, hs]⟩
  simpa [hi, eraseLead_coeff_of_ne] using
    IH (p := p.eraseLead) _ (p.eraseLead_natDegree_le.trans_lt (by lia)) this rfl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case inr.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
this✝¹ : (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)
this✝ : X ^ m - p ∣ Polynomial.map (algebraMap R S) (eval (X ^ m) q)
this : IsIntegral R (-(X ^ m - p).coeff i)
hi : p.natDegree < i
⊢ IsIntegral R (p.coeff i)

Tactic:
· simp [coeff_eq_zero_of_natDegree_lt hi, isIntegral_zero]

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
hJ : J = Ideal.map C I
⊢ J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField

Tactic:
by
  letI f : J.ResidueField →+* RatFunc I.ResidueField := by
    refine Ideal.ResidueField.lift _
        ((algebraMap I.ResidueField[X] _).comp (mapRingHom (algebraMap _ _))) ?_ ?_
    · simp [hJ, Ideal.map_le_iff_le_comap, RingHom.comap_ker _ C, mapRingHom_comp_C,
        RingHom.ker_comp_of_injective, C_injective,
        FaithfulSMul.algebraMap_injective I.ResidueField[X] (RatFunc I.ResidueField)]
    · rintro x (hx : x ∉ J)
      suffices ∃ i, x.coeff i ∉ I by simpa [IsUnit.mem_submonoid_iff, Polynomial.ext_iff]
      contrapose! hx
      rwa [hJ, Ideal.mem_map_C_iff]
  haveI hf : f.comp (algebraMap I.ResidueField _) = algebraMap _ _ := by
    ext
    simp [f, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R R[X] J.ResidueField]
  refine .ofAlgHom ⟨f, fun r ↦ congr($hf r)⟩
      (RatFunc.liftAlgHom (aeval (algebraMap R[X] _ X)) fun x ↦ ?_) ?_ ?_
  · suffices Function.Injective (aeval (R := I.ResidueField) (algebraMap R[X] J.ResidueField X)) by
      simp [← this.eq_iff]
    rw [injective_iff_map_eq_zero]
    intro x hx
    obtain ⟨r, hr⟩ := map_surjective _ Ideal.Quotient.mk_surjective
      (IsLocalization.integerNormalization (R ⧸ I)⁰ x)
    obtain ⟨s, hs, hr⟩ : ∃ s ∉ I, r.map (algebraMap _ _) = s • x := by
      obtain ⟨b, hb0, hb⟩ := IsLocalization.integerNormalization_spec (R ⧸ I)⁰ x
      obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective b
      refine ⟨s, by simpa [Ideal.Quotient.eq_zero_iff_mem] using! hb0, ?_⟩
      simpa [← hr, map_map, ← Ideal.Quotient.algebraMap_eq] using! hb
    replace hx : r ∈ J := by
      apply_fun aeval (algebraMap R[X] J.ResidueField X) at hr
      simpa [hx, aeval_map_algebraMap, aeval_algebraMap_apply, Algebra.smul_def] using! hr
    refine ((IsUnit.mk0 (algebraMap R I.ResidueField s) (by simpa)).map C).mul_right_injective ?_
    simp only [← algebraMap_eq, ← Algebra.smul_def]
    rw [algebraMap_smul]
    simp only [← hr]
    simpa [Polynomial.ext_iff, Ideal.mem_map_C_iff] using! hJ.le hx
  · apply AlgHom.coe_ringHom_injective
    apply IsFractionRing.injective_comp_algebraMap (A := I.ResidueField[X])
    dsimp [RatFunc.liftAlgHom]
    simp only [AlgHom.comp_toRingHom, AlgHom.coe_ringHom_mk, RingHom.comp_assoc,
      RatFunc.liftRingHom_comp_algebraMap, RingHomCompTriple.comp_eq, f]
    ext <;> simp [← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R R[X] J.ResidueField]
  · apply AlgHom.coe_ringHom_injective
    ext
    · simp [f, RatFunc.liftAlgHom, ← IsScalarTower.algebraMap_apply]; rfl
    · simp [f, RatFunc.liftAlgHom]

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

Goal state before:
pp: case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) ≠ 0

Tactic:
· refine algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp ?_)
    exact inv_ne_zero (Polynomial.leadingCoeff_ne_zero.mpr q_div_ne_zero)

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

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
f : K⟮X⟯
⊢ (map φ hφ) f = (algebraMap R[X] R⟮X⟯) (φ f.num) / (algebraMap R[X] R⟮X⟯) (φ f.denom)

Tactic:
← num_div_denom f,

Goal state after:
K : Type u
inst✝⁴ : Field K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
f : K⟮X⟯
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) f.num / (algebraMap K[X] K⟮X⟯) f.denom) =
    (algebraMap R[X] R⟮X⟯) (φ ((algebraMap K[X] K⟮X⟯) f.num / (algebraMap K[X] K⟮X⟯) f.denom).num) /
      (algebraMap R[X] R⟮X⟯) (φ ((algebraMap K[X] K⟮X⟯) f.num / (algebraMap K[X] K⟮X⟯) f.denom).denom)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
f : K⟮X⟯
⊢ (liftMonoidWithZeroHom φ hφ) f = φ f.num / φ f.denom

Tactic:
← num_div_denom f,

Goal state after:
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
f : K⟮X⟯
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] K⟮X⟯) f.num / (algebraMap K[X] K⟮X⟯) f.denom) =
    φ ((algebraMap K[X] K⟮X⟯) f.num / (algebraMap K[X] K⟮X⟯) f.denom).num /
      φ ((algebraMap K[X] K⟮X⟯) f.num / (algebraMap K[X] K⟮X⟯) f.denom).denom