mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
hfP : (RingHom.ker fP).FG
algInst✝ : Algebra P' S := fP.toAlgebra
this✝¹ : FormallyEtale (MvPolynomial (Fin n) R) P'
this✝ : FormallySmooth R P'
this : Module.Free P' Ω[P'⁄R]
⊢ FormallySmooth R S

Tactic:
exact FormallySmooth.of_formallySmooth_residueField_tensor_aux (R := R) (S := S) hf₁ hfP

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : AdicCauchySequence I N
n : ℕ
y yₙ : M
hy : f y = ↑x (n + 1)
hyₙ : f yₙ = ↑x n
⊢ ↑x n - ↑x (n + 1) ∈ I ^ n • ⊤

Tactic:
← Submodule.neg_mem_iff,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : AdicCauchySequence I N
n : ℕ
y yₙ : M
hy : f y = ↑x (n + 1)
hyₙ : f yₙ = ↑x n
⊢ -(↑x n - ↑x (n + 1)) ∈ I ^ n • ⊤
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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
a : AdicCauchySequence I M
m n : ℕ
hmn : m ≤ n
hm : Submodule.map f (I ^ m • ⊤) ≤ I ^ m • ⊤
⊢ (fun n ↦ f (↑a n)) m ≡ (fun n ↦ f (↑a n)) n [SMOD I ^ m • ⊤]

Tactic:
apply SModEq.mono hm

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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
a : AdicCauchySequence I M
m n : ℕ
hmn : m ≤ n
hm : Submodule.map f (I ^ m • ⊤) ≤ I ^ m • ⊤
⊢ (fun n ↦ f (↑a n)) m ≡ (fun n ↦ f (↑a n)) n [SMOD Submodule.map f (I ^ m • ⊤)]
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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
n✝ : ℕ
⊢ (reduceModIdeal (I ^ n✝) f) (↑r n✝ • ↑x n✝) = ↑r n✝ • (reduceModIdeal (I ^ n✝) f) (↑x n✝)

Tactic:
rw [val_smul_eq_evalₐ_smul, val_smul_eq_evalₐ_smul, map_smul]

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

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
inst✝ : Module.Finite R M
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Tactic:
by
  obtain ⟨n, p, hp⟩ := Module.Finite.exists_fin' R M
  let f := ofTensorProduct I M ∘ₗ p.baseChange (AdicCompletion I R)
  let g := map I p ∘ₗ ofTensorProduct I (Fin n → R)
  have hfg : f = g := by
    ext
    simp [f, g]
  have hf : Function.Surjective f := by
    simp only [hfg, LinearMap.coe_comp, g]
    apply Function.Surjective.comp
    · exact AdicCompletion.map_surjective I hp
    · exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective
  exact Function.Surjective.of_comp hf

Goal state after:
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 ι σ
⊢ Function.Surjective ⇑P.cotangentComplexAux

Tactic:
rw [← LinearMap.range_eq_top, _root_.eq_top_iff, ← P.basisDeriv.span_eq, Submodule.span_le]
  rintro - ⟨i, rfl⟩
  use Cotangent.mk ⟨P.relation i, P.relation_mem_ker i⟩
  ext j
  rw [P.cotangentComplexAux_apply]
  simp

Goal state after:
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
⊢ (localizationAway T g).ker =
    Ideal.map ((localizationAway T g).ofComp P).toAlgHom (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1})

Tactic:
Ideal.map_span,

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
⊢ (localizationAway T g).ker =
    Ideal.span (⇑((localizationAway T g).ofComp P).toAlgHom '' {(rename Sum.inr) f * X (Sum.inl ()) - 1})
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 σ
inst✝¹ : Nontrivial S
inst✝ : Finite ι
P : SubmersivePresentation R S ι σ
⊢ Module.rank S Ω[S⁄R] = ↑P.dimension

Tactic:
simp only [rank_eq_card_basis P.basisKaehler, Fintype.card_compl_set,
    Presentation.dimension, Nat.card_eq_fintype_card, Set.card_range_of_injective P.map_inj]

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
A₀ : Subalgebra R A
B₀ : Type u
w✝¹ : CommRing B₀
w✝ : Algebra (↥A₀) B₀
hA₀ : A₀.FG
left✝ : Smooth (↥A₀) B₀
right✝ : Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
⊢ ∃ A₀ B₀ x x_1 x_2 x_3 x_4,
    Function.Injective ⇑(algebraMap A₀ A) ∧ FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)

Tactic:
use A₀, B₀, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
    Subtype.val_injective, ⟨A₀.fg_top.mpr hA₀⟩, inferInstance

Goal state after:
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
⊢ f.Smooth

Tactic:
by
  algebraize [f]
  rw [RingHom.Smooth]
  infer_instance

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

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
x✝⁷ x✝⁶ : Type u
x✝⁵ : CommRing x✝⁷
x✝⁴ : CommRing x✝⁶
f x✝³ : Type u
x✝² : CommRing f
x✝¹ : CommRing x✝³
x✝ : f →+* x✝³
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) x✝ ↔ x✝.Smooth

Tactic:
rw [RingHom.smooth_iff_locally_isStandardSmooth]

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case inr
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
this : ∀ (q₁ q₂ : MvPolynomial ι k), F = q₁ * q₂ → (aeval a) q₁ = 0 → IsUnit q₁ ∨ IsUnit q₂
h₁ : ¬(aeval a) q₁ = 0
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
exact .symm (this q₂ q₁ (e.trans (mul_comm ..)) <| by
      simpa [h₁, hFa] using Eq.symm <| congr(aeval a $e))

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_1
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  coeff (Finsupp.mapDomain (⇑e) σ).some
      (((optionEquivLeft k { b // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)).coeff
        (σ ((Equiv.optionSubtypeNe i) none))) =
    coeff σ F
⊢ False

Tactic:
Equiv.optionSubtypeNe_none,

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  coeff (Finsupp.mapDomain (⇑e) σ).some
      (((optionEquivLeft k { b // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)).coeff (σ i)) =
    coeff σ F
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

Tactic:
by
  have : CompactSpace X := (quasiCompact_iff_compactSpace f).mp inferInstance
  have : UniversallyClosed (X.toSpecΓ ≫ Spec.map f.appTop) := by
    rwa [← Scheme.toSpecΓ_naturality,
      MorphismProperty.cancel_right_of_respectsIso (P := @UniversallyClosed)]
  have : UniversallyClosed X.toSpecΓ := .of_comp_of_isSeparated _ (Spec.map f.appTop)
  rw [← IsIntegralHom.SpecMap_iff, IsIntegralHom.iff_universallyClosed_and_isAffineHom]
  exact ⟨.of_comp_surjective X.toSpecΓ _, inferInstance⟩

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

Goal state before:
pp: X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : LocallyOfFinitePresentation g
⊢ f ⁻¹ᵁ smoothLocus g = smoothLocus (f ≫ g)

Tactic:
by
  ext x
  refine (RingHom.FormallySmooth.respectsIso.cancel_right_isIso _ (f.stalkMap x)).symm.trans ?_
  rw [← CommRingCat.hom_comp, ← stalkMap_comp]
  rfl

Goal state after:
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
x : ↑S
⊢ F (((TensorProduct.mk ↑R ↑S ↑S) x) 1) = x

Tactic:
simp [F]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (W'⁄B).addY (⇑f ∘ P) (⇑f ∘ Q) = f ((W'⁄A).addY P Q)

Tactic:
by
  rw [← RingHom.coe_coe, ← map_addY, map_baseChange]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat) (φ : R ⟶ S),
    Function.Surjective ⇑(ConcreteCategory.hom φ) →
      RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x✝¹ : CommRing R
x✝ : Algebra (↑Γ(Y, U)) R
I : Ideal R
hI : I ^ 2 = ⊥
g₁ g₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] R
hg₁g₂ : (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₁ = (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₂
hg₁ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₁ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
hg₂ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₂ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
⊢ g₁ = g₂

Tactic:
have := H (.of R) (.of (R ⧸ I)) (CommRingCat.ofHom (Ideal.Quotient.mkₐ Γ(Y, U) I))
    Ideal.Quotient.mk_surjective (by simpa)
    (Spec.map (CommRingCat.ofHom g₁) ≫ hV.fromSpec) (Spec.map (CommRingCat.ofHom g₂) ≫ hV.fromSpec)
    (by simp only [← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, ← AlgHom.comp_toRingHom, *])
    (by simp only [Category.assoc, ← hU.SpecMap_appLE_fromSpec f hV hVU, ← Spec.map_comp_assoc, *])

Goal state after:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat) (φ : R ⟶ S),
    Function.Surjective ⇑(ConcreteCategory.hom φ) →
      RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x✝¹ : CommRing R
x✝ : Algebra (↑Γ(Y, U)) R
I : Ideal R
hI : I ^ 2 = ⊥
g₁ g₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] R
hg₁g₂ : (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₁ = (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₂
hg₁ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₁ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
hg₂ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₂ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
this : Spec.map (CommRingCat.ofHom ↑g₁) ≫ hV.fromSpec = Spec.map (CommRingCat.ofHom ↑g₂) ≫ hV.fromSpec
⊢ g₁ = g₂
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
f : K⟮X⟯
⊢ (∃ c, f = C c) ↔ f.num.natDegree = 0 ∧ f.denom.natDegree = 0

Tactic:
refine ⟨by rintro ⟨c, rfl⟩; simp, ?_⟩

Goal state after:
K : Type u
inst✝ : Field K
f : K⟮X⟯
⊢ f.num.natDegree = 0 ∧ f.denom.natDegree = 0 → ∃ c, f = C c
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
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)
⊢ X ^ m - p ∣ Polynomial.map (algebraMap R S) (eval (X ^ m) q)

Tactic:
change X ^ m - p ∣ Algebra.ofId R[X] S[X] _

Goal state after:
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)
⊢ X ^ m - p ∣ (Algebra.ofId R[X] S[X]) (eval (X ^ m) q)
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
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)
⊢ p.degree < (X ^ m).degree

Tactic:
simpa [← natDegree_lt_iff_degree_lt, hp0]

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

Goal state before:
pp: case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ ({ toFractionRing := Localization.mk p q } * { toFractionRing := Localization.mk p' q' }).liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk p q }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := Localization.mk p' q' }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯

Tactic:
← ofFractionRing_mul,

Goal state after:
case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk p q * Localization.mk p' q' }.liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk p q }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := Localization.mk p' q' }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk (φ (p * p')) ⟨φ ↑(q * q'), hqq'⟩ } =
    { toFractionRing := Localization.mk (φ p) ⟨φ ↑q, hq⟩ } * { toFractionRing := Localization.mk (φ p') ⟨φ ↑q', hq'⟩ }

Tactic:
← ofFractionRing_mul,

Goal state after:
case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ { toFractionRing := Localization.mk (φ (p * p')) ⟨φ ↑(q * q'), hqq'⟩ } =
    { toFractionRing := Localization.mk (φ p) ⟨φ ↑q, hq⟩ * Localization.mk (φ p') ⟨φ ↑q', hq'⟩ }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝¹ y✝ : R[X] × ↥R[X]⁰
⊢ ({ toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } * { toFractionRing := Localization.mk y✝.1 y✝.2 }).liftOn
      (fun p q ↦ φ p / φ q) ⋯ =
    { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯ *
      { toFractionRing := Localization.mk y✝.1 y✝.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯

Tactic:
← ofFractionRing_mul,

Goal state after:
case H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝¹ y✝ : R[X] × ↥R[X]⁰
⊢ { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 * Localization.mk y✝.1 y✝.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯ =
    { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯ *
      { toFractionRing := Localization.mk y✝.1 y✝.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ QuasiFiniteAt f x ↔ LocallyQuasiFinite (X.fromSpecStalk x ≫ f)

Tactic:
by
  rw [← SpecMap_stalkMap_fromSpecStalk, LocallyQuasiFinite.comp_iff,
    HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), QuasiFiniteAt]

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

Goal state before:
pp: case _pq
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
c : R
p q : K[X]
hq : q ≠ 0
⊢ { toFractionRing := IsLocalization.mk' (FractionRing K[X]) (c • p) ⟨q, ⋯⟩ } =
    { toFractionRing := (algebraMap K[X] (FractionRing K[X])) ((algebraMap R K[X]) c) } *
      { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p ⟨q, ⋯⟩ }

Tactic:
← ofFractionRing_mul,

Goal state after:
case _pq
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
c : R
p q : K[X]
hq : q ≠ 0
⊢ { toFractionRing := IsLocalization.mk' (FractionRing K[X]) (c • p) ⟨q, ⋯⟩ } =
    {
      toFractionRing :=
        (algebraMap K[X] (FractionRing K[X])) ((algebraMap R K[X]) c) *
          IsLocalization.mk' (FractionRing K[X]) p ⟨q, ⋯⟩ }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inl
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p : K[X]
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 0) = φ p / φ 0

Tactic:
simp only [div_zero, map_zero]

Goal state after: