mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hFa : (aeval a) F = 0
i : ι
hi : i ∈ F.vars
⊢ IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
have ⟨σ, hσ, hσi⟩ := (mem_vars_iff_mem_support i).mp hi

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hFa : (aeval a) F = 0
i : ι
hi : i ∈ F.vars
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hσi : i ∈ σ.support
⊢ IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
⊢ ∀ b ∈ F''.support, (p * b.sum fun x e ↦ e) ≤ F.totalDegree

Tactic:
intro σ hσ

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
σ : ι →₀ ℕ
hσ : σ ∈ F''.support
⊢ (p * σ.sum fun x e ↦ e) ≤ F.totalDegree
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
have alg := isAlgebraic_of_mem_vars_of_forall_totalDegree_le hFmin hFa i <|
    (mem_vars_iff_mem_support i).mpr ⟨σ, hσ, by simpa⟩

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this✝ : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
this : g₁.base = g₂.base
⊢ x ∈ ↑(g₂ ⁻¹ᵁ V)

Tactic:
simpa [← this]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P Q W : MorphismProperty C
A X✝ Y✝ Z : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z
g✝ : Y✝ ⟶ Z
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
⊢ s ≫ 𝟙 S = f ≫ t

Tactic:
simp [hf]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (W'⁄B).negAddY (⇑↑f ∘ P) (⇑↑f ∘ Q) = ↑f ((W'⁄A).negAddY P Q)

Tactic:
← map_negAddY,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (W'⁄B).negAddY (⇑↑f ∘ P) (⇑↑f ∘ Q) = ((W'⁄A).map ↑f).negAddY (⇑↑f ∘ P) (⇑↑f ∘ Q)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ p ∈ Ideal.span {map (algebraMap R P.ResidueField) r}

Tactic:
(IsLocalization.map_units P.ResidueField[X] s).unit.eq_mul_inv_iff_mul_eq.mpr e

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
inst✝ : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = Ideal.span {p}
this✝¹ : Algebra (R ⧸ P)[X] P.ResidueField[X] := (mapRingHom (algebraMap (R ⧸ P) P.ResidueField)).toAlgebra
this✝ : IsLocalization (Submonoid.map C (R ⧸ P)⁰) P.ResidueField[X]
this : p ∈ Ideal.map (algebraMap (R ⧸ P)[X] P.ResidueField[X]) (Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I)
s : ↥(Submonoid.map C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr : (mapRingHom (algebraMap R (R ⧸ P))) r ∈ Ideal.map (mapRingHom (algebraMap R (R ⧸ P))) I
e : p * map (algebraMap (R ⧸ P) P.ResidueField) ↑s = map (algebraMap R P.ResidueField) r
⊢ map (algebraMap R P.ResidueField) r * ↑⋯.unit⁻¹ ∈ Ideal.span {map (algebraMap R P.ResidueField) r}
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
P : Ideal ↑R
hP : P.IsPrime
⊢ LocallyQuasiFinite (Spec.map (CommRingCat.ofHom (algebraMap P.ResidueField (P.Fiber ↑S))))

Tactic:
obtain ⟨x, rfl⟩ : ∃ x : Spec R, P = x.asIdeal := ⟨⟨P, hP⟩, rfl⟩

Goal state after:
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ LocallyQuasiFinite (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
⊢ Sieve.generate (U.presieveOfSections s) ∈ (grothendieckTopology X) U ↔ ↑U ≤ ⨆ f, X.basicOpen ↑f

Tactic:
mem_grothendieckTopology,

Goal state after:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
⊢ (∀ x ∈ U.toOpens, ∃ V f, (Sieve.generate (U.presieveOfSections s)).arrows f ∧ x ∈ V.toOpens) ↔
    ↑U ≤ ⨆ f, X.basicOpen ↑f
Module: Mathlib.FieldTheory.RatFunc.Basic

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

Tactic:
by
  by_cases hf : Module.Finite k⟮X⟯ K⟮X⟯
  · have hrank := rank_ratFunc_ratFunc k K
    rw [← Module.finrank_eq_rank] at hrank
    exact (Module.finrank_eq_of_rank_eq hrank.symm).symm
  · have hf' : ¬ Module.Finite k K := by
      rwa [← Module.rank_lt_aleph0_iff, ← rank_ratFunc_ratFunc, Module.rank_lt_aleph0_iff]
    rw [Module.finrank_of_not_finite hf, Module.finrank_of_not_finite hf']

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
x : S
h : P.HasMap x
⊢ (P.lift x h) P.X = x

Tactic:
by
  simp [lift, StandardEtalePair.Ring, StandardEtalePair.X]

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

Goal state before:
pp: case mp
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ x.num ∣ p → ∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

pp: case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ (∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.num ∣ p

Tactic:
· rintro ⟨q, rfl⟩
    obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp
    use denom x * q
    rw [map_mul, map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]
    · exact ⟨mul_ne_zero (denom_ne_zero x) hq, rfl⟩
    · exact algebraMap_ne_zero hq

Goal state after:
case mpr
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hp : p ≠ 0
⊢ (∃ q, q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) → x.num ∣ p
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
P : StandardEtalePresentation R S
⊢ Function.Bijective ⇑({ f := X, monic_f := ⋯, g := 1, cond := ⋯ }.lift 0 ⋯)

Tactic:
by
    set P : StandardEtalePair R := ⟨.X, by simp, 1, 1, 0, 0, by simp⟩
    have : P.X = 0 := Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span (Set.mem_insert _ _))
    let e := AlgEquiv.ofAlgHom (P.lift (0 : R) ⟨by simp [P], by simp [P]⟩) (Algebra.ofId _ _)
      (by ext) (by ext; simp [this])
    exact e.bijective

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]
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)]
this✝³ : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝² : Algebra (↥R₂) St := R₂.toAlgebra
this✝¹ : Algebra (↥R₁) St := R₁.toAlgebra
this✝ : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ eval₂ (algebraMap (↥R₂) St) ((algebraMap S St) t) (map (↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)) q) = 0

Tactic:
eval₂_map,

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]
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)]
this✝³ : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝² : Algebra (↥R₂) St := R₂.toAlgebra
this✝¹ : Algebra (↥R₁) St := R₁.toAlgebra
this✝ : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ eval₂ ((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)) ((algebraMap S St) t) q = 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]
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
⊢ eval₂ (aeval ((algebraMap S S') (φ X))).toRingHom ((algebraMap S S') t) (map (mapRingHom (algebraMap R R')) q) = 0

Tactic:
eval₂_map,

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
⊢ eval₂ ((aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R'))) ((algebraMap S S') t) q = 0
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case pos.refine_3
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
⊢ (algebraMap R S) ((f.eraseLead + C a * X ^ m).coeff n) ∉ p

Tactic:
suffices algebraMap R S (f.coeff n) + algebraMap R S (if n = m then a else 0) ∉ p by
        simpa [eraseLead_coeff, show n ≠ f.natDegree by rintro rfl; exact hfn (by simpa)]
      rwa [Ideal.add_mem_iff_left]
      split_ifs
      · convert p.mul_mem_right x Hfp
        simpa [Algebra.smul_def] using! ha
      · simp

Goal state after:
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' := ⋯ }
⊢ WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p

Tactic:
exact .of_restrictScalars R _ _

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.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ app (fromNormalization f) U =
    CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
      (normalizationObjIso f hU).inv

Tactic:
rw [← cancel_mono (((normalizationOpenCover f).f ⟨U, hU⟩).app (f.fromNormalization ⁻¹ᵁ U)),
    ← Scheme.Hom.comp_app, Scheme.Hom.congr_app (f.ι_fromNormalization ⟨U, hU⟩) U,
    ← cancel_mono (((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op)]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsAffineOpen U
this✝ : Algebra ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this : IsIso (app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U))
H : ⊤ = ((normalizationOpenCover f).f ⟨U, hU⟩ ≫ fromNormalization f) ⁻¹ᵁ U
⊢ (app (Spec.map ((normalizationDiagramMap f).app (Opposite.op ↑⟨U, hU⟩)) ≫ IsAffineOpen.fromSpec ⋯) U ≫
        ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom ⋯).op) ≫
      ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op =
    ((CommRingCat.ofHom (algebraMap ↑(Y.presheaf.1 (Opposite.op U)) ↥(integralClosure ↑Γ(Y, U) ↑Γ(X, f ⁻¹ᵁ U))) ≫
          (normalizationObjIso f hU).inv) ≫
        app ((normalizationOpenCover f).f ⟨U, hU⟩) (fromNormalization f ⁻¹ᵁ U)) ≫
      ((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op
Module: Mathlib.RingTheory.ZariskisMainTheorem

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 S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
this✝ : Small.{u, v} S
this :
  ∃ r ∉ Ideal.comap (Shrink.algEquiv R S).toRingEquiv.toRingHom p,
    ∀ (x : Shrink.{u, v} S), ∃ m, IsIntegral R (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)

Tactic:
obtain ⟨r, hr, H⟩ := this

Goal state after:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FiniteType R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
this : Small.{u, v} S
r : Shrink.{u, v} S
hr : r ∉ Ideal.comap (Shrink.algEquiv R S).toRingEquiv.toRingHom p
H : ∀ (x : Shrink.{u, v} S), ∃ m, IsIntegral R (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)
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
⊢ (-1) ^ (g.natDegree * (f.natDegree - r.natDegree)) * g.coeff g.natDegree ^ (f.natDegree - r.natDegree) *
      ((-1) ^ (r.natDegree * g.natDegree) * g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

Tactic:
apply (algebraMap K L).injective
    rw [map_mul, map_mul, map_mul, this, map_sub_roots_sprod_eq_prod_map_eval _ _ hf hf',
      map_sub_sprod_roots_eq_prod_map_eval _ _ (hr.map _) (SplittingField.splits _), map_mul,
      hg'.roots_map]
    have : (g.roots.map (eval · f)).prod =
        (f %ₘ g).leadingCoeff ^ g.natDegree * (g.roots.map (eval · r)).prod := by
      trans (g.roots.map ((f %ₘ g).leadingCoeff * eval · r)).prod
      · congr 1
        refine Multiset.map_congr rfl ?_
        simp only [mem_roots', ne_eq, IsRoot.def, eval_mul, eval_C, leadingCoeff_eq_zero, hr₀,
          not_false_eq_true, mul_inv_cancel_left₀, and_imp, r]
        intro x hx hxg
        conv_lhs => rw [← f.modByMonic_add_div, eval_add, eval_mul, hxg, zero_mul, add_zero]
      · simp [hg'.natDegree_eq_card_roots]
    simp only [coeff_natDegree, hg.leadingCoeff, one_pow, map_one, map_multiset_prod,
      ← hf'.natDegree_eq_card_roots, ← hg'.natDegree_eq_card_roots, this, map_mul, Multiset.map_map,
      map_pow, map_neg, mul_one, eval_map_algebraMap, Function.comp_apply]
    simp only [← mul_assoc, ← pow_add, ← add_mul, Nat.sub_add_cancel (hrd.le.trans hfg),
      mul_comm g.natDegree]
    congr 3 with x
    exact aeval_algebraMap_apply _ _ _

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

Goal state before:
pp: 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

pp: 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

Tactic:
· subst hg0
    by_cases hf' : f.natDegree = 0
    · obtain ⟨r, rfl⟩ := hfm.natDegree_eq_zero.mp hf'; simp
    simp [← hf.natDegree_eq_card_roots, hf']

Goal state after:
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.Resultant.Basic

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

Tactic:
convert! resultant_X_sub_C_pow_right f 0 m n hm <;> simp [coeff_zero_eq_eval_zero]

Goal state after: