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

Goal state before:
pp: case inr
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
⊢ ∃ g, φ (derivative f) * φ y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)

Tactic:
algebraize [(algebraMap S S').comp (algebraMap R S)]

Goal state after:
case inr
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'))
⊢ ∃ g, φ (derivative f) * φ y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)
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
p : Ideal S
⊢ ZariskisMainProperty R p ↔
    ∃ r ∉ p, ∃ (h : IsIntegral R r), (integralClosure R S).saturation (Submonoid.powers r) ⋯ = ⊤

Tactic:
simp [zariskisMainProperty_iff, ← top_le_iff, SetLike.le_def,
    Submonoid.mem_powers_iff, mem_integralClosure_iff]

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
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
⊢ IsIntegral R t

Tactic:
let R₂ := Algebra.adjoin R₁ {algebraMap S St (φ X)}

Goal state after:
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 : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
⊢ IsIntegral R t
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
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
⊢ (algebraMap S S') (eval₂ (↑φ) t q) = 0

Tactic:
← AlgHom.toRingHom_eq_coe,

Goal state after:
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]
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
⊢ (algebraMap S S') (eval₂ φ.toRingHom t q) = 0
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
x : S
hQ' : (Ideal.under (↥R[x]) Q).primesOver S = {Q}
hQ'Q : Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this✝³ : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this✝² : Module.Finite (↥S') S
this✝¹ : IsUnramifiedAt (↥S') Q
hφ : Function.Bijective ⇑(Localization.localRingHom Q' Q ↑S'.val ⋯)
r : ↥R[x]
hrQ' : r ∉ Ideal.under (↥R[x]) Q
H : ∀ (r' : ↥R[x]), r ∣ r' → Function.Bijective ⇑(Localization.awayMap (algebraMap (↥R[x]) S) r')
this✝ : Module.Finite R ↥S'
this : IsUnramifiedAt R Q'
⊢ Subalgebra.map S'.val R[⟨x, ⋯⟩] = Subalgebra.map S'.val ⊤

Tactic:
by simp [Subalgebra.range_val, S']

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝⁴ : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝³ : Algebra R[X] S := f.toAlgebra
this✝² : IsScalarTower R R[X] S
this✝¹ : Module.Finite R[X] S
this✝ : FaithfulSMul R[X] S
this : Ideal.map C (Ideal.under R P) < Ideal.under R[X] P
⊢ False

Tactic:
obtain ⟨Q, hQ, _, ⟨e⟩⟩ := Ideal.exists_ideal_lt_liesOver_of_lt (S := S) P this

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝⁴ : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝³ : Algebra R[X] S := f.toAlgebra
this✝² : IsScalarTower R R[X] S
this✝¹ : Module.Finite R[X] S
this✝ : FaithfulSMul R[X] S
this : Ideal.map C (Ideal.under R P) < Ideal.under R[X] P
Q : Ideal S
hQ : Q < P
left✝ : Q.IsPrime
e : Ideal.map C (Ideal.under R P) = Ideal.under R[X] Q
⊢ False
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case inr.refine_1
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✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
    [inst_3 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q],
    Unramified R S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H✝ : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
inst : Unramified R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf : IsLocalization.mk' (Localization.Away s) f t ∉ Ideal.map (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (IsLocalization.mk' (Localization.Away s) f t)
⊢ s * f ∉ Q

pp: case inr.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✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
    [inst_3 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q],
    Unramified R S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H✝ : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
inst : Unramified R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf : IsLocalization.mk' (Localization.Away s) f t ∉ Ideal.map (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (IsLocalization.mk' (Localization.Away s) f t)
⊢ HasStandardEtaleSurjectionOn R (s * f)

Tactic:
· simpa [IsLocalization.mk'_mem_map_algebraMap_iff, Submonoid.mem_powers_iff,
        Ideal.IsPrime.mul_mem_left_iff, hsQ, (mt (‹Q.IsPrime›.mem_of_pow_mem _) hsQ)] using hf

Goal state after:
case inr.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✝¹ : FiniteType R S
inst✝ : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
    [inst_3 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q],
    Unramified R S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H✝ : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified R (Localization.Away s)
hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime
inst : Unramified R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf : IsLocalization.mk' (Localization.Away s) f t ∉ Ideal.map (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (IsLocalization.mk' (Localization.Away s) f t)
⊢ HasStandardEtaleSurjectionOn R (s * f)
Module: Mathlib.RingTheory.Polynomial.DegreeLT

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

Tactic:
rw [and_comm, eq_comm, eq_comm (b := _ %ₘ _)]
  nontriviality R; refine div_modByMonic_unique _ _ (monic_X_pow _) ⟨?_, ?_⟩
  · rw [← addLinearEquiv_symm_apply', LinearEquiv.symm_apply_apply]
  · rw [degree_X_pow, ← mem_degreeLT]; exact Subtype.prop _

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.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝³ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝² : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝¹ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)

Tactic:
f.preimage_basicOpen r

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝³ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝² : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝¹ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ f.resultant g m n = (-1) ^ (m * n) * g.resultant f n m

Tactic:
rw [resultant, resultant, sylvester_comm, Matrix.det_reindex, Equiv.Perm.sign_eq_prod_prod_Ioi]
  congr 1
  dsimp
  simp only [Fin.cast_lt_cast, Units.coe_prod, apply_ite, Units.val_one, Units.val_neg,
    Int.reduceNeg, Int.cast_prod, Int.cast_one, Int.cast_neg]
  simp_rw [← finSumFinEquiv.prod_comp, ← Finset.prod_map_equiv finSumFinEquiv.symm]
  simp only [Equiv.symm_apply_apply, ← Fin.val_fin_lt, Equiv.symm_symm, Function.comp_apply,
    ← Finset.prod_ite_mem_eq (Finset.map _ _), Finset.mem_map_equiv, Finset.mem_Ioi,
    Fintype.prod_sum_type, finSumFinEquiv_apply_left, Fin.val_castAdd, Sum.swap_inl,
    finSumFinEquiv_apply_right, Fin.val_natAdd, Sum.swap_inr, add_lt_add_iff_left,
    ← ite_not (α := R) (p := _ < _) (y := 1), ← ite_and, and_not_self]
  simp [(Fin.isLt _).trans_le, (Fin.isLt _).le.trans, pow_mul]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (-1) ^ (↑(Fin.last ((m + 1).add n)) + ↑(Fin.castAdd (n + 1) (Fin.last m))) *
        f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) (Fin.castAdd (n + 1) (Fin.last m)) *
      ((f.sylvester g (m + 1) (n + 1)).submatrix (Fin.last ((m + 1).add n)).succAbove
          (Fin.castAdd (n + 1) (Fin.last m)).succAbove).det =
    (-1) ^ (n + 1) * g.coeff (n + 1) * (f.sylvester g m (n + 1)).det

Tactic:
← Matrix.det_reindex_self (finCongr (show (m + 1).add n = m + (n + 1) by grind))

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (-1) ^ (↑(Fin.last ((m + 1).add n)) + ↑(Fin.castAdd (n + 1) (Fin.last m))) *
        f.sylvester g (m + 1) (n + 1) (Fin.last ((m + 1).add n)) (Fin.castAdd (n + 1) (Fin.last m)) *
      ((Matrix.reindex (finCongr ⋯) (finCongr ⋯))
          ((f.sylvester g (m + 1) (n + 1)).submatrix (Fin.last ((m + 1).add n)).succAbove
            (Fin.castAdd (n + 1) (Fin.last m)).succAbove)).det =
    (-1) ^ (n + 1) * g.coeff (n + 1) * (f.sylvester g m (n + 1)).det
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := ⋯
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := ⋯
this :
  (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
⊢ (Multiset.map (fun x ↦ (f %ₘ g).leadingCoeff * eval x r) g.roots).prod =
    (f %ₘ g).leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x r) g.roots).prod

Tactic:
· simp [hg'.natDegree_eq_card_roots]

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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
s : MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R
⊢ (aeval (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)) ((map C) ((tensorEquivSum R (Fin m) (Fin k) R) s)) = s

Tactic:
by
      change ((aeval _).restrictScalars R |>.comp (mapAlgHom (Algebra.ofId _ _)) |>.comp
          (tensorEquivSum R (Fin m) (Fin k) R).toAlgHom) s = AlgHom.id R _ s
      congr 1
      ext <;> simp

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

Goal state before:
pp: case neg.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ (f.scaleRoots r).leadingCoeff ^ (g.scaleRoots r).natDegree *
      (Multiset.map (fun x ↦ r ^ g.natDegree * eval x g) f.roots).prod =
    r ^ (f.natDegree * g.natDegree) * (f.leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x g) f.roots).prod)

Tactic:
simp only [leadingCoeff_scaleRoots, natDegree_scaleRoots, Multiset.prod_map_mul,
      Multiset.map_const', Multiset.prod_replicate, ← hf'.natDegree_eq_card_roots]

Goal state after:
case neg.inr
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
hr : r ≠ 0
⊢ f.leadingCoeff ^ g.natDegree * ((r ^ g.natDegree) ^ f.natDegree * (Multiset.map (fun i ↦ eval i g) f.roots).prod) =
    r ^ (f.natDegree * g.natDegree) * (f.leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x g) f.roots).prod)
Module: Mathlib.RingTheory.Finiteness.Descent

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
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
⊢ Ideal.map (algebraMap R S) I ≤ f.range

Tactic:
rw [Ideal.map_le_iff_le_comap]
      intro x hx
      use 1 ⊗ₜ ⟨x, hx⟩
      simp [f, Algebra.smul_def]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X✝ Y✝ S✝ : Scheme
f✝ : X✝ ⟶ S✝
inst✝⁴ : LocallyOfFiniteType f✝
X Y S : Scheme
f : X ⟶ Y
inst✝³ : LocallyQuasiFinite f
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
⊢ IsOpenImmersion (Scheme.Hom.toNormalization f)

Tactic:
convert!
    (inferInstance :
      IsOpenImmersion
        (X.topIso.inv ≫
          (X.isoOfEq f.quasiFiniteLocus_eq_top).inv ≫
            f.quasiFiniteLocus.ι ≫ f.toNormalization)) using 1

Goal state after:
X✝ Y✝ S✝ : Scheme
f✝ : X✝ ⟶ S✝
inst✝⁴ : LocallyOfFiniteType f✝
X Y S : Scheme
f : X ⟶ Y
inst✝³ : LocallyQuasiFinite f
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
⊢ Scheme.Hom.toNormalization f =
    X.topIso.inv ≫ (X.isoOfEq ⋯).inv ≫ (Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsProper f
inst✝ : LocallyQuasiFinite f
this : IsIso (Scheme.Hom.toNormalization f)
⊢ IsFinite f

Tactic:
refine (IsFinite.iff_isIntegralHom_and_locallyOfFiniteType _).mpr ⟨?_, inferInstance⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsProper f
inst✝ : LocallyQuasiFinite f
this : IsIso (Scheme.Hom.toNormalization f)
⊢ IsIntegralHom f
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
⊢ Over.Hom.left (Over.homMk (𝟙 (Spec R)) ⋯) = Over.Hom.left (CartesianMonoidalCategory.terminalComparison (algSpec R))

Tactic:
← preservesTerminalIso_hom,

Goal state after:
R : CommRingCat
⊢ Over.Hom.left (Over.homMk (𝟙 (Spec R)) ⋯) = Over.Hom.left (preservesTerminalIso (algSpec R)).hom
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h i j : b ⟶ c
α : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
θ : f ≫ i ⟶ f ≫ j
e_θ : f ◁ ηs = θ
⊢ f ◁ (α.hom ≫ η ≫ ηs) = (f ◁ᵢ α).hom ≫ f ◁ η ≫ θ

Tactic:
simp [e_θ]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η ε ⊗≫ rightZigzag η ε = rightZigzag η ε

Tactic:
by
  dsimp only [rightZigzag]
  calc
    _ = g ◁ η ⊗≫ ((ε ▷ g ▷ 𝟙 a) ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g := by
      bicategory
    _ = 𝟙 _ ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g := by
      rw [← whisker_exchange, ← whisker_exchange, leftZigzag]; bicategory
    _ = g ◁ η ⊗≫ ε ▷ g := by
      rw [h]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.inv.τl ≫ e.hom.τl = 𝟙 adj₂.l

Tactic:
rw [← comp_τl, e.inv_hom_id, id_τl]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom

Tactic:
by
      rw [← whisker_exchange η.hom η.inv]; bicategory

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
⊢ IsOpenImmersion f

Tactic:
let U : Y.Opens := ⟨Set.range f.base, f.isOpenMap.isOpen_range⟩

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
⊢ IsOpenImmersion f
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑f
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.Finite S T
algebraizeInst✝ : Module.Flat S T
this✝¹ : Module.Finite R T
this✝ : Module.Flat R T
this : Algebra.IsPushout R T S T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x

Tactic:
exact (Algebra.rankAtStalk_eq_of_isPushout _ _ _ _ _).symm

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

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective ⇑f
h1 : g.Finite
h2 : g.Flat
y : PrimeSpectrum R
x : PrimeSpectrum S
hy : y = PrimeSpectrum.comap f x
⊢ (g.comp f).finrank y = g.finrank x

Tactic:
subst hy
  algebraize [f, g, (g.comp f)]
  have : Module.Finite R T := h1.comp <| .of_surjective _ hg.2
  have : Module.Flat R T := (RingHom.Flat.of_bijective hg).comp h2
  have : Algebra.IsPushout R T S T := .of_bijective_left _ _ hg
  exact (Algebra.rankAtStalk_eq_of_isPushout _ _ _ _ _).symm

Goal state after: