mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : X.AffineZariskiSite
h : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V
x : ↥X
hx : x ∈ (toOpensFunctor X).obj U
⊢ ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h)).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨f, hfU, hxf⟩ := V.2.exists_basicOpen_le ⟨x, hx⟩ (h.le hx)

Goal state after:
X : Scheme
U V : X.AffineZariskiSite
h : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V
x : ↥X
hx : x ∈ (toOpensFunctor X).obj U
f : ↑Γ(X, ↑V)
hfU : X.basicOpen f ≤ (toOpensFunctor X).obj U
hxf : ↑⟨x, hx⟩ ∈ X.basicOpen f
⊢ ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h)).arrows f ∧ x ∈ U_1
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ Sieve.coverByImage (toOpensFunctor X) U ∈ (Opens.grothendieckTopology ↥X) U

Tactic:
x

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
⊢ x ∈ U → ∃ U_1 f, (Sieve.coverByImage (toOpensFunctor X) U).arrows f ∧ x ∈ U_1
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1) → ∃ V f, S.arrows f ∧ x ∈ V.toOpens

pp: X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ V f, S.arrows f ∧ x ∈ V.toOpens) → ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1

Tactic:
· rintro ⟨V, f, ⟨W, g, h, hg, rfl⟩, hxV⟩
    exact ⟨W, g, hg, h.le hxV⟩

Goal state after:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ V f, S.arrows f ∧ x ∈ V.toOpens) → ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case refine_2
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ Presieve.ofArrows (fun i ↦ U.basicOpen ↑i) (fun i ↦ homOfLE ⋯) { down := { down := ⋯ } } →
    U.presieveOfSections s { down := { down := ⋯ } }

Tactic:
rintro ⟨⟨f, hfs⟩⟩
    exact ⟨f, hfs, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

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✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
p : Ideal T
inst✝ : p.IsPrime
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ m, IsIntegral R (s ^ m * x)
t : S
htp : t ∉ Ideal.under S p
Ht : ⊥.saturation (Submonoid.powers ((algebraMap S T) t)) ⋯ = ⊤
m : ℕ
hm : IsIntegral R (s ^ m * t)
⊢ (algebraMap S T) (s ^ (m + 1) * t) ∉ p

Tactic:
simpa using ‹p.IsPrime›.mul_notMem
      (mt ((inferInstance : (p.under S).IsPrime).mem_of_pow_mem (m + 1)) hsp) htp

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
hRS : integralClosure R S = ⊥
x : S
hx : (aeval x).Finite
u : S
p : R[X]
e : (aeval ((Ideal.Quotient.mk (conductor R x).radical) x)) p * (Ideal.Quotient.mk (conductor R x).radical) u = 0
⊢ map (algebraMap R (S ⧸ (conductor R x).radical)) p * C ((Ideal.Quotient.mk (conductor R x).radical) u) = 0

Tactic:
rw [← Ideal.Quotient.algebraMap_eq, aeval_algebraMap_apply, Ideal.Quotient.algebraMap_eq,
    ← map_mul, Ideal.Quotient.eq_zero_iff_mem] at e

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
hRS : integralClosure R S = ⊥
x : S
hx : (aeval x).Finite
u : S
p : R[X]
e : (aeval x) p * u ∈ (conductor R x).radical
⊢ map (algebraMap R (S ⧸ (conductor R x).radical)) p * C ((Ideal.Quotient.mk (conductor R x).radical) u) = 0
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
⊢ ↑f /ₘ X ^ m = ↑((addLinearEquiv R m n) f).2 ∧ ↑((addLinearEquiv R m n) f).1 = ↑f %ₘ X ^ m

Tactic:
eq_comm (b := _ %ₘ _)

Goal state after:
m n : ℕ
R : Type u_2
inst✝ : Ring R
f : ↥R[X]_(m + n)
⊢ ↑f /ₘ X ^ m = ↑((addLinearEquiv R m n) f).2 ∧ ↑f %ₘ X ^ m = ↑((addLinearEquiv R m n) f).1
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝³ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝¹ : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this : Algebra (Localization.AtPrime (Ideal.under (↥R') p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R') p) p
x : S
hx : x ∈ ↑s
⊢ r ∈ p.primeCompl ⊓ R'.toSubmonoid

Tactic:
exact ⟨hrp, hrR'⟩

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

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
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
this :
  (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).range ≤
    (Localization.awayMapₐ (adjoin R t).val r').range
x : S
n : ℕ
y : Localization.Away r'
hy :
  (Localization.awayMap (adjoin R t).val.toRingHom r') y =
    (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).toRingHom x
⊢ ∃ a,
    (Localization.awayMap (adjoin R t).val.toRingHom r') a =
      IsLocalization.mk' (Localization.Away ((adjoin R t).val.toRingHom r')) x
        ⟨(fun x ↦ (adjoin R t).val.toRingHom r' ^ x) n, ⋯⟩

Tactic:
refine ⟨y * Localization.Away.invSelf _ ^ n, ?_⟩

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
p : Ideal S
H : ZariskisMainProperty R p
s : Finset S
hs : adjoin R ↑s = ⊤
r : S
hrp : r ∉ p
hr : IsIntegral R r
m : S → ℕ
hm : ∀ (x : S), IsIntegral R (r ^ m x * x)
t : Set S := insert r {x | ∃ x_1 ∈ s, r ^ m x_1 * x_1 = x}
r' : ↥(adjoin R t) := ⟨r, ⋯⟩
this :
  (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).range ≤
    (Localization.awayMapₐ (adjoin R t).val r').range
x : S
n : ℕ
y : Localization.Away r'
hy :
  (Localization.awayMap (adjoin R t).val.toRingHom r') y =
    (IsScalarTower.toAlgHom R S (Localization.Away ((adjoin R t).val r'))).toRingHom x
⊢ (Localization.awayMap (adjoin R t).val.toRingHom r') (y * Localization.Away.invSelf r' ^ n) =
    IsLocalization.mk' (Localization.Away ((adjoin R t).val.toRingHom r')) x
      ⟨(fun x ↦ (adjoin R t).val.toRingHom r' ^ x) 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₂
⊢ normalizationDesc f f₁ f₂ H ≫ f₂ = fromNormalization f

Tactic:
by
  refine colimit.hom_ext fun U ↦ ?_
  dsimp [normalizationDesc, fromNormalization]
  rw [colimit.ι_desc_assoc, (normalizationGlueData f).ι_toBase, Category.assoc,
    ← IsAffineOpen.SpecMap_appLE_fromSpec _ U.2 _ le_rfl, ← Spec.map_comp_assoc]
  dsimp [normalizationGlueData, relativeGluingData, restrictIsoSpec]
  rw [Category.assoc]
  congr 2
  ext i
  dsimp [normalizationDiagram, normalizationDiagramMap, RingHom.algebraMap_toAlgebra]
  rw [← CommRingCat.comp_apply, Hom.appLE_comp_appLE, app_eq_appLE]
  simp_rw [H]

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
⊢ f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
by_cases hg0 : g = 0

Goal state after:
case pos
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
⊢ f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod

case neg
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
⊢ f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
a b : ℕ
⊢ a + b = ↑j →
    (a = ↑i → ¬b = ↑j - ↑i) →
      (if h : b < k then if a < m ∧ a = ↑i then X (Sum.inr ⟨b, ⋯⟩) else 0
        else if b = k ∧ a < m ∧ a = ↑i then 1 else 0) =
        0

Tactic:
e

Goal state after:
case inr.h₀
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑i ≤ ↑j
a b : ℕ
e : a + b = ↑j
⊢ (a = ↑i → ¬b = ↑j - ↑i) →
    (if h : b < k then if a < m ∧ a = ↑i then X (Sum.inr ⟨b, ⋯⟩) else 0 else if b = k ∧ a < m ∧ a = ↑i then 1 else 0) =
      0
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.e_a.e_3.e_f.hC
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
x✝ : R
⊢ (((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
            ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl))).comp
        C)
      x✝ =
    (Algebra.TensorProduct.includeLeftRingHom.comp C) x✝

Tactic:
simp [-algebraMap_apply, -AddMonoidAlgebra.coe_algebraMap, ← algebraMap_eq]

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

Goal state before:
pp: case inr.e_a.e_3.e_f.hX
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
i✝ : Fin m
⊢ ((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
        ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)))
      (X i✝) =
    Algebra.TensorProduct.includeLeftRingHom (X i✝)

Tactic:
simp [-algebraMap_apply, -AddMonoidAlgebra.coe_algebraMap, ← algebraMap_eq]

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

Goal state before:
pp: case inr.e_a.e_4.e_f.hC
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
x✝ : R
⊢ (((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
            ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr))).comp
        C)
      x✝ =
    ((↑Algebra.TensorProduct.includeRight).comp C) x✝

Tactic:
simp [-algebraMap_apply, -AddMonoidAlgebra.coe_algebraMap, ← algebraMap_eq]

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

Goal state before:
pp: case inr.e_a.e_4.e_f.hX
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
i✝ : Fin k
⊢ ((↑(aeval (universalFactorizationMapPresentation R n m k hn).val)).comp
        ↑((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)))
      (X i✝) =
    ↑Algebra.TensorProduct.includeRight (X i✝)

Tactic:
simp [-algebraMap_apply, -AddMonoidAlgebra.coe_algebraMap, ← algebraMap_eq]

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]
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
H : (b * g).natDegree < (a * f).natDegree
⊢ False

Tactic:
have := natDegree_add_eq_left_of_natDegree_lt H

Goal state after:
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
H : (b * g).natDegree < (a * f).natDegree
this : (a * f + b * g).natDegree = (a * f).natDegree
⊢ False
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.leadingCoeff ^ m ≠ 0
hn : g.natDegree ≤ n
⊢ (f ^ m).resultant g (f ^ m).natDegree n = f.resultant g f.natDegree n ^ m

Tactic:
convert! resultant_prod_left (Finset.range m) (fun _ ↦ f) g n (by simpa) hn <;> simp

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

Goal state before:
pp: case neg
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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
by_cases hg0 : g = 0

Goal state after:
case pos
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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

case neg
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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
by_cases hg0 : g = 0

Goal state after:
case pos
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : g = 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case Splits.mem.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r s : R
⊢ ((taylor r) (X + C s)).resultant ((taylor r) g) = (X + C s).resultant g

Tactic:
· nontriviality R
        rw [map_add, taylor_X, taylor_C, add_assoc, ← map_add]
        simp [-map_add, taylor_eval]

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
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
φ : 𝓡' →ₐ[R] P.ResidueField := (homEquiv P.ResidueField m k hn p).symm ⟨(f, g), ⋯⟩
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
⊢ ∃ Q,
    ∃ (x : Q.IsPrime) (x_1 : Q.LiesOver P),
      Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯) ∧
        f.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
            (factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField) ∧
          g.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
            (factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField)

Tactic:
have H : φi.comp φ = (IsScalarTower.toAlgHom _ _ _) :=
    AlgHom.ext fun x ↦ e.eq_symm_apply.mp (by simp [e, φ'])

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
P : Ideal R
inst✝ : P.IsPrime
f : MonicDegreeEq P.ResidueField m
g : MonicDegreeEq P.ResidueField k
H✝ : map (algebraMap R P.ResidueField) ↑p = ↑f * ↑g
Hpq : IsCoprime ↑f ↑g
φ : 𝓡' →ₐ[R] P.ResidueField := (homEquiv P.ResidueField m k hn p).symm ⟨(f, g), ⋯⟩
Q : Ideal 𝓡' := RingHom.ker φ.toRingHom
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := Ideal.ResidueField.liftₐ Q φ ⋯ ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := AlgEquiv.ofAlgHom φi φ' ⋯ ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ ∃ Q,
    ∃ (x : Q.IsPrime) (x_1 : Q.LiesOver P),
      Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯) ∧
        f.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
            (factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField) ∧
          g.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
            (factor₂ m k hn p).map (algebraMap 𝓡' Q.ResidueField)
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
⊢ (LinearMap.toMatrix (((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv)
        (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) =
    f.sylvester g m n

Tactic:
by
  ext i j
  obtain ⟨j, rfl⟩ := finSumFinEquiv.surjective j
  simpa [LinearMap.toMatrix_apply] using congr($(toMatrix_sylvesterMap f g hf hg) i j)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : (b * g).natDegree < (a * f).natDegree
⊢ False

Tactic:
have := natDegree_add_eq_left_of_natDegree_lt H

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this✝ : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
H : (b * g).natDegree < (a * f).natDegree
this : (a * f + b * g).natDegree = (a * f).natDegree
⊢ False
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
⊢ ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}

Tactic:
Set.image_subset_iff,

Goal state after:
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
⊢ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Extension R S
T✝ : Type u_3
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
P : Extension R S
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
this✝¹ : Algebra P.Ring P.baseChange.Ring := P.algebraBaseChange T
this✝ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
x : R
⊢ (algebraMap R T) x ⊗ₜ[R] 1 = ((algebraMap S (T ⊗[R] S)).comp (algebraMap P.Ring S)) ((algebraMap R P.Ring) x)

Tactic:
Algebra.TensorProduct.tmul_one_eq_one_tmul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P✝ : Extension R S
T✝ : Type u_3
inst✝³ : CommRing T✝
inst✝² : Algebra R T✝
P : Extension R S
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
this✝¹ : Algebra P.Ring P.baseChange.Ring := P.algebraBaseChange T
this✝ : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
x : R
⊢ 1 ⊗ₜ[R] (algebraMap R S) x = ((algebraMap S (T ⊗[R] S)).comp (algebraMap P.Ring S)) ((algebraMap R P.Ring) x)