mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
            Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
          (P x * Q z - Q x * P z) /
        (P z * Q z) ^ 2 /
      ((P x * Q z - Q x * P z) ^ 3 / (P z * Q z)) =
    W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
toAffine_slope_of_ne hPz hQz hx,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
            Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
          (P x * Q z - Q x * P z) /
        (P z * Q z) ^ 2 /
      ((P x * Q z - Q x * P z) ^ 3 / (P z * Q z)) =
    W.toAffine.addX (P x / P z) (Q x / Q z) ((P y * Q z - Q y * P z) / (P x * Q z - Q x * P z))
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig✝ : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
p :
  Fin (Presentation.ofFinitePresentationRels A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
homog : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (p j).IsHomogeneous 2
hp : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (eval P.relation) (p j) = (aeval h) (P.relation j)
hsig : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), f (h i) = P.val i
i : Fin (Presentation.ofFinitePresentationVars A B)
⊢ h i - X i ∈ Ideal.span (Set.range P.relation)

Tactic:
simpa [P.span_range_relation_eq_ker, sub_eq_zero, f] using hsig i

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsProper f ↔ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f

Tactic:
rw [isProper_iff, ← and_assoc]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (IsSeparated f ∧ UniversallyClosed f) ∧ LocallyOfFiniteType f ↔
    (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f
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
⊢ ∑ i, (fun x ↦ coeff (↑x) F) i • (aeval a) ((monomial ↑i) 1) = 0

Tactic:
simp only [← map_smul, ← map_sum, Finset.univ_eq_attach, smul_eq_mul, mul_one]

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
⊢ (aeval a) (∑ x ∈ F.support.attach, (monomial ↑x) (coeff (↑x) F)) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ((P y * Q z - Q y * P z) *
            ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                      W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                    W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
                  P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
                Q x * P z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2) +
          P y * Q z * (P x * Q z - Q x * P z) ^ 3) /
        (P z * Q z) ^ 2 /
      ((P x * Q z - Q x * P z) ^ 3 / (P z * Q z)) =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
toAffine_slope_of_ne hPz hQz hx,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ((P y * Q z - Q y * P z) *
            ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                      W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                    W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
                  P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
                Q x * P z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2) +
          P y * Q z * (P x * Q z - Q x * P z) ^ 3) /
        (P z * Q z) ^ 2 /
      ((P x * Q z - Q x * P z) ^ 3 / (P z * Q z)) =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z) ((P y * Q z - Q y * P z) / (P x * Q z - Q x * P z))
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
this :
  ((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) =
    Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)
⊢ (aeval a) F'' = 0

Tactic:
simp only [← hF', F'', ← this]

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
this :
  ((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) =
    Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)
⊢ (aeval a) (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')) =
    ((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) F'
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFinitePresentation f
⊢ Flat f ∧ FormallyUnramified f ∧ LocallyOfFinitePresentation f

Tactic:
exact ⟨inferInstance, inferInstance, inferInstance⟩

Goal state after:
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_4
S' : Type u_5
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsPushout R S R' S'
inst✝ : IsStandardOpenImmersion R S
⊢ IsPushout R R' S S'

Tactic:
IsPushout.comm

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_4
S' : Type u_5
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsPushout R S R' S'
inst✝ : IsStandardOpenImmersion R S
⊢ IsPushout R S R' S'
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: ⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ IsStandardOpenImmersion

Tactic:
introv R h
  exact .algebraMap r

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

Goal state before:
pp: X Y : Scheme
⊢ ∀ {Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f → IsOpenImmersion (pullback.fst f g) → IsOpenImmersion g

Tactic:
Z

Goal state after:
X Y Z : Scheme
⊢ ∀ {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f → IsOpenImmersion (pullback.fst f g) → IsOpenImmersion g
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ∀ {a b : S}, a ∈ {s | IsAlmostIntegral R s} → b ∈ {s | IsAlmostIntegral R s} → a * b ∈ {s | IsAlmostIntegral R s}

Tactic:
by
    rintro a b ⟨r, hr, hr'⟩ ⟨s, hs, hs'⟩
    refine ⟨r * s, mul_mem hr hs, fun n ↦ ?_⟩
    rw [mul_pow, mul_smul_mul_comm]
    exact mul_mem (hr' _) (hs' _)

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
z : S
hz : z ∈ R[x]
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
⊢ (algebraMap R S) p * z + (algebraMap R S) q * z = z

Tactic:
simp only [← add_mul, ← map_add (algebraMap R S), hpq, map_one, one_mul]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx : x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p)
a : S
ha : x • a ∈ Ideal.map (algebraMap R S) p
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : (aeval (x • a)) f = 0
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
i : ℕ
hi : i ≠ (minpoly R a).natDegree
hip : (minpoly R a).coeff i ∉ p
hx0 : x = 0
⊢ x ∈ p

Tactic:
simp [hx0]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case smul
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal R
x✝ : S
A : Subalgebra R R[X] := Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}
this : Algebra R[X] S[X] := algebra R S
a x : S
hx✝ : x ∈ Submodule.span S (⇑(algebraMap R S) '' ↑I)
hx : IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C x * X)
⊢ IsIntegral (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) (C (a • x) * X)

Tactic:
simp only [smul_eq_mul, map_mul, mul_assoc]
    refine .mul ?_ hx
    exact ((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ (valuation K⟮X⟯ (idealX K)) ((algebraMap K[X] K⟮X⟯) X) = exp (-1)

Tactic:
valuation_of_algebraMap,

Goal state after:
K : Type u_1
inst✝ : Field K
⊢ (idealX K).intValuation X = exp (-1)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
H : ∀ {x : S}, x ∈ m → p.IsRoot x
⊢ ∀ i ∈ Finset.univ, ∀ (j : ℕ), IsIntegral R (i.fst.coeff j)

Tactic:
rintro ⟨a, ⟨i, hi⟩⟩ -

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i✝ : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
H : ∀ {x : S}, x ∈ m → p.IsRoot x
a : S[X]
i : ℕ
hi : i < Multiset.count a (Multiset.map (fun x ↦ X - C x) m)
⊢ ∀ (j : ℕ), IsIntegral R (⟨a, ⟨i, hi⟩⟩.fst.coeff j)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i✝ : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
i : ℕ
hi : i ∉ q.support
⊢ (q.coeff i).natDegree < m

Tactic:
simp_all [m]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ (∑ i ∈ Finset.range (q.natDegree + 1), q.coeff i * (X ^ m) ^ i).Monic

Tactic:
Finset.sum_range_succ

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
⊢ (∑ x ∈ Finset.range q.natDegree, q.coeff x * (X ^ m) ^ x + q.coeff q.natDegree * (X ^ m) ^ q.natDegree).Monic
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

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
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
r : R[X]
hr✝ : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
hx : r ∈ J
⊢ x = 0

Tactic:
refine ((IsUnit.mk0 (algebraMap R I.ResidueField s) (by simpa)).map C).mul_right_injective ?_

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
r : R[X]
hr✝ : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
hx : r ∈ J
⊢ (fun x ↦ C ((algebraMap R I.ResidueField) s) * x) x = (fun x ↦ C ((algebraMap R I.ResidueField) s) * x) 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.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✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
y✝¹ y✝ : R[X] × ↥R[X]⁰
⊢ (↑(map φ hφ)).toFun
      ({ toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } + { toFractionRing := Localization.mk y✝.1 y✝.2 }) =
    (↑(map φ hφ)).toFun { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } +
      (↑(map φ hφ)).toFun { toFractionRing := Localization.mk y✝.1 y✝.2 }

Tactic:
simp only [← ofFractionRing_add, Localization.add_mk, map_add, map_mul,
          MonoidHom.toFun_eq_coe, map_apply_ofFractionRing_mk, Submonoid.coe_mul,
          -- We have to specify `S[X]⁰` to `mk_mul_mk`, otherwise it will try to rewrite
          -- the wrong occurrence.
          Submonoid.mk_mul_mk S[X]⁰]

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

Goal state before:
pp: X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
⊢ MorphismProperty.isomorphisms Scheme
    (Cover.pullbackHom (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯) ((colimit.isColimit F).desc (cocone X)) U)

Tactic:
change IsIso (pullback.snd (colimit.desc F (cocone X)) U.1.ι)

Goal state after:
X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
⊢ IsIso (pullback.snd (colimit.desc F (cocone X)) (↑U).ι)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr.H.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]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ (↑q * p' + ↑q' * p) * (φ ↑q * φ ↑q') = (φ p * φ ↑q' + φ ↑q * φ p') * φ ↑(q * q')

Tactic:
rw [mul_comm _ p, mul_comm _ p', mul_comm _ (φ p'), add_comm]
        simp only [map_add, map_mul, Submonoid.coe_mul]

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.finrank k⟮X⟯ K⟮X⟯) = Module.rank k K
⊢ Module.finrank k⟮X⟯ K⟮X⟯ = Module.finrank k K

Tactic:
exact (Module.finrank_eq_of_rank_eq hrank.symm).symm

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case inr.refine_2
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' : derivative m ≠ 0
⊢ (aeval x) (derivative q) ∉ Q

Tactic:
suffices ¬m ∣ derivative (q.map (algebraMap R _)) by
    rwa [← Ideal.ker_algebraMap_residueField Q, RingHom.mem_ker, ← aeval_algebraMap_apply,
      ← aeval_map_algebraMap P.ResidueField, ← derivative_map, ← minpoly.dvd_iff]

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
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' : derivative m ≠ 0
⊢ ¬m ∣ derivative (Polynomial.map (algebraMap R P.ResidueField) q)