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

Goal state before:
pp: case H.H.refine_3
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
h : φ y✝.1 / φ ↑y✝.2 = φ a'.1 / φ ↑a'.2
this : ↑a'.2 * y✝.1 = a'.1 * ↑y✝.2
⊢ ↑(a'.1, a'.2).2 * (y✝.1, y✝.2).1 = ↑(y✝.1, y✝.2).2 * (a'.1, a'.2).1

Tactic:
mul_comm a'.fst

Goal state after:
case H.H.refine_3
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
h : φ y✝.1 / φ ↑y✝.2 = φ a'.1 / φ ↑a'.2
this : ↑a'.2 * y✝.1 = ↑y✝.2 * a'.1
⊢ ↑(a'.1, a'.2).2 * (y✝.1, y✝.2).1 = ↑(y✝.1, y✝.2).2 * (a'.1, a'.2).1
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) x } = (algebraMap K[X] K⟮X⟯) x

Tactic:
← mk_one,

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) x } = RatFunc.mk x 1
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_2
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 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ IsUnit ((aeval (x + (aeval x) P.f * -b)) P.g)

Tactic:
rw [← IsNilpotent.isUnit_quotient_mk_iff (I := I) ⟨2, hI⟩, ← Ideal.Quotient.mkₐ_eq_mk R,
      ← aeval_algHom_apply, Ideal.Quotient.mkₐ_eq_mk, map_add,
      Ideal.Quotient.eq_zero_iff_mem.mpr (I.mul_mem_right _ hf), add_zero]

Goal state after:
case refine_2
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 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ IsUnit ((aeval ((Ideal.Quotient.mk I) x)) P.g)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ x.num ∣ p ↔ ∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

Tactic:
by
  constructor
  · rintro ⟨q, rfl⟩
    obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp
    use denom x * q
    rw [map_mul, map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]
    · exact ⟨mul_ne_zero (denom_ne_zero x) hq, rfl⟩
    · exact algebraMap_ne_zero hq
  · rintro ⟨q, hq, rfl⟩
    exact num_div_dvd p hq

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

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
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
algInst✝ : Algebra R (P.map (algebraMap R T)).Ring :=
  ((algebraMap T (P.map (algebraMap R T)).Ring).comp (algebraMap R T)).toAlgebra
scalarTowerInst✝ : IsScalarTower R T (P.map (algebraMap R T)).Ring :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R (P.map (algebraMap R T)).Ring))
H : P.HasMap (P.map (algebraMap R T)).X
f : T ⊗[R] S →ₐ[T] (P.map (algebraMap R T)).Ring :=
  Algebra.TensorProduct.lift (Algebra.ofId T (P.map (algebraMap R T)).Ring)
    ((P.lift (P.map (algebraMap R T)).X H).comp ↑P.equivRing) ⋯
α : T ⊗[R] S ≃ₐ[T] (P.map (algebraMap R T)).Ring :=
  AlgEquiv.ofAlgHom f ((P.map (algebraMap R T)).lift (1 ⊗ₜ[R] P.x) ⋯) ⋯ ⋯
⊢ Function.Bijective ⇑((P.map (algebraMap R T)).lift (1 ⊗ₜ[R] P.x) ⋯)

Tactic:
exact α.symm.bijective

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

Goal state before:
pp: case hb
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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
x : ↥(integralClosure R B)
⊢ 1 ⊗ₜ[R] ↑x =
    ↑((IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) (S ⊗[R] ↥(integralClosure R B))
          ↥(integralClosure S (S ⊗[R] B)))
        (1 ⊗ₜ[R] x))

Tactic:
simp [← Algebra.TensorProduct.right_algebraMap_apply]

Goal state after:
case hb
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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
x : ↥(integralClosure R B)
⊢ (algebraMap B (S ⊗[R] B)) ↑x = ↑((algebraMap ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))) x)
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
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := leftModule
this✝³ : SMul p.ResidueField (p.Fiber S) := this✝⁴.toSMul
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
this : Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯ = AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField)
⊢ (AlgHom.restrictScalars R φ) r ≠ 0

Tactic:
Algebra.TensorProduct.restrictScalars_lift

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
this✝⁴ : Module p.ResidueField (p.Fiber S) := leftModule
this✝³ : SMul p.ResidueField (p.Fiber S) := this✝⁴.toSMul
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
this : Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯ = AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField)
⊢ (TensorProduct.lift (AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField))
        (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯)
      r ≠
    0
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.leadingCoeff ^ (n * k) • t ^ n ∈ conductor R (φ X)
hpn : ¬p.leadingCoeff ^ n = 0
⊢ (p.coeff i ^ (n * k) * p.coeff i ^ n) • (t ^ n * t ^ (n * k)) ∈ conductor R (φ X)

Tactic:
mul_smul_mul_comm,

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 ^ (n * k) • t ^ n * p.coeff i ^ n • t ^ (n * k) ∈ conductor R (φ X)
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 ((PQ.1, 0).1 + (0, PQ.2).1, (PQ.1, 0).2 + (0, PQ.2).2))

Tactic:
add_zero,

Goal state after:
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 ((PQ.1, 0).1, (PQ.1, 0).2 + (0, PQ.2).2))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (if m ≤ m + 1 + n ∧ m + 1 + n ≤ m + (n + 1) then g.coeff (m + 1 + n - m) else 0) = g.coeff (n + 1)

Tactic:
if_pos (by lia)

Goal state after:
case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ g.coeff (m + 1 + n - m) = g.coeff (n + 1)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
    f.Monic →
      g.Monic →
        f.Splits →
          g.Splits →
            g.natDegree ≤ f.natDegree → f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
hfg : ¬g.natDegree ≤ f.natDegree
⊢ (-1) ^ (f.natDegree * g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) (Multiset.map Prod.swap (f.roots ×ˢ g.roots))).prod =
    (Multiset.map (fun ij ↦ -1 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots)).prod

Tactic:
Multiset.map_map,

Goal state after:
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
this :
  ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
    f.Monic →
      g.Monic →
        f.Splits →
          g.Splits →
            g.natDegree ≤ f.natDegree → f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
hfg : ¬g.natDegree ≤ f.natDegree
⊢ (-1) ^ (f.natDegree * g.natDegree) * (Multiset.map ((fun ij ↦ ij.1 - ij.2) ∘ Prod.swap) (f.roots ×ˢ g.roots)).prod =
    (Multiset.map (fun ij ↦ -1 * (ij.2 - ij.1)) (f.roots ×ˢ g.roots)).prod
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
n k : ℕ
h : ¬k < n
⊢ (if k = n then 1 else 0) + 0 = if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0

Tactic:
add_zero,

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
n k : ℕ
h : ¬k < n
⊢ (if k = n then 1 else 0) = if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
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
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots)).prod
⊢ (algebraMap R L) (f.resultant g f.natDegree n) = (algebraMap R L) (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
← resultant_map_map,

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
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots)).prod
⊢ (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree n =
    (algebraMap R L) (Multiset.map (fun x ↦ eval x g) f.roots).prod
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
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots)).prod
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots)).prod =
    (algebraMap R L) (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
map_sub_sprod_roots_eq_prod_map_eval _ _ (hgm.map _) (SplittingField.splits _),

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
hfm : f.Monic
hg0 : ¬g = 0
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots)).prod
⊢ (Multiset.map (fun x ↦ eval x (map (algebraMap R g.SplittingField) g)) (map (algebraMap R L) f).roots).prod =
    (algebraMap R L) (Multiset.map (fun x ↦ eval x g) f.roots).prod
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)

Tactic:
obtain ⟨p, hp, hp'⟩ : (universalFactorizationMap ℤ n m k hn).IsIntegralElem (.X i ⊗ₜ 1) := by
      simpa [coeff_freeMonic] using! Polynomial.isIntegral_coeff_of_dvd _ _ (monic_freeMonic _ _)
        ((monic_freeMonic _ _).map _) ⟨_, universalFactorizationMap_freeMonic ℤ n m k hn⟩ i

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
i : Fin m
p : (MvPolynomial (Fin n) ℤ)[X]
hp : p.Monic
hp' : Polynomial.eval₂ (universalFactorizationMap ℤ n m k hn).toRingHom (X i ⊗ₜ[ℤ] 1) p = 0
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (a * f + b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree

Tactic:
e,

Goal state after:
case inr.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant 1 f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
⊢ (map φ f').coeff f'.natDegree = φ (f'.coeff f'.natDegree)

Tactic:
coeff_map

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

Goal state before:
pp: R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = φ f'.leadingCoeff
⊢ (map φ g').coeff g'.natDegree = φ (g'.coeff g'.natDegree)

Tactic:
coeff_map

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf' =>
    by_cases hf0 : f.natDegree = 0
    · obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hf0; simp
    by_cases hg0 : g.natDegree = 0
    · obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hg0; simp
    obtain rfl | hr := eq_or_ne r 0
    · rw [scaleRoots_zero, scaleRoots_zero, Algebra.smul_def, Algebra.smul_def]
      simp [resultant_C_mul_right, resultant_X_pow_right, *, (Ne.symm hf0)]
    conv_lhs => rw [← natDegree_scaleRoots f r, ← natDegree_scaleRoots g r]
    rw [resultant_eq_prod_eval _ _ _ le_rfl hf',
      resultant_eq_prod_eval _ _ _ le_rfl (hf'.scaleRoots _),
      roots_scaleRoots _ (isUnit_iff_ne_zero.mpr hr)]
    simp only [Multiset.map_map, Function.comp_def, scaleRoots_eval_mul]
    simp only [leadingCoeff_scaleRoots, natDegree_scaleRoots, Multiset.prod_map_mul,
      Multiset.map_const', Multiset.prod_replicate, ← hf'.natDegree_eq_card_roots]
    ring
  | injective R S φ hφ f IH =>
    have := IH (g.map φ) (φ r) (by simpa using (map_injective _ hφ).ne hf)
      (by simpa using (map_injective _ hφ).ne hg)
    apply hφ
    rw [← map_scaleRoots, ← map_scaleRoots] at this
    · simpa [natDegree_map_eq_of_injective hφ] using this
    all_goals simpa [map_eq_zero_iff _ hφ]
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g', hg', eg⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g)
    obtain ⟨r, rfl⟩ := hφ r
    have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
    have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
    rw [← hf', ← map_scaleRoots _ _ _ (by simpa [← hfl]), ← hg',
      ← map_scaleRoots _ _ _ (by simpa [← hgl]), hf', hg',
      ← natDegree_eq_natDegree ef, ← natDegree_eq_natDegree eg,
      resultant_map_map, IH f' g' r (by aesop) (by aesop)]
    rw [← hf', ← hg', resultant_map_map]
    simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
⊢ (map φ f').coeff f'.natDegree = φ (f'.coeff f'.natDegree)

Tactic:
coeff_map

Goal state after: