mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr.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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ (p' * ↑q + p * ↑q') * (φ ↑q * φ ↑q') = (φ p * φ ↑q' + φ ↑q * φ p') * φ ↑(q * q')

Tactic:
mul_comm _ (φ p'),

Goal state after:
case inr.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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ (p' * ↑q + p * ↑q') * (φ ↑q * φ ↑q') = (φ p * φ ↑q' + φ p' * φ ↑q) * φ ↑(q * q')
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]
⊢ (algebraMap K[X] K⟮X⟯) (c • p) / (algebraMap K[X] K⟮X⟯) q = c • ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q)

Tactic:
by
  rw [← mk_eq_div, mk_smul, mk_eq_div]

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

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : K⟮X⟯ → Prop
x : K⟮X⟯
f : ∀ (p q : K[X]), q ≠ 0 → P ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q)
p q : K[X]
hq : q ≠ 0
⊢ P (RatFunc.mk p q)

Tactic:
by simpa using f p q hq

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ x.num * q = p * x.denom ↔ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

Tactic:
by
  rw [← (algebraMap_injective K).eq_iff, eq_div_iff (algebraMap_ne_zero hq)]
  conv_rhs => rw [← num_div_denom x]
  rw [map_mul, map_mul, div_eq_mul_inv, mul_assoc, mul_comm (Inv.inv _), ←
    mul_assoc, ← div_eq_mul_inv, div_eq_iff]
  exact algebraMap_ne_zero (denom_ne_zero x)

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

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
r : MvPolynomial σ R
⊢ e₀.toRingEquiv.toFun ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)) r) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ B)) r

Tactic:
by
        change e₀.toRingHom.comp (algebraMap _ _) r = _
        congr 1
        ext <;> simp [e₀, MvPolynomial.coeff_X]

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

Goal state before:
pp: 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
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
⊢ ¬f = 1

Tactic:
rintro rfl

Goal state after:
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
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
y : B
hy : IsIntegral R y
h✝ : Nontrivial B
hf : Monic 1
hf' : ∀ (i : ℕ), IsIntegral R (coeff 1 i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {1}
⊢ False
Module: Mathlib.RingTheory.ZariskisMainTheorem

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
p : Ideal T
inst✝ : p.IsPrime
h₁ : ZariskisMainProperty R (Ideal.under S p)
h₂ : ∃ r ∉ Ideal.under S p, ⊥.saturation (Submonoid.powers ((algebraMap S T) r)) ⋯ = ⊤
⊢ ZariskisMainProperty R p

Tactic:
rw [zariskisMainProperty_iff] at h₁
  rw [zariskisMainProperty_iff']
  obtain ⟨s, hsp, hs, Hs⟩ := h₁
  obtain ⟨t, htp, Ht⟩ := h₂
  obtain ⟨m, hm⟩ := Hs t
  refine ⟨algebraMap _ _ (s ^ (m + 1) * t), ?_, fun x ↦ ?_⟩
  · simpa using ‹p.IsPrime›.mul_notMem
      (mt ((inferInstance : (p.under S).IsPrime).mem_of_pow_mem (m + 1)) hsp) htp
  obtain ⟨_, ⟨n, rfl⟩, a, ha⟩ := Ht.ge (Set.mem_univ x)
  obtain ⟨k, hk⟩ := Hs a
  refine ⟨k + n, ?_⟩
  convert_to IsIntegral R (algebraMap S T ((s ^ ((m + 1) * n) * (s ^ m * t) ^ k * (s ^ k * a))))
  · simp only [AlgHom.toRingHom_eq_coe, Algebra.toRingHom_ofId] at ha
    simp only [map_pow, map_mul, ha, pow_add, mul_pow]
    ring
  · exact .algebraMap (.mul ((hs.pow _).mul (hm.pow _)) hk)

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝² : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝¹ : Algebra (↥R₂) St := R₂.toAlgebra
this✝ : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h✝ : Nontrivial ↥R₁
⊢ Algebra.IsIntegral ↥R₁ ↥R₂

Tactic:
← le_integralClosure_iff_isIntegral,

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝² : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝¹ : Algebra (↥R₂) St := R₂.toAlgebra
this✝ : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h✝ : Nontrivial ↥R₁
⊢ R₂ ≤ integralClosure (↥R₁) St
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
Q : ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n) Q)) = ↑Q * X ^ m

Tactic:
by
  rw [← (basis ..).sum_repr Q]
  simp [-LinearMap.coe_inr, Finset.sum_mul, addLinearEquiv_symm_apply_inr_basis,
    smul_eq_C_mul, mul_assoc, ← pow_add, add_comm]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm PQ) =
    ↑((addLinearEquiv R m n).symm ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n) PQ.1 + (LinearMap.inr R (↥R[X]_m) ↥R[X]_n) PQ.2))

Tactic:
by
    rw [LinearMap.inl_apply, LinearMap.inr_apply, Prod.add_def, add_zero, zero_add]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
this : (algebraMap R S) (f.coeff n) + (algebraMap R S) (if n = m then a else 0) ∉ p
⊢ n ≠ f.natDegree

Tactic:
rintro rfl

Goal state after:
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
hfn : (algebraMap R S) (f.coeff f.natDegree) ∉ p
this : (algebraMap R S) (f.coeff f.natDegree) + (algebraMap R S) (if f.natDegree = m then a else 0) ∉ p
⊢ False
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝³ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝² : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝¹ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r))

Tactic:
exact isLocalization_basicOpen_of_qcqs (f.isCompact_preimage U.2.isCompact)
        (f.isQuasiSeparated_preimage U.2.isQuasiSeparated) (f.app _ r)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
g : R[X]
n : ℕ
r : R
hg✝ : g.natDegree ≤ n
a✝ : Nontrivial R
hg : g.natDegree = 0
⊢ (X - C r).resultant g 1 n = eval r g

Tactic:
obtain ⟨s, rfl⟩ := natDegree_eq_zero.mp hg
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
⊢ (normalizationObjIso f hU).hom ≫ CommRingCat.ofHom (integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)).val.toRingHom =
    appLE (toNormalization f) (fromNormalization f ⁻¹ᵁ U) (f ⁻¹ᵁ U) ⋯

Tactic:
rw [appLE, f.toNormalization_app_preimage ⟨U, hU⟩, Category.assoc]
  simp [← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ IsIso (Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom))

Tactic:
have : integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1) = ⊤ := by
    rw [integralClosure_eq_top_iff, ← algebraMap_isIntegral_iff, RingHom.algebraMap_toAlgebra]
    exact IsIntegralHom.isIntegral_app _ _ U.2

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
this✝ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this : integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) = ⊤
⊢ IsIso (Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom))
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R S
p : Ideal R
q : Ideal R'
inst✝² : p.IsPrime
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)
Q : ↑(q.primesOver (R' ⊗[R] S))
⊢ ↑((fiberIsoOfBijectiveResidueField H) Q) = comap Algebra.TensorProduct.includeRight ↑Q

Tactic:
simpa using! (Ideal.comap_fiberIsoOfBijectiveResidueField_symm H
    (Ideal.fiberIsoOfBijectiveResidueField H Q)).symm

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ f.resultant (derivative f) f.natDegree (f.natDegree - 1) =
    (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff * f.discr

Tactic:
rw [resultant_comm, resultant, ← sylvesterDeriv_updateRow f hf, Matrix.det_updateRow_smul,
    Matrix.updateRow_eq_self, discr, mul_comm f.natDegree]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : 0 < f.natDegree
⊢ (-1) ^ ((f.natDegree - 1) * f.natDegree) * (f.leadingCoeff * f.sylvesterDeriv.det) =
    (-1) ^ ((f.natDegree - 1) * f.natDegree / 2) * f.leadingCoeff *
      (f.sylvesterDeriv.det * (-1) ^ ((f.natDegree - 1) * f.natDegree / 2))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
⊢ f.natDegree - 1 + f.natDegree = 5

Tactic:
by rw [hf]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q✝ : Ideal S
inst✝² : q✝.IsPrime
inst✝¹ : q✝.LiesOver p
inst✝ : QuasiFiniteAt R q✝
s : S
hsq : s ∉ q✝
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q✝ → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q✝ → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
f : R[X] := X * minpoly R s
q : p.ResidueField[X]
hq' : ¬X - C 0 ∣ q
hqm : q.Monic
m' : ℕ := rootMultiplicity 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s))
hq : Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) = (X - C 0) ^ m' * q
⊢ ∃ m f b,
    f.Monic ∧
      b.Monic ∧
        IsCoprime (X ^ (m + 1)) b ∧ Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b ∧ (aeval s) f = 0

Tactic:
refine ⟨m', f, q, monic_X.mul (minpoly.monic hRs), hqm, ?_,
      by simp [f, hq, pow_succ', mul_assoc], by simp [f]⟩

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q✝ : Ideal S
inst✝² : q✝.IsPrime
inst✝¹ : q✝.LiesOver p
inst✝ : QuasiFiniteAt R q✝
s : S
hsq : s ∉ q✝
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q✝ → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q✝ → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
f : R[X] := X * minpoly R s
q : p.ResidueField[X]
hq' : ¬X - C 0 ∣ q
hqm : q.Monic
m' : ℕ := rootMultiplicity 0 (Polynomial.map (algebraMap R p.ResidueField) (minpoly R s))
hq : Polynomial.map (algebraMap R p.ResidueField) (minpoly R s) = (X - C 0) ^ m' * q
⊢ IsCoprime (X ^ (m' + 1)) q
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case h₁
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Bialgebra R T
⊢ (Over.Hom.left
          (η ≫
            Hom.asOver
              (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
              (Spec (of S))) ≫
        (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Over.Hom.left η ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
· simp [Scheme.monObjAsOverPullback_one, ε_algSpec_left (R := CommRingCat.of _),
        pullbackSpecIso', specOverSpec_over, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
        AlgHom.toUnder, Under.homMk_right,
        ← AlgHom.coe_restrictScalars R (Bialgebra.counitAlgHom S _), -AlgHom.coe_restrictScalars,
        ← AlgHom.comp_toRingHom, Bialgebra.counitAlgHom_comp_includeRight]
      simp [AlgHom.comp_toRingHom, Algebra.toRingHom_ofId]

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ ↑U := lift U.ι f ⋯
heq : f = f' ≫ U.ι
⊢ IsOpenImmersion f

Tactic:
have hflat : Flat f' :=
      of_postcomp (W := @Flat) f' U.ι hU (by rwa [← heq])

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ ↑U := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
⊢ IsOpenImmersion f
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Finite σ
⊢ ringKrullDim R + ↑↑(Nat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
push_cast

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Finite σ
⊢ ringKrullDim R + ↑(Nat.card σ) ≤ ringKrullDim (MvPolynomial σ R)
Module: Mathlib.RingTheory.GradedAlgebra.RingHom

Goal state before:
pp: ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
σ : Type u_6
τ : Type u_7
ψ : Type u_8
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Semiring C
inst✝² : SetLike σ A
inst✝¹ : SetLike τ B
inst✝ : SetLike ψ C
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
g : ℬ →+*ᵍ 𝒞
f₁ f₂ : 𝒜 →+*ᵍ ℬ
hg : Function.Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : A
⊢ (g.comp f₂) x = g (f₂ x)

Tactic:
comp_apply

Goal state after:
ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
σ : Type u_6
τ : Type u_7
ψ : Type u_8
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Semiring C
inst✝² : SetLike σ A
inst✝¹ : SetLike τ B
inst✝ : SetLike ψ C
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
g : ℬ →+*ᵍ 𝒞
f₁ f₂ : 𝒜 →+*ᵍ ℬ
hg : Function.Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : A
⊢ g (f₂ x) = g (f₂ x)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    (fun x ↦ a (ia x)) x =
      HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
wb :
  ∀ (x : ↥Vb),
    (fun x ↦ b (ib x)) x =
      HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (a + b) (i x)

Tactic:
refine
    ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ja + jb,
      ⟨sb * ra + sa * rb,
        add_mem (add_comm jb ja ▸ mul_mem_graded sb_mem ra_mem : sb * ra ∈ 𝒜 (ja + jb))
          (mul_mem_graded sa_mem rb_mem)⟩,
      ⟨sa * sb, mul_mem_graded sa_mem sb_mem⟩, fun y ↦
        y.1.asHomogeneousIdeal.toIdeal.primeCompl.mul_mem (hwa ⟨y.1, y.2.1⟩) (hwb ⟨y.1, y.2.2⟩), ?_⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
wa :
  ∀ (x : ↥Va),
    (fun x ↦ a (ia x)) x =
      HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
wb :
  ∀ (x : ↥Vb),
    (fun x ↦ b (ib x)) x =
      HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
⊢ ∀ (x : ↥(Va ⊓ Vb)),
    (fun x ↦ (a + b) ((Va.infLELeft Vb ≫ ia) x)) x =
      HomogeneousLocalization.mk { deg := ja + jb, num := ⟨sb * ra + sa * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
e :
  NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl f =
    NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl g
⊢ (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑f.den) x ⋯))
      (sectionInBasicOpen 𝒜 x f) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 ↑g.den) x ⋯))
      (sectionInBasicOpen 𝒜 x g)

Tactic:
simp only [HomogeneousLocalization.NumDenSameDeg.embedding, Localization.mk_eq_mk',
      IsLocalization.mk'_eq_iff_eq,
      IsLocalization.eq_iff_exists x.asHomogeneousIdeal.toIdeal.primeCompl] at e
    obtain ⟨⟨c, hc⟩, hc'⟩ := e
    apply (Proj.structureSheaf 𝒜).presheaf.germ_ext
      (ProjectiveSpectrum.basicOpen 𝒜 f.den.1 ⊓
        ProjectiveSpectrum.basicOpen 𝒜 g.den.1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 c)
      ⟨⟨mem_basicOpen_den _ x f, mem_basicOpen_den _ x g⟩, hc⟩
      (homOfLE inf_le_left ≫ homOfLE inf_le_left) (homOfLE inf_le_left ≫ homOfLE inf_le_right)
    apply Subtype.ext
    ext ⟨t, ⟨htf, htg⟩, ht'⟩
    rw [Proj.res_apply, Proj.res_apply]
    simp only [sectionInBasicOpen, HomogeneousLocalization.val_mk, Localization.mk_eq_mk',
      IsLocalization.mk'_eq_iff_eq]
    apply (IsLocalization.map_units (M := t.asHomogeneousIdeal.toIdeal.primeCompl)
      (Localization t.asHomogeneousIdeal.toIdeal.primeCompl) ⟨c, ht'⟩).mul_left_cancel
    rw [← map_mul, ← map_mul, hc']

Goal state after: