mathlib-initiative/mathlib-tactics huggingface dataset:
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]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
x y : FractionRing R[X]
⊢ ({ toFractionRing := x } * { toFractionRing := y }).liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := x }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := y }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯

Tactic:
cases x using Localization.induction_on with | _ pq
     =>  _ 

Goal state after:
case H
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]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
y : FractionRing R[X]
pq : R[X] × ↥R[X]⁰
⊢ ({ toFractionRing := Localization.mk pq.1 pq.2 } * { toFractionRing := y }).liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk pq.1 pq.2 }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := y }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
S : Sieve U
⊢ S ∈ (grothendieckTopology X) U ↔
    Sieve.generate (U.presieveOfSections (sectionsOfPresieve S.arrows)) ∈ (grothendieckTopology X) U

Tactic:
presieveOfSections_sectionsOfPresieve,

Goal state after:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
⊢ S ∈ (grothendieckTopology X) U ↔ Sieve.generate S.arrows ∈ (grothendieckTopology X) U
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ ∀ (z : K⟮X⟯), ∃ x, z * (algebraMap K[X] K⟮X⟯) ↑x.2 = (algebraMap K[X] K⟮X⟯) x.1

Tactic:
rintro ⟨z⟩

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
z : FractionRing K[X]
⊢ ∃ x, { toFractionRing := z } * (algebraMap K[X] K⟮X⟯) ↑x.2 = (algebraMap K[X] K⟮X⟯) x.1
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ (toFractionRingRingEquiv K).symm = (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) K⟮X⟯).toRingEquiv

Tactic:
ext x
  simp [toFractionRingRingEquiv, ofFractionRing_eq]

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

Goal state before:
pp: case pos
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
hf : Module.Finite k⟮X⟯ K⟮X⟯
hrank : Module.rank k⟮X⟯ K⟮X⟯ = Module.rank k K
⊢ Module.finrank k⟮X⟯ K⟮X⟯ = Module.finrank k K

Tactic:
← Module.finrank_eq_rank

Goal state after:
case pos
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
hf : Module.Finite k⟮X⟯ K⟮X⟯
hrank : ↑(Module.finrank k⟮X⟯ K⟮X⟯) = Module.rank k K
⊢ Module.finrank k⟮X⟯ K⟮X⟯ = Module.finrank k K
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
⊢ QuasiFiniteAt (Spec.map φ) x ↔ IsOpen {⟨x, ⋯⟩}

Tactic:
HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)

Goal state after:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝ : (CommRingCat.Hom.hom φ).FiniteType
⊢ QuasiFiniteAt (Spec.map φ) x ↔ IsOpen {⟨x, ⋯⟩}
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra R S✝
inst✝ : Algebra R T
P : StandardEtalePair R
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
⊢ Function.Bijective (⇑P.homEquiv ∘ (Ideal.Quotient.mkₐ R I).comp ∘ ⇑P.homEquiv.symm)

Tactic:
suffices ∀ x, P.HasMap (Ideal.Quotient.mk I x) → ∃! a : { x : S // P.HasMap x }, a - x ∈ I by
    simpa [Function.bijective_iff_existsUnique, Ideal.Quotient.mk_surjective.forall,
      Subtype.ext_iff, Ideal.Quotient.mk_eq_mk_iff_sub_mem]

Goal state after:
R : Type u_1
S✝ : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
inst✝² : CommRing T
inst✝¹ : Algebra R S✝
inst✝ : Algebra R T
P : StandardEtalePair R
S : Type u_1
x✝¹ : CommRing S
x✝ : Algebra R S
I : Ideal S
hI : I ^ 2 = ⊥
⊢ ∀ (x : S), P.HasMap ((Ideal.Quotient.mk I) x) → ∃! a, ↑a - x ∈ I
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
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
a : S'
ham : a ∈ m
⊢ {f} ⊆ ↑(RingHom.ker (AlgHom.restrictScalars R (aeval a)).toRingHom)

Tactic:
suffices (m.map (a - ·)).prod = 0 by simpa [← eval_map_algebraMap, hm, eval_multiset_prod]

Goal state after:
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
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
a : S'
ham : a ∈ m
⊢ (Multiset.map (fun x ↦ a - x) m).prod = 0
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]
ht : φ.IsIntegralElem t
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'
⊢ ∃ q n, IsIntegral R (a ^ n • t - φ q)

Tactic:
have ha : IsUnit (algebraMap R R' a) := IsLocalization.Away.algebraMap_isUnit a

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]
ht : φ.IsIntegralElem t
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)
⊢ ∃ q n, IsIntegral R (a ^ n • t - φ q)
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)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x : S
⊢ p.leadingCoeff ^ s.sup n • t * x ∈ φ.range

Tactic:
Algebra.smul_mul_assoc

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
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x : S
⊢ p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
i : Fin n
⊢ ↑((basis R n) i) = X ^ ↑i

Tactic:
change _ = ((⟨X ^ (i : ℕ), mem_degreeLT.2 <| (degree_X_pow_le i).trans_lt <|
      Nat.cast_lt.2 i.is_lt⟩ : R[X]_n) : R[X])

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
i : Fin n
⊢ ↑((basis R n) i) = ↑⟨X ^ ↑i, ⋯⟩
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
inst✝ : Algebra.Smooth R S
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
by
  have (m : PrimeSpectrum S) : ∃ f ∉ m.asIdeal,
      Function.Bijective (toIntegralClosure R (Localization.Away f) B) := by
    obtain ⟨f, hfm, n, _, _, _⟩ :=
      Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial (R := R) (p := m.asIdeal)
    exact ⟨f, hfm, toIntegralClosure_bijective_of_tower (S := MvPolynomial (Fin n) R)
      toIntegralClosure_mvPolynomial_bijective toIntegralClosure_bijective_of_isStandardEtale⟩
  choose f hfm hf using this
  refine TensorProduct.toIntegralClosure_bijective_of_isLocalizationAway (R := R)
    (s := Set.range f) (B := B) ?_ (Localization.Away ·.1) (Set.forall_subtype_range_iff.mpr hf)
  by_contra H
  obtain ⟨m, hm, e⟩ := Ideal.exists_le_maximal _ H
  exact hfm ⟨m, inferInstance⟩ (e (Ideal.subset_span (Set.mem_range_self ⟨m, inferInstance⟩)) :)

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
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
⊢ (algebraMap ↑Γ(Y, ↑U) ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))).IsIntegral

Tactic:
exact algebraMap_isIntegral_iff.mpr inferInstance

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
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
⊢ (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    (Algebra.ofId R 𝓡).comp ((MvPolynomial.mapEquivMonic R R n).symm p)

Tactic:
let := ((MvPolynomial.mapEquivMonic R _ n).symm p).toAlgebra

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) =
    (Algebra.ofId R 𝓡).comp ((MvPolynomial.mapEquivMonic R R n).symm p)
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
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
⊢ (fun q ↦
        Algebra.TensorProduct.lift (Algebra.ofId R S)
          (let __RingHom :=
            (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))).symm
                  q)).toRingHom;
          { toRingHom := __RingHom, commutes' := ⋯ })
          ⋯)
      ((fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩) f) =
    f

Tactic:
let := ((MvPolynomial.mapEquivMonic R _ n).symm p).toAlgebra

Goal state after:
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
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (fun q ↦
        Algebra.TensorProduct.lift (Algebra.ofId R S)
          (let __RingHom :=
            (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))).symm
                  q)).toRingHom;
          { toRingHom := __RingHom, commutes' := ⋯ })
          ⋯)
      ((fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩) f) =
    f
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
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p }
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
⊢ (fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩)
      ((fun q ↦
          Algebra.TensorProduct.lift (Algebra.ofId R S)
            (let __RingHom :=
              (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))).symm
                    q)).toRingHom;
            { toRingHom := __RingHom, commutes' := ⋯ })
            ⋯)
        q) =
    q

Tactic:
let := ((MvPolynomial.mapEquivMonic R _ n).symm p).toAlgebra

Goal state after:
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
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p }
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩)
      ((fun q ↦
          Algebra.TensorProduct.lift (Algebra.ofId R S)
            (let __RingHom :=
              (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))).symm
                    q)).toRingHom;
            { toRingHom := __RingHom, commutes' := ⋯ })
            ⋯)
        q) =
    q
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
⊢ (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)

Tactic:
let := ((MvPolynomial.mapEquivMonic R _ n).symm p).toAlgebra

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝² : Nontrivial 𝓡
h✝¹ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
h✝ : Nontrivial R
this✝ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
⊢ (presentation m k hn p).jacobian = (-1) ^ n * (↑(factor₁ m k hn p)).resultant ↑(factor₂ m k hn p)
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
⊢ P = RingHom.ker (algebraMap R P.ResidueField)

Tactic:
Ideal.ker_algebraMap_residueField

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
⊢ P = P
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H : W ≤ f ⁻¹ᵁ U
⊢ appLE (toNormalization f ≫ fromNormalization f) U (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r) ⋯ =
    appLE f U W H

Tactic:
simp [W]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hf₂
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
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor T (↑R h1Cotangentι))

Tactic:
simp only [LinearMap.exact_zero_iff_injective]

Goal state after:
case hf₂
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
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑(LinearMap.lTensor T (↑R h1Cotangentι))
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝ R A : CommRingCat
inst✝¹ : Algebra ↑R ↑A
inst✝ : Algebra.FiniteType ↑R ↑A
⊢ LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A)))

Tactic:
HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)

Goal state after:
R✝ R A : CommRingCat
inst✝¹ : Algebra ↑R ↑A
inst✝ : Algebra.FiniteType ↑R ↑A
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap ↑R ↑A))).FiniteType
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g h i : a ⟶ b
η η' : f ⟶ g
α : g ≅ h
θ θ' : h ⟶ i
αθ : g ⟶ i
ηαθ : f ⟶ i
e_η : η = η'
e_θ : θ = θ'
e_αθ : α.hom ≫ θ' = αθ
e_ηαθ : η' ≫ αθ = ηαθ
⊢ η ≫ α.hom ≫ θ = ηαθ

Tactic:
simp [e_η, e_θ, e_αθ, e_ηαθ]

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

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f :
  (Spec (CommRingCat.of T)).asOver (Spec (CommRingCat.of R)) ⟶
    (Spec (CommRingCat.of S)).asOver (Spec (CommRingCat.of R))
⊢ CommRingCat.ofHom (algebraMap R S) ≫ preimage (Over.Hom.left f) = CommRingCat.ofHom (algebraMap R T)

Tactic:
apply Spec.map_injective

Goal state after:
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f :
  (Spec (CommRingCat.of T)).asOver (Spec (CommRingCat.of R)) ⟶
    (Spec (CommRingCat.of S)).asOver (Spec (CommRingCat.of R))
⊢ map (CommRingCat.ofHom (algebraMap R S) ≫ preimage (Over.Hom.left f)) = map (CommRingCat.ofHom (algebraMap R T))
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
tfae_1_to_2 : Function.Surjective ⇑(algebraMap R S) → Function.Bijective ⇑(LinearMap.mul' R S)
H : Function.Bijective ⇑(LinearMap.mul' R S)
p : PrimeSpectrum R
⊢ rankAtStalk S p ≤ 1

Tactic:
by
    have h : rankAtStalk (S ⊗[R] S) p = rankAtStalk S p ^ 2 := by
      simp [rankAtStalk_tensorProduct, sq]
    by_contra! hc
    apply Nat.succ_succ_ne_one 0
    rw [← Nat.pow_eq_self_iff hc, ← h, Module.rankAtStalk_eq_of_equiv
      (AlgEquiv.ofBijective (Algebra.TensorProduct.lmul' R (S := S)) H).toLinearEquiv]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
hg : g = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

Tactic:
simp [hg]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ (Scheme.Hom.opensRange (Sigma.ι (fun i ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier ⊆ (zeroLocus t)ᶜ

Tactic:
· rw [Scheme.Hom.opensRange_comp]
      exact (Set.image_subset_range _ _).trans (hV.trans ht')

Goal state after: