mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i✝ : ℕ
hi✝ : i✝ ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
hi : p.natDegree < i
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (X ^ p.natDegree).coeff i

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hi, hi.ne']

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

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
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
g : R[X] := minpoly R a
H : ∀ (i : ℕ), i ≠ g.natDegree → g.coeff i ∈ p
i : ℕ
hi : g.natDegree < i
⊢ (map (Ideal.Quotient.mk p) g).coeff i = (X ^ g.natDegree).coeff i

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hi, hi.ne']

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

Goal state before:
pp: case smul
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
a x : S
hx✝ : x ∈ Submodule.span S (⇑(algebraMap R S) '' ↑I)
hx : IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C x * X)
⊢ IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C a)

Tactic:
exact ((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ (idealX K).intValuation X = exp (-1)

Tactic:
intValuation_singleton
      _ (Polynomial.X_ne_zero) (idealX_span K)

Goal state after:
K : Type u_1
inst✝ : Field K
⊢ exp (-1) = exp (-1)
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
⊢ c • RatFunc.mk p q =
    { toFun := fun x ↦ RatFunc.mk ((algebraMap R K[X]) x) 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        c *
      RatFunc.mk p q

Tactic:
rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, mk_one', ← mk_smul,
      mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← ofFractionRing_mul,
      IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]

Goal state after:
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
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (p / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∧
    C (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))).leadingCoeff⁻¹ * (a * q / (a * (C a.leadingCoeff⁻¹ * gcd p q))) =
      C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)

Tactic:
EuclideanDomain.mul_div_mul_cancel ha hdivq,

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
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C (q / (C a.leadingCoeff⁻¹ * gcd p q)).leadingCoeff⁻¹ * (p / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∧
    C (q / (C a.leadingCoeff⁻¹ * gcd p q)).leadingCoeff⁻¹ * (q / (C a.leadingCoeff⁻¹ * gcd p q)) =
      C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
this : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) (CAlgHom P.g * Y) -
      (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) 1 =
    0

Tactic:
← map_sub,

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
this : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) (CAlgHom P.g * Y - 1) = 0
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤

Tactic:
have : p.IsPrime := Ideal.IsPrime.under R Q

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this : p.IsPrime
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case mem
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[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x✝ x : S
h : x ∈ ↑s
⊢ p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range

Tactic:
← Nat.sub_add_cancel (s.le_sup h),

Goal state after:
case mem
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[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x✝ x : S
h : x ∈ ↑s
⊢ p.leadingCoeff ^ (s.sup n - n x + n x) • (t * x) ∈ φ.range
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
this✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q'
ht : (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤
p : Ideal R := Ideal.under R Q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
Q' : Ideal S
e : Q' ∈ {Q}
⊢ Q' ∈ (Ideal.under (↥R[t]) Q).primesOver S

Tactic:
exact ⟨e ▸ inferInstance, ⟨e ▸ rfl⟩⟩

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝² : P.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsReduced S]
    {x : S},
    (aeval x).Finite →
      ∀ (P : Ideal S) [inst_4 : P.IsPrime] [WeaklyQuasiFiniteAt R P],
        IsDomain S ∧ FaithfulSMul R S → ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : p ∈ ⊥.minimalPrimes
hpP : p ≤ P
inst✝ : p.IsPrime
inst : (Ideal.map (Ideal.Quotient.mk p) P).IsPrime
⊢ WeaklyQuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk p) P)

Tactic:
refine .of_surjectiveOnStalks P _ (Ideal.Quotient.mkₐ _ _)
        (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective) ?_

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝² : P.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R P
this :
  ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsReduced S]
    {x : S},
    (aeval x).Finite →
      ∀ (P : Ideal S) [inst_4 : P.IsPrime] [WeaklyQuasiFiniteAt R P],
        IsDomain S ∧ FaithfulSMul R S → ¬IsStronglyTranscendental R x
hS : ¬(IsDomain S ∧ FaithfulSMul R S)
hx : IsStronglyTranscendental R x
p : Ideal S
hp : p ∈ ⊥.minimalPrimes
hpP : p ≤ P
inst✝ : p.IsPrime
inst : (Ideal.map (Ideal.Quotient.mk p) P).IsPrime
⊢ P = Ideal.comap (Ideal.Quotient.mkₐ R p) (Ideal.map (Ideal.Quotient.mk p) P)
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin n
⊢ Sum.elim (⇑(LinearMap.inl R (↥R[X]_m) ↥R[X]_n) ∘ ⇑(basis R m)) (⇑(LinearMap.inr R (↥R[X]_m) ↥R[X]_n) ∘ ⇑(basis R n))
      (Sum.inr i) =
    (0, (basis R n) i)

Tactic:
Sum.elim_inr,

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
i : Fin n
⊢ (⇑(LinearMap.inr R (↥R[X]_m) ↥R[X]_n) ∘ ⇑(basis R n)) i = (0, (basis R n) i)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
x : ↑Γ(T, f₂ ⁻¹ᵁ ↑U)
algInst✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
algInst✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(T, f₂ ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f₂ ↑U)).toAlgebra
algInst✝ : Algebra ↑Γ(T, f₂ ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) :=
  (CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ?m.135)).toAlgebra
⊢ (CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) ⋯)) x ∈
    integralClosure ↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U)))
      ↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U)))

Tactic:
have : IsScalarTower Γ(Y, U.1) Γ(T, f₂ ⁻¹ᵁ U.1) Γ(X, f ⁻¹ᵁ U.1) := .of_algebraMap_eq' <| by
      simp only [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
        Hom.app_eq_appLE, Hom.appLE_comp_appLE, ← H]

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
x : ↑Γ(T, f₂ ⁻¹ᵁ ↑U)
algInst✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
algInst✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(T, f₂ ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f₂ ↑U)).toAlgebra
algInst✝ : Algebra ↑Γ(T, f₂ ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) :=
  (CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ⋯)).toAlgebra
this : IsScalarTower ↑Γ(Y, ↑U) ↑Γ(T, f₂ ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)
⊢ (CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U))) ⋯)) x ∈
    integralClosure ↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U)))
      ↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op U)))
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
⊢ f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U

Tactic:
simp only [← Scheme.Hom.comp_preimage, hf₂, toNormalization_fromNormalization]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
this :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R → f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
hR : ¬IsField R
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
· let K := FractionRing R
    apply FaithfulSMul.algebraMap_injective R K
    have := this (f.map (algebraMap R K)) (g.map (algebraMap R K)) n (natDegree_map_le.trans hg)
      (hf.map _) (Field.toIsField _)
    simp only [resultant_map_map, natDegree_map_eq_of_injective, leadingCoeff_map_of_injective,
      FaithfulSMul.algebraMap_injective R K, ← hf.natDegree_eq_card_roots,
      ← roots_map_of_injective_of_card_eq_natDegree] at this
    simpa [map_multiset_prod, aeval_algebraMap_apply, Multiset.map_map] using this

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
H : m ≠ 0 ∨ n ≠ 0
a✝ : Nontrivial R
X : ↥R[X]_m × ↥R[X]_n := (f.adjSylvester g) ⟨1, ⋯⟩
this : ↑((f.sylvesterMap g hf hg) X) = ↑((f.resultant g m n • LinearMap.id) ⟨1, ⋯⟩)
⊢ (↑X.2).degree < ↑n

Tactic:
by simpa [-SetLike.coe_mem] using X.2.2

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x✝ : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x✝ ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x✝ ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := ⋯
this✝² : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
this✝¹ : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst✝² : Algebra ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U) := ⋯
algInst✝¹ : Algebra ↑Γ(S, U) ↑Γ(Y, V) := ⋯
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) := ⋯
algebraizeInst✝ : Algebra.Smooth ↑Γ(S, U) ↑Γ(Y, V)
this✝ : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
e₀ : CommRingCat.of
    (↑(Y.presheaf.1 (Opposite.op V)) ⊗[↑(S.presheaf.1 (Opposite.op U))] ↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U)))) ≅
  Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) := ⋯
e : ↑Γ(Y, V) ⊗[↑Γ(S, U)] ↑Γ(X, f ⁻¹ᵁ U) ≃ₐ[↑Γ(Y, V)] ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) := ⋯
ψ : ↑Γ(Y, V) ⊗[↑Γ(S, U)] ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)) →ₐ[↑Γ(Y, V)]
  ↥(integralClosure ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) := ⋯
hψ : Function.Bijective ⇑ψ
φ : pushout (app (fromNormalization f) U) (appLE g U V hVU) ⟶
  Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W) := ⋯
this : Mono (CommRingCat.ofHom (integralClosure ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)).val.toRingHom)
H : pullback.snd f g ⁻¹ᵁ V ≤ pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U
x : ↑(CommRingCat.of ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)))
⊢ (ConcreteCategory.hom (appLE (pullback.fst f g) (f ⁻¹ᵁ U) (pullback.snd f g ⁻¹ᵁ V) H)) ↑x =
    (ConcreteCategory.hom (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ e₀.hom)) ↑x

Tactic:
congr 2; simp [e₀, pushout.inl_desc_assoc]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M := ⋯
⊢ Function.Surjective ⇑f₀

Tactic:
have : Function.Surjective (AlgebraTensorModule.lTensor T T f₀) := by
    rw [← LinearMap.range_eq_top, eq_top_iff, ← hs, Submodule.span_le, Set.range_subset_iff]
    intro i
    use ∑ (j : Fin (k i)), t i j ⊗ₜ Pi.basisFun R _ ⟨i, j⟩
    simp [f₀, -Pi.basisFun_equivFun, -Pi.basisFun_apply, h i]

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FaithfullyFlat R T
inst✝ : Module.Finite T (T ⊗[R] M)
n : ℕ
s : Fin n → T ⊗[R] M
hs : Submodule.span T (Set.range s) = ⊤
k : Fin n → ℕ
t : (i : Fin n) → Fin (k i) → T
m : (i : Fin n) → Fin (k i) → M
h : ∀ (i : Fin n), s i = ∑ j, t i j ⊗ₜ[R] m i j
f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
  ((Pi.basisFun R ((i : Fin n) × Fin (k i))).constr R) fun x ↦
    match x with
    | ⟨i, j⟩ => m i j
this : Function.Surjective ⇑((AlgebraTensorModule.lTensor T T) f₀)
⊢ Function.Surjective ⇑f₀
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
x : ↥Y
⊢ _root_.IsDiscrete (⇑f ⁻¹' {x})

Tactic:
isDiscrete_iff_discreteTopology,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : quasiFiniteLocus f = ⊤
x : ↥Y
⊢ DiscreteTopology ↑(⇑f ⁻¹' {x})
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
⊢ ¬↑(Scheme.Hom.smoothLocus f) ≠ Set.univ

Tactic:
← Set.nonempty_compl

Goal state after:
K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
⊢ ¬(↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = η_f

Tactic:
rw [← ih_η, ← ih_θ]
  apply Iso.ext (by simp)

Goal state after:
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
          ((Hom.asOver
                (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom
                (Spec (of S)) ⊗ₘ
              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))

Tactic:
convert! congr($(μ_pullback_left_fst R S T) ≫ (pullbackSpecIso R T T).hom ≫
        Spec.map (CommRingCat.ofHom (Bialgebra.comulAlgHom R T).toRingHom)) using 1
      · simp [Scheme.monObjAsOverPullback_mul, pullbackSpecIso', specOverSpec_over,
          OverClass.asOver, Hom.asOver, OverClass.asOverHom, mul_spec_asOver_spec_left]
      · simp [pullbackSpecIso', specOverSpec_over, OverClass.asOver, Hom.asOver, ← Spec.map_comp,
          OverClass.asOverHom, mul_spec_asOver_spec_left, ← CommRingCat.ofHom_comp,
          ← Bialgebra.comul_includeRight]

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

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✝² : Flat R S
inst✝¹ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst✝ : p.IsMaximal
hr : ¬rankAtStalk S { asIdeal := p, isPrime := ⋯ } = 0
⊢ Function.Surjective ⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S))

Tactic:
refine (Free.bijective_algebraMap_of_finrank_eq_one ?_).2

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Flat R S
inst✝¹ : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst✝ : p.IsMaximal
hr : ¬rankAtStalk S { asIdeal := p, isPrime := ⋯ } = 0
⊢ finrank (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S) = 1
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝¹ : Flat f
inst✝ : IsFinite f
y : ↥Y
⊢ finrank (pullback.snd f g) y = finrank f (g y)

Tactic:
finrank_pullback_snd

Goal state after:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝¹ : Flat f
inst✝ : IsFinite f
y : ↥Y
⊢ finrank f (g y) = finrank f (g y)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case refine_1.inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], 1 ≤ finrank f → (∃ R, Y = Spec R) → Surjective f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ 1 y ≤ finrank (pullback.snd f (Y.affineCover.f i)) y

Tactic:
finrank_pullback_snd

Goal state after:
case refine_1.inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], 1 ≤ finrank f → (∃ R, Y = Spec R) → Surjective f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ 1 y ≤ finrank f ((Y.affineCover.f i) y)