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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ IsLocalRing.maximalIdeal (Localization.AtPrime p) ≤
    Ideal.comap (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) (Ideal.map (algebraMap R Sq) p)

Tactic:
by
    rw [← IsLocalization.AtPrime.map_eq_maximalIdeal p, Ideal.map_le_iff_le_comap,
      ← Ideal.comap_coe (F := AlgHom _ _ _), Ideal.comap_comap]
    simpa [← IsScalarTower.algebraMap_eq] using Ideal.le_comap_map

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

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
S : Sieve U
⊢ S ∈ (grothendieckTopology X) U ↔ ∀ x ∈ U.toOpens, ∃ V f, S.arrows f ∧ x ∈ V.toOpens

Tactic:
rw [grothendieckTopology, Functor.mem_inducedTopology_iff_of_isCoverDense]

Goal state after:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
⊢ Sieve.functorPushforward (toOpensFunctor X) S ∈ (Opens.grothendieckTopology ↥X) ((toOpensFunctor X).obj U) ↔
    ∀ x ∈ U.toOpens, ∃ V f, S.arrows f ∧ x ∈ V.toOpens
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
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
hp : φ p * t ∈ (conductor R (φ X)).radical
i : ℕ
this :
  ∀ (p : R[X]),
    φ p * t ∈ (conductor R (φ X)).radical → ∀ (i : ℕ), i = p.natDegree → p.coeff i • t ∈ (conductor R (φ X)).radical
hi : ¬i = p.natDegree
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

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]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
i : ℕ
hi : i = p.natDegree
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
· clear hi
    simp only [forall_eq, coeff_natDegree] at this
    induction hpn : p.natDegree using Nat.strong_induction_on generalizing p with
    | h n IH =>
    cases n with
    | zero =>
      obtain hi' | hi' := lt_or_ge p.natDegree i
      · simp [coeff_eq_zero_of_natDegree_lt hi']
      · simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp
    | succ n =>
      obtain hi' | hi' := eq_or_ne i p.natDegree
      · simpa [hi'] using this _ hp
      have : φ p.eraseLead * t ∈ (conductor R (φ X)).radical := by
        simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
        exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))
      simpa [eraseLead_coeff, hi'] using
        IH _ ((eraseLead_natDegree_le _).trans_lt (by lia)) _ this rfl

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]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
i : ℕ
hi : i = p.natDegree
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical
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]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ (conductor R (φ X)).radical
i : ℕ
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
wlog hi : i = p.natDegree generalizing p i
  · clear hi
    simp only [forall_eq, coeff_natDegree] at this
    induction hpn : p.natDegree using Nat.strong_induction_on generalizing p with
    | h n IH =>
    cases n with
    | zero =>
      obtain hi' | hi' := lt_or_ge p.natDegree i
      · simp [coeff_eq_zero_of_natDegree_lt hi']
      · simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp
    | succ n =>
      obtain hi' | hi' := eq_or_ne i p.natDegree
      · simpa [hi'] using this _ hp
      have : φ p.eraseLead * t ∈ (conductor R (φ X)).radical := by
        simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ t]
        exact sub_mem hp (Ideal.mul_mem_right _ _ (this _ hp))
      simpa [eraseLead_coeff, hi'] using
        IH _ ((eraseLead_natDegree_le _).trans_lt (by lia)) _ this rfl
  obtain ⟨n, hn⟩ := hp
  obtain ⟨k, hk⟩ := exists_leadingCoeff_pow_smul_mem_conductor φ (t ^ n) (p ^ n) hRS hφ
    (by simpa [mul_pow] using hn)
  by_cases hpn : p.leadingCoeff ^ n = 0
  · use n; simp [_root_.smul_pow, hpn, hi]
  rw [leadingCoeff_pow' hpn, ← pow_mul] at hk
  refine ⟨n * k + n, ?_⟩
  rw [_root_.smul_pow, pow_add, add_comm, pow_add, mul_smul_mul_comm, hi]
  exact Ideal.mul_mem_right _ _ hk

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
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
⊢ False

Tactic:
have : IsDomain R := (FaithfulSMul.algebraMap_injective R S).isDomain

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
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this : IsDomain R
⊢ False
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case intro
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
⊢ ¬IsStronglyTranscendental R x

Tactic:
have : IsDomain R := (FaithfulSMul.algebraMap_injective R S).isDomain

Goal state after:
case intro
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsReduced S
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
left✝ : IsDomain S
right✝ : FaithfulSMul R S
this : IsDomain R
⊢ ¬IsStronglyTranscendental R x
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

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

Tactic:
← two_mul,

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

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

Tactic:
congr 1; lia

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case e'_6
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✝¹ : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this✝ : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
this : IsScalarTower (MvPolynomial (Fin n) R) (↥R') S
i : Fin n
⊢ f (MvPolynomial.X i.succ) = (algebraMap (MvPolynomial (Fin n) R) S) (MvPolynomial.X i)

Tactic:
simp [RingHom.algebraMap_toAlgebra, f', MvPolynomial.finSuccEquiv,
            MvPolynomial.optionEquivLeft]

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

Goal state before:
pp: case neg
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] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
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
this :
  (Multiset.map (fun x ↦ eval x f) g.roots).prod =
    (f %ₘ g).leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x r) g.roots).prod
⊢ (-1) ^ (f.natDegree * g.natDegree) * (algebraMap K L) (f %ₘ g).leadingCoeff ^ g.natDegree *
      (Multiset.map (fun x ↦ (aeval ((algebraMap K L) x)) r) g.roots).prod =
    (-1) ^ (f.natDegree * g.natDegree) * (algebraMap K L) (f %ₘ g).leadingCoeff ^ g.natDegree *
      (Multiset.map (fun x ↦ (algebraMap K L) (eval x r)) g.roots).prod

Tactic:
congr 3 with x

Goal state after:
case neg.e_a.e_f
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] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
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
this :
  (Multiset.map (fun x ↦ eval x f) g.roots).prod =
    (f %ₘ g).leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x r) g.roots).prod
x : K
⊢ (aeval ((algebraMap K L) x)) r = (algebraMap K L) (eval x r)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.Splits
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
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
| Splits R f hf' =>

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
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ f' ≠ 0

Tactic:
by aesop

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
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ g' ≠ 0

Tactic:
by aesop

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
p : MonicDegreeEq R n
Δ : 𝓡 := (presentation m k hn p).jacobian
hΔ : IsUnit ((algebraMap 𝓡 (Localization.Away Δ)) Δ)
P : Algebra.SubmersivePresentation R (Localization.Away Δ) (Unit ⊕ Fin m ⊕ Fin k) (Unit ⊕ Fin n) :=
  let __PreSubmersivePresentation :=
    (Algebra.PreSubmersivePresentation.localizationAway (Localization.Away Δ) Δ).comp (presentation m k hn p);
  { toPreSubmersivePresentation := __PreSubmersivePresentation, jacobian_isUnit := ⋯ }
⊢ P.dimension = 0

Tactic:
by
      simp only [Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension, P]
      simp [Algebra.Presentation.dimension, hn]

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

Goal state before:
pp: case Splits
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
⊢ ((taylor r) f).resultant ((taylor r) g) = f.resultant g

Tactic:
| Splits R f hf' =>

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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ f.map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R 𝓡') ⋯).toRingHom =
    (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).1

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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).1 = (factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField)

Tactic:
· simp [homEquiv_comp_fst, φ, φi]

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 := ⋯
Q : Ideal 𝓡' := ⋯
this✝ : Q.IsPrime
this : Q.LiesOver P
φ' : Q.ResidueField →ₐ[R] P.ResidueField := ⋯
φi : P.ResidueField →ₐ[R] Q.ResidueField := ⋯
e : P.ResidueField ≃ₐ[R] Q.ResidueField := ⋯
H : φi.comp φ = IsScalarTower.toAlgHom R 𝓡' Q.ResidueField
⊢ (↑((homEquiv Q.ResidueField m k hn p) (φi.comp φ))).1 = (factor₁ m k hn p).map (algebraMap 𝓡' Q.ResidueField)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
p : R[X]
f g : P.ResidueField[X]
hp : p.Monic
hf : f.Monic
hg : g.Monic
H : map (algebraMap R P.ResidueField) p = f * g
Hpq : IsCoprime f g
Q : Ideal (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
w✝¹ : Q.IsPrime
w✝ : Q.LiesOver P
h₁ :
  Function.Bijective
    ⇑(Ideal.ResidueField.mapₐ P Q
        (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))) ⋯)
h₂ :
  (MonicDegreeEq.mk f hf ⋯).map
      (Ideal.ResidueField.mapₐ P Q
          (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)))
          ⋯).toRingHom =
    (factor₁ f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)).map
      (algebraMap (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
        Q.ResidueField)
h₃ :
  (MonicDegreeEq.mk g hg ⋯).map
      (Ideal.ResidueField.mapₐ P Q
          (Algebra.ofId R (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)))
          ⋯).toRingHom =
    (factor₂ f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯)).map
      (algebraMap (UniversalCoprimeFactorizationRing f.natDegree g.natDegree ⋯ (MonicDegreeEq.mk p hp ⋯))
        Q.ResidueField)
⊢ ∃ R' x x_1,
    ∃ (_ : Algebra.Etale R R'),
      ∃ Q,
        ∃ (x_3 : Q.IsPrime) (x_4 : Q.LiesOver P),
          ∃ f' g',
            Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯) ∧
              f'.Monic ∧
                g'.Monic ∧
                  map (algebraMap R R') p = f' * g' ∧
                    IsCoprime f' g' ∧
                      map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom f =
                          map (algebraMap R' Q.ResidueField) f' ∧
                        map (Ideal.ResidueField.mapₐ P Q (Algebra.ofId R R') ⋯).toRingHom g =
                          map (algebraMap R' Q.ResidueField) g'

Tactic:
exact ⟨_, _, _, inferInstance, Q, ‹_›, ‹_›, (factor₁ ..).1, (factor₂ ..).1, h₁,
    (factor₁ ..).monic, (factor₂ ..).monic, (factor₁_mul_factor₂ ..).symm,
    isCoprime_factor₁_factor₂ .., congr(($h₂).1), congr(($h₃).1)⟩

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⟨s, hRs⟩
hfs₀ : (aeval s₀) f = 0
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : (aeval s') f = 0
hs₀'f : (aeval (1 ⊗ₜ[R] s₀)) f = 0
e₀ : R' ⊗[R] ↥(integralClosure R S) := (aeval (1 ⊗ₜ[R] s₀)) (c * a')
⊢ (aeval (1 ⊗ₜ[R] s₀)) (c * a' - c * d * Polynomial.map (algebraMap R R') f) = (aeval (1 ⊗ₜ[R] s₀)) (c * a')

Tactic:
simp only [map_mul, map_sub, aeval_map_algebraMap, hs₀'f, mul_zero, sub_zero]

Goal state after:
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
x y : ↥I
⊢ (↑R (map (algebraMap S (T ⊗[R] S)) I).toCotangent)
      ((Algebra.idealMap (T ⊗[R] S) I) x * (Algebra.idealMap (T ⊗[R] S) I) y) =
    0

Tactic:
simp only [RingHom.algebraMap_toAlgebra, AlgHom.toRingHom_eq_coe, LinearMap.coe_restrictScalars,
      toCotangent_eq_zero, sq, MulMemClass.coe_mul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
x y : ↥I
⊢ ↑((Algebra.idealMap (T ⊗[R] S) I) x) * ↑((Algebra.idealMap (T ⊗[R] S) I) y) ∈
    map (↑Algebra.TensorProduct.includeRight) I * map (↑Algebra.TensorProduct.includeRight) I
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ IsFinite (f ∣_ V)

Tactic:
suffices LocallyQuasiFinite (f ∣_ V) from .of_isProper_of_locallyQuasiFinite _
    rw [← Scheme.Hom.quasiFiniteLocus_eq_top_iff]
    ext x
    have : f.QuasiFiniteAt ((f ⁻¹ᵁ V).ι x) := by by_contra H; exact x.2 ⟨_, H, by simp⟩
    rw [← Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion, ← morphismRestrict_ι,
      Scheme.Hom.quasiFiniteAt_comp_iff] at this
    simpa

Goal state after:
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)
this✝¹ : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := P.baseChange
this✝ : IsPushout R T P.Ring PT.Ring
this : IsScalarTower P.Ring PT.Ring (T ⊗[R] S)
⊢ ∀ (t x : T) (y : S), ((TensorProduct.mk R T S) (t • x)) y = t • ((TensorProduct.mk R T S) x) y

Tactic:
by simp [Algebra.smul_def]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R : CommRingCat
X Y : (CommAlgCat ↑R)ᵒᵖ
⊢ Over.Hom.left (Over.homMk (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv ⋯) =
    Over.Hom.left (prodComparison (algSpec R) X Y)

Tactic:
prodComparison_algSpec_left

Goal state after:
R : CommRingCat
X Y : (CommAlgCat ↑R)ᵒᵖ
⊢ Over.Hom.left (Over.homMk (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv ⋯) =
    (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv