mathlib-initiative/mathlib-tactics huggingface dataset:
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 (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * C a.leadingCoeff⁻¹⁻¹ * (p / gcd p q) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (p / gcd p q) ∧
    C (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * (C a.leadingCoeff⁻¹⁻¹ * (q / gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (q / gcd p q)

Tactic:
← Polynomial.C_mul,

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.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * a.leadingCoeff⁻¹⁻¹) * (p / gcd p q) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (p / gcd p q) ∧
    C (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * (C a.leadingCoeff⁻¹⁻¹ * (q / gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (q / gcd p q)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
obtain ⟨ε, hεI, b, hb⟩ : ∃ ε ∈ I, ∃ b, aeval x (derivative P.f) * b = 1 + ε := by
    refine ⟨_, ?_, (a ^ n * aeval x p₁), sub_eq_iff_eq_add'.mp rfl⟩
    convert_to (aeval x P.g * a) ^ n - 1 - aeval x P.f * (a ^ n * aeval x p₂) ∈ I
    · linear_combination a ^ n * e
    · exact sub_mem (Ideal.mem_of_dvd _ (sub_one_dvd_pow_sub_one _ _) ha) (I.mul_mem_right _ hf)

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * (aeval P.x) P.g ^ n = (aeval P.x) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 := Localization.Away ((AdjoinRoot.mk P.f) P.g)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this✝ :
  IsLocalization.Away ((AdjoinRoot.mk P.f) (p * P.g))
    (Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)))
this : ((↑e.symm).comp (IsScalarTower.toAlgHom R (AdjoinRoot P.f) S')).comp (AdjoinRoot.mkₐ P.f) = aeval P.x
⊢ Submonoid.map e.symm.toRingEquiv.toMonoidHom
      (Submonoid.powers ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p))) =
    Submonoid.powers ((aeval P.x) p)

Tactic:
rw [Submonoid.map_powers]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsStandardEtale R S
Sₛ : Type u_4
inst✝⁴ : CommRing Sₛ
inst✝³ : Algebra S Sₛ
inst✝² : Algebra R Sₛ
inst✝¹ : IsScalarTower R S Sₛ
s : S
inst✝ : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * (aeval P.x) P.g ^ n = (aeval P.x) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 := Localization.Away ((AdjoinRoot.mk P.f) P.g)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this✝ :
  IsLocalization.Away ((AdjoinRoot.mk P.f) (p * P.g))
    (Localization.Away ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p)))
this : ((↑e.symm).comp (IsScalarTower.toAlgHom R (AdjoinRoot P.f) S')).comp (AdjoinRoot.mkₐ P.f) = aeval P.x
⊢ Submonoid.powers (e.symm.toRingEquiv.toMonoidHom ((algebraMap (AdjoinRoot P.f) S') ((AdjoinRoot.mk P.f) p))) =
    Submonoid.powers ((aeval P.x) p)
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case refine_2
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}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
a : S'
ham : a ∈ m
⊢ 0 ∈ Multiset.map (eval a) (Multiset.map (fun x ↦ X - C x) m)

Tactic:
simpa using ⟨a, ham, by simp⟩

Goal state after:
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
inst✝ : Algebra.IsIntegral R S
p : Ideal T
H : ZariskisMainProperty S p
⊢ ZariskisMainProperty R p

Tactic:
rw [zariskisMainProperty_iff'] at H ⊢
  obtain ⟨r, hrp, H⟩ := H
  exact ⟨r, hrp, fun x ↦ ⟨_, isIntegral_trans _ (H x).choose_spec⟩⟩

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}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
a : S'
ham : a ∈ m
⊢ (Multiset.map (fun x ↦ X - C x) (m.erase a)).prod * (X - C a) ∣
    (Multiset.map (fun x ↦ X - C x) (m.erase a)).prod * (Polynomial.map (algebraMap S S') y - C ((aeval a) y))

Tactic:
refine mul_dvd_mul_left _ ?_

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 ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
a : S'
ham : a ∈ m
⊢ X - C a ∣ Polynomial.map (algebraMap S S') y - C ((aeval a) y)
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}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
a : S'
ham : a ∈ m
⊢ 0 ∈ Multiset.map (fun x ↦ a - x) m

Tactic:
simpa using ⟨a, ham, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case neg
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
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn : (φ p * t) ^ n ∈ conductor R (φ X)
k : ℕ
hk : (p ^ n).leadingCoeff ^ k • t ^ n ∈ conductor R (φ X)
hpn : ¬p.leadingCoeff ^ n = 0
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
leadingCoeff_pow' hpn,

Goal state after:
case neg
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
p : R[X]
i : ℕ
hi : i = p.natDegree
n : ℕ
hn : (φ p * t) ^ n ∈ conductor R (φ X)
k : ℕ
hk : (p.leadingCoeff ^ n) ^ k • t ^ n ∈ conductor R (φ X)
hpn : ¬p.leadingCoeff ^ n = 0
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
⊢ ∀ (a : Fin n), (LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n)) (↑(taylorLinearEquiv r n)) a a = 1

Tactic:
intro i
    rw [LinearMap.toMatrix_apply, degreeLT.basis_repr, ← natDegree_X_pow (R := R) (i : ℕ)]
    change (taylor r (degreeLT.basis R n i)).coeff _ = 1
    rw [degreeLT.basis_val, coeff_taylor_natDegree, leadingCoeff_X_pow]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
i j : Fin n
hji : id j < id i
⊢ ((degreeLT.basis R n).repr (↑(taylorLinearEquiv r n) ((degreeLT.basis R n) j))) i = 0

Tactic:
LinearEquiv.coe_coe,

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
i j : Fin n
hji : id j < id i
⊢ ((degreeLT.basis R n).repr ((taylorLinearEquiv r n) ((degreeLT.basis R n) j))) i = 0
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
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
f : S →ₐ[R] ↥S' := (IsScalarTower.toAlgHom R S L).codRestrict (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
⊢ Function.Surjective ⇑g

Tactic:
rw [← AlgHom.range_eq_top,
      ← (Subalgebra.map_injective (f := S'.val) Subtype.val_injective).eq_iff, Algebra.map_top]

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
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this✝ : IsDomain R
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
R' : Subalgebra R K := integralClosure R K
S' : Subalgebra (↥R') L := adjoin ↥R' ↑(algebraMap S L).range
f : S →ₐ[R] ↥S' := (IsScalarTower.toAlgHom R S L).codRestrict (Subalgebra.restrictScalars R S') ⋯
g : ↥R' ⊗[R] S →ₐ[↥R'] ↥S' := TensorProduct.lift (ofId ↥R' ↥S') f ⋯
⊢ Subalgebra.map S'.val g.range = S'.val.range
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
hx : x ∈ integralClosure ↑Γ(Y, Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V))
i : Opposite.op V ⟶ Opposite.op U
algInst✝⁴ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝³ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ V) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst✝² : Algebra ↑Γ(Y, V) ↑Γ(Y, U) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst✝¹ : Algebra ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) ↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
⊢ algebraMap ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ U) = (algebraMap ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U)).comp (algebraMap ↑Γ(Y, V) ↑Γ(Y, U))

Tactic:
by
        simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp]; rfl

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : j = 2 * f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree * ↑f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
      (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + ↑1)

Tactic:
← Nat.cast_add

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : j = 2 * f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree * ↑f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) * ↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
⊢ f.resultant (g + f * p) m n = f.resultant g m n

Tactic:
have H : p.support ⊆ Finset.range (n - m + 1) := by
    simp only [Finset.subset_iff, Finset.mem_range]
    exact fun x hx ↦ (le_natDegree_of_mem_supp _ hx).trans_lt (by lia)
  rw [← p.sum_monomial_eq, Polynomial.sum_eq_of_subset _ (by simp) H]
  set k := n - m + 1
  replace H := show k ≤ n - m + 1 from le_rfl
  clear_value k
  induction k generalizing g with
  | zero =>
    simp only [Finset.range_zero, Finset.sum_empty]
    rw [mul_zero, add_zero]
  | succ k IH =>
    rw [Finset.sum_range_succ, mul_add, ← add_assoc, resultant_add_mul_monomial_right, IH] <;> lia

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
hf : f.natDegree < m
hg : g.natDegree < n
⊢ f.resultant g m n = 0

Tactic:
obtain _ | m := m; · lia
  obtain _ | n := n; · lia
  rw [resultant_add_left_deg _ _ _ _ _ (by lia), resultant_add_right_deg _ _ _ _ _ (by lia)]
  simp [coeff_eq_zero_of_natDegree_lt hg]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ IsDominant (toNormalization f)

Tactic:
have := congr(($(f.ker_toNormalization).support : Set f.normalization))

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
this : ↑(ker (toNormalization f)).support = ↑⊥.support
⊢ IsDominant (toNormalization f)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegral X
⊢ ⊤ = closure (⇑(toNormalization f) '' Set.univ)

Tactic:
simpa using f.toNormalization.denseRange.closure_range.symm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : Nontrivial R
⊢ (freeMonic R n).coeff n ≠ 0

Tactic:
simp [coeff_freeMonic]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin n) R →ₐ[R] S
i : Fin n
⊢ ((fun p ↦ aeval fun x ↦ (↑p).coeff ↑x) ((fun f ↦ (MonicDegreeEq.freeMonic R n).map f.toRingHom) f)) (X i) = f (X i)

Tactic:
simp [coeff_freeMonic]

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn✝ hn : n = m + k
a✝¹ : Nontrivial R
a✝ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
      ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
          Algebra.TensorProduct.includeRight)).Monic

Tactic:
exact ((monic_freeMonic R m).map _).mul ((monic_freeMonic R _).map _)

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

Goal state before:
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
hfm : f.Monic
hg0 : ¬g = 0
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.Monic → ¬g = 0 → g.Monic → f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
hgm : ¬g.Monic
inst : Field R := hR.toField
⊢ (C g.leadingCoeff⁻¹ * g).Monic

Tactic:
rw [Monic, ← coeff_natDegree, natDegree_C_mul (by simp [hg0]), coeff_C_mul]; simp [hg0]

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

Goal state before:
pp: case inr.e_a.e_5
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ m = (freeMonic R m).natDegree

Tactic:
natDegree_freeMonic

Goal state after:
case inr.e_a.e_5
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ m = m
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.e_a.e_6
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ k = (freeMonic R k).natDegree

Tactic:
natDegree_freeMonic

Goal state after:
case inr.e_a.e_6
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ k = k
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (-1) ^ n *
      (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeLeftRingHom) (freeMonic R m)).resultant
        (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeRight.toRingHom) (freeMonic R k)) m
        (freeMonic R k).natDegree =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant (↑(factor₂ m k hn p)) m k

Tactic:
natDegree_freeMonic

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (-1) ^ n *
      (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeLeftRingHom) (freeMonic R m)).resultant
        (map ((↑(fromTensor m k hn p)).comp Algebra.TensorProduct.includeRight.toRingHom) (freeMonic R k)) m k =
    (-1) ^ n * (↑(factor₁ m k hn p)).resultant (↑(factor₂ m k hn p)) m k
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, ⋯⟩
⊢ ∃ p q, p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = C (f.resultant g m n)

Tactic:
have : ((sylvesterMap f g hf hg X)).1 = _ :=
    congr(($(sylveserMap_comp_adjSylvester f g hf hg) _).1)

Goal state after:
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, ⋯⟩)
⊢ ∃ p q, p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = C (f.resultant g m n)