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

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
lem :
  ∀ {a : R},
    a ∈ I →
      l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
y : R
⊢ y ∈ l.support →
    (fun a c ↦ c • (algebraMap R S) a * (algebraMap R S) p) y (l y) ∈
      ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
hy

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
lem :
  ∀ {a : R},
    a ∈ I →
      l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
y : R
hy : y ∈ l.support
⊢ (fun a c ↦ c • (algebraMap R S) a * (algebraMap R S) p) y (l y) ∈
    ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
y : ↥R[x]
⊢ y ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I) → y ∈ Ideal.map (algebraMap R ↥R[x]) I

Tactic:
hy

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
y : ↥R[x]
hy : y ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)
⊢ y ∈ Ideal.map (algebraMap R ↥R[x]) I
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
r : ↥R[x]
hr : r ∈ Ideal.map (algebraMap R ↥R[x]) I
this : algebraMap R S = (algebraMap (↥R[x]) S).comp (algebraMap R ↥R[x])
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((algebraMap (↥R[x]) S) r) = 0

Tactic:
Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
r : ↥R[x]
hr : r ∈ Ideal.map (algebraMap R ↥R[x]) I
this : algebraMap R S = (algebraMap (↥R[x]) S).comp (algebraMap R ↥R[x])
⊢ (algebraMap (↥R[x]) S) r ∈ Ideal.map (algebraMap R S) I
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
u : ↥R[x]
hu : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((algebraMap (↥R[x]) S) u) = 0
⊢ u ∈ Ideal.map (algebraMap R ↥R[x]) I

Tactic:
Ideal.Quotient.eq_zero_iff_mem,

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
u : ↥R[x]
hu : (algebraMap (↥R[x]) S) u ∈ Ideal.map (algebraMap R S) I
⊢ u ∈ Ideal.map (algebraMap R ↥R[x]) I
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
⊢ v (∑ x ∈ Finset.range (p.natDegree + 1), (algebraMap K[X] K⟮X⟯) ((monomial x) (p.coeff x))) ≤ 1

Tactic:
apply map_sum_le v

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
⊢ ∀ i ∈ Finset.range (p.natDegree + 1), v ((algebraMap K[X] K⟮X⟯) ((monomial i) (p.coeff i))) ≤ 1
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case h
K : Type u_1
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ Valued.v (X ^ (-n.log)) = n

Tactic:
simp [WithZero.exp_log hn0]

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

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ 0 / φ ↑1 = 0

Tactic:
zero_div

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
⊢ Set.range ⇑(pullback.fst (colimit.desc F (cocone X)) (↑U).ι) =
    Set.range ⇑((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U)

Tactic:
rw [Pullback.range_fst, Opens.range_ι, ← Hom.coe_opensRange, Hom.opensRange_comp_of_isIso,
        ← Scheme.Hom.coe_preimage]
      convert! congr($(D.toBase_preimage_eq_opensRange_ι U).1)
      · delta cocone
        congr with U
        simp [D, relativeGluingData, restrictIsoSpec]
      · simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
⊢ ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.fst f ι) ⁻¹' ⇑f ⁻¹' {f ((pullback.fst f ι) x)}

Tactic:
rw [← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ← Scheme.Hom.comp_apply,
        pullback.condition]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
⊢ ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.snd f ι ≫ ι) ⁻¹' {(pullback.snd f ι ≫ ι) x}
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) = 1

Tactic:
← map_one (Ideal.Quotient.mk _),

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) =
    (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) 1
Module: Mathlib.FieldTheory.RatFunc.Basic

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

Tactic:
num_div _ q,

Goal state after:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
h : x.num = 0
⊢ 0 / (algebraMap K[X] K⟮X⟯) x.denom = 0

Tactic:
zero_div

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
h : x.num = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case e_6
R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ⋯
this✝⁴ : Q'.LiesOver Q
this✝³ : Q'.LiesOver P
this✝² : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := ⋯
this✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := ⋯
this✝ : IsUnramifiedAt P.ResidueField Q'
this : Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x))
⊢ (IsScalarTower.toAlgHom P.ResidueField Q.ResidueField Q'.ResidueField) ((algebraMap S Q.ResidueField) x) =
    (algebraMap (P.Fiber S) Q'.ResidueField) (1 ⊗ₜ[R] x)

Tactic:
simp [← TensorProduct.right_algebraMap_apply, ← IsScalarTower.algebraMap_apply]

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
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
a : S'
ha : a ∈ m
⊢ (Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) (m.erase a))).sum ≤ f.natDegree - 1

Tactic:
simp [ha, hmc]

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_2
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
⊢ Function.Surjective ⇑(algebraMap (Ideal.under (↥R[t]) Q).ResidueField Q.ResidueField)

Tactic:
change Function.Surjective (IsScalarTower.toAlgHom p.ResidueField _ _)
    rw [← AlgHom.range_eq_top, ← top_le_iff, ← ht]
    refine adjoin_singleton_le ?_
    use algebraMap (R[t]) _ ⟨t, self_mem_adjoin_singleton _ _⟩
    rw [AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom, ← IsScalarTower.algebraMap_apply]
    rfl

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

Goal state before:
pp: case convert_4
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
inst✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hfg : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
heg :
  ∀ (g : R[X]),
    e (1 ⊗ₜ[R] (aeval 𝓟.x) g) =
      (algebraMap (AdjoinRoot 𝓟'.f) (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)))
        ((AdjoinRoot.mk 𝓟'.f) (Polynomial.map (algebraMap R B) g))
k : ℕ
hk : IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a)
y : B[X]
hy : (AdjoinRoot.mk 𝓟'.f) (derivative 𝓟'.f) * ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ k * a) = (AdjoinRoot.mk 𝓟'.f) y
hRy : ∀ (i : ℕ), IsIntegral R (y.coeff i)
⊢ ∑ i ∈ Finset.range (y.natDegree + 1), Algebra.TensorProduct.includeRight.toRingHom (y.coeff i) * 𝓟.x ⊗ₜ[R] 1 ^ i ∈
    Subalgebra.toSubmodule (Algebra.adjoin S ↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)))

Tactic:
exact sum_mem fun i hi ↦ Subalgebra.mul_mem _ (Algebra.subset_adjoin ⟨_, hRy _, rfl⟩)
    (pow_mem (Subalgebra.algebraMap_mem _ _) _)

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.affineOpens
⊢ ((pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι) ≫ toNormalization f =
    (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫ toNormalization f

Tactic:
congr 1; simp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
⊢ f.resultant (g + f * (monomial k) r) m n = f.resultant g m n

Tactic:
have (i : ℕ) (hi : i ≤ m) : (M i).det = M₂.det := by
    induction i with
    | zero => simp [M]; rfl
    | succ i IH =>
      rw [← IH (by lia), ← Matrix.det_updateCol_add_smul_self (i := ⟨i, by lia⟩)
        (j := ⟨i + k + m, by lia⟩) (c := -r) (M (i + 1)) (by simp; lia)]
      congr 1
      ext j₁ j₂
      simp only [Matrix.of_apply, lt_add_iff_pos_right, zero_lt_one, ↓reduceIte, add_assoc,
        add_lt_add_iff_left, Nat.lt_one_iff, Nat.add_eq_zero_iff, hm, and_false, smul_eq_mul,
        Matrix.updateCol_apply, Fin.ext_iff, M, M₂, neg_mul, ← sub_eq_add_neg]
      obtain rfl | h := eq_or_ne ↑j₂ i
      · simp only [↓reduceIte, sylvester, Set.mem_Icc, coeff_add, Fin.eta, Matrix.of_apply,
          lt_self_iff_false, M₁]
        induction j₂ using Fin.addCases with
        | left j₂ =>
          dsimp at hi
          have : Fin.mk (n := m + n) (↑j₂ + (k + m)) (by lia) = .natAdd m ⟨j₂ + k, by lia⟩ :=
            Fin.ext (by simp; lia)
          simp only [Fin.addCases_left, Fin.val_castAdd, this, Fin.addCases_right, mul_ite,
            mul_zero, ← C_mul_X_pow_eq_monomial, ← mul_assoc, coeff_mul_X_pow', ite_add_zero,
            coeff_mul_C, add_assoc, add_eq_left, ← ite_and, ← mul_comm r, tsub_add_eq_tsub_tsub,
            add_sub_assoc, sub_eq_zero]
          split_ifs with h₁ h₂ h₂ <;> try rfl
          · rw [coeff_eq_zero_of_natDegree_lt, mul_zero]
            exact hf.trans_lt (by lia)
          · lia
        | right i =>
          simp only [Fin.val_natAdd] at hi
          have : Fin.mk (n := m + n) (m + ↑i + (k + m)) (by lia) =
              Fin.natAdd m ⟨↑i + (k + m), by lia⟩ := Fin.ext (by simp; lia)
          simp only [Fin.addCases_right, Fin.val_natAdd, sub_eq_self, this]
          rw [if_neg, mul_zero]
          lia
      lia

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
this : ∀ i ≤ m, (M i).det = M₂.det
⊢ f.resultant (g + f * (monomial k) r) m n = f.resultant g m n
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: 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₀
⊢ Spec.map
        (CommRingCat.ofHom
          ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
            (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)) ≫
      ⋯.fromSpec ≫ f₂ =
    (normalizationGlueData f).natTrans.app U ≫ (directedCover Y).f U

Tactic:
← IsAffineOpen.SpecMap_appLE_fromSpec _ U.2 _ le_rfl,

Goal state after:
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₀
⊢ Spec.map
        (CommRingCat.ofHom
          ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯)).codRestrict
            (integralClosure ↑Γ(Y, toOpens U) ↑Γ(X, f ⁻¹ᵁ toOpens U)) ⋯)) ≫
      Spec.map (appLE f₂ (↑U) (f₂ ⁻¹ᵁ ↑U) ⋯) ≫ ⋯.fromSpec =
    (normalizationGlueData f).natTrans.app U ≫ (directedCover Y).f U
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
⊢ f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
let L := g.SplittingField

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
⊢ f.resultant g f.natDegree n = (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
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
⊢ (-1) ^ ((f₁.natDegree + f₂.natDegree) * n) *
      ((-1) ^ (n * f₁.natDegree) * f₁.resultant g f₁.natDegree n * g.resultant f₂ n) =
    f₁.resultant g f₁.natDegree n * f₂.resultant g f₂.natDegree n

Tactic:
resultant_comm f₂

Goal state after:
R : Type u_1
inst✝ : CommRing R
f₁ f₂ g : R[X]
n : ℕ
hn : g.natDegree ≤ n
⊢ (-1) ^ ((f₁.natDegree + f₂.natDegree) * n) *
      ((-1) ^ (n * f₁.natDegree) * f₁.resultant g f₁.natDegree n * g.resultant f₂ n) =
    f₁.resultant g f₁.natDegree n * ((-1) ^ (f₂.natDegree * n) * g.resultant f₂ n)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.surjective
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]
r : S
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:
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.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ ↑((MvPolynomial.mapEquivMonic R 𝓡 n) ((Algebra.ofId R 𝓡).comp ((MvPolynomial.mapEquivMonic R R n).symm p))) =
    ↑(monicDegreeEq m k hn p)

Tactic:
simp [MvPolynomial.coe_mapEquivMonic_comp, monicDegreeEq]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Nontrivial 𝓡'
⊢ IsUnit ((↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p))

Tactic:
factor₁,

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Nontrivial 𝓡'
⊢ IsUnit ((↑((UniversalFactorizationRing.factor₁ m k hn p).map (algebraMap 𝓡 𝓡'))).resultant ↑(factor₂ m k hn p))
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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
by
  rw [natDegree_scaleRoots, natDegree_integralNormalization]
  wlog hR : IsDomain R
  · by_cases hf0 : f = 0; · simp [hf0]
    by_cases hg0 : g = 0; · simp [hg0]
    let S := MvPolynomial R ℤ
    let φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap _ _) id
    have hφ : Function.Surjective φ := fun x ↦ ⟨.X x, by simp [φ, MvPolynomial.eval₂Hom]⟩
    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)
    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 [← natDegree_eq_natDegree ef, ← natDegree_eq_natDegree eg,
      ← hf', hgl, ← map_scaleRoots _ _ _ (by simpa [← hfl]), ← hg', integralNormalization_map _ _
      (by simpa [← hgl]), resultant_map_map,
      this f' g' (by simpa [natDegree_eq_natDegree eg]) inferInstance]
    simp [resultant_map_map]
  by_cases hg0 : g = 0; · simp [hg0]
  apply mul_right_injective₀ (a := g.leadingCoeff ^ f.natDegree) (by simp [hg0])
  dsimp
  have := resultant_scaleRoots f g g.leadingCoeff
  rw [natDegree_scaleRoots, natDegree_scaleRoots,
    ← integralNormalization_mul_C_leadingCoeff, mul_comm, resultant_C_mul_right] at this
  rw [this, ← mul_assoc, ← pow_add, add_comm, ← Nat.mul_add_one, Nat.sub_add_cancel (by lia)]

Goal state after: