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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h✝ : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
hq' : PrimeSpectrum.comap (algebraMap S (T i)) q' = { asIdeal := q, isPrime := hq }
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion R (Localization.Away g')
n : ℕ
g : S
hg : g' * (algebraMap S (T i)) (f i) ^ n = (algebraMap S (T i)) g
⊢ IsLocalization.Away g' (Localization.Away ((algebraMap S (T i)) g))

Tactic:
rw [← hg]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h✝ : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
hq' : PrimeSpectrum.comap (algebraMap S (T i)) q' = { asIdeal := q, isPrime := hq }
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion R (Localization.Away g')
n : ℕ
g : S
hg : g' * (algebraMap S (T i)) (f i) ^ n = (algebraMap S (T i)) g
⊢ IsLocalization.Away g' (Localization.Away (g' * (algebraMap S (T i)) (f i) ^ n))
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalIso R S
⊢ Ideal.map TensorProduct.includeRight ⊤ ≤ Ideal.span {g | IsStandardOpenImmersion T (Localization.Away g)}

Tactic:
← span_isStandardOpenImmersion_eq_top R S,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalIso R S
⊢ Ideal.map TensorProduct.includeRight (Ideal.span {g | IsStandardOpenImmersion R (Localization.Away g)}) ≤
    Ideal.span {g | IsStandardOpenImmersion T (Localization.Away g)}
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
⊢ (ResidueField R)[(residue S) β] = ⊤ → R[β] = ⊤

pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
⊢ R[β] = ⊤ → (ResidueField R)[(residue S) β] = ⊤

Tactic:
· intro hβ
    refine eq_top_iff.mpr <| Submodule.le_of_le_smul_of_le_jacobson_bot
      (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥)
      (?_ : ⊤ ≤ (adjoin R {β}).toSubmodule ⊔ maximalIdeal R • ⊤)
    intro s _
    rw [adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hβ
    obtain ⟨p, hp⟩ := hβ (residue S s)
    obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ residue_surjective p
    rw [Ideal.smul_top_eq_map]
    refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
    · rw [adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩
    · rw [Algebra.FormallyUnramified.map_maximalIdeal, Submodule.restrictScalars_mem,
        ← Ideal.Quotient.eq]
      -- def eq abuse since IsLocalRing.residue needs to be an abbrev
      rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl] at hp
      exact hp.symm

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
⊢ R[β] = ⊤ → (ResidueField R)[(residue S) β] = ⊤
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : (ResidueField R)⟮β₀⟯ = ⊤
β : S
hβ : (residue S) β = β₀
⊢ (ResidueField R)[(residue S) β] = ⊤

Tactic:
rw [hβ,
    ← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite _ _),
    hβ₀, IntermediateField.top_toSubalgebra]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : Etale R S
β : S
hadj : R[β] = ⊤
⊢ IsUnit ((aeval β) (derivative (minpoly R β)))

Tactic:
by
  apply fun s ↦ (residue_ne_zero_iff_isUnit s).mp
  rw [map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl,
    ← derivative_map, minpoly_map_residue hadj]
  exact (Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)

Goal state after:
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ maximalIdeal R ^ 2 < maximalIdeal R ↔ ¬IsField R

Tactic:
trans ¬ maximalIdeal R ^ 2 = maximalIdeal R

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ maximalIdeal R ^ 2 < maximalIdeal R ↔ ¬maximalIdeal R ^ 2 = maximalIdeal R

R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ ¬maximalIdeal R ^ 2 = maximalIdeal R ↔ ¬IsField R
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

Tactic:
intValuation_if_neg _ hP,

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ exp (-↑((Associates.mk (Polynomial.idealX K).asIdeal).count (Associates.mk (Ideal.span {P})).factors)) =
    (idealX K).intValuation ↑P
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

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
inst✝⁹ : p.IsPrime
Rₚ : Type u_3
inst✝⁸ : CommRing Rₚ
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : IsLocalization.AtPrime Rₚ p
inst✝⁵ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
⊢ P = RingHom.ker ((algebraMap Sₚ (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)).comp (algebraMap S Sₚ))

Tactic:
← RingHom.comap_ker,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
p : Ideal R
inst✝⁹ : p.IsPrime
Rₚ : Type u_3
inst✝⁸ : CommRing Rₚ
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : IsLocalization.AtPrime Rₚ p
inst✝⁵ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
⊢ P = comap (algebraMap S Sₚ) (RingHom.ker (algebraMap Sₚ (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ∃ a, Valued.v a = n

Tactic:
use ((HahnSeries.single (-WithZero.log n)) 1)
    simp [LaurentSeries.valuation_single_zpow, exp_log hn0]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
⊢ ∀ b ∈ {i_1 | ↑⟨i, ⋯⟩ ≤ ↑i_1}, b ≠ ⟨i, hin⟩ → t b = 0

Tactic:
refine fun j hij hji ↦ ht j ?_

Goal state after:
case h₀
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0
j : Fin n
hij : j ∈ {i_1 | ↑⟨i, ⋯⟩ ≤ ↑i_1}
hji : j ≠ ⟨i, hin⟩
⊢ m ≤ ↑j
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
H : IsUnit p
⊢ False

Tactic:
by
    simp [(MvPolynomial.isUnit_iff_totalDegree_of_isReduced.mp H).2] at hp

Goal state after:
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∀ x ∈ range (n + 1), (monomial (single x (p ^ (n - x)))) (↑p ^ x) = C (↑p ^ x) * X x ^ p ^ (n - x)

Tactic:
rintro i -

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ (monomial (single i (p ^ (n - i)))) (↑p ^ i) = C (↑p ^ i) * X i ^ p ^ (n - i)
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((⇑Polynomial.C ∘ ⇑MvPolynomial.C) (MvPolynomial.coeff v f)).leadingCoeff *
      ∏ i, ((MvPolynomial.finSuccEquiv k n) ((T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Tactic:
simp only [AlgEquiv.ofAlgHom_apply, Function.comp_apply, leadingCoeff_C, map_pow,
      leadingCoeff_pow, algebraMap_eq]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ MvPolynomial.C (MvPolynomial.coeff v f) *
      ∏ x, ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X x))).leadingCoeff ^ v x =
    MvPolynomial.C (MvPolynomial.coeff v f)
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittNeg p n) = 0

Tactic:
by
  apply constantCoeff_wittStructureInt p _ _ n
  simp only [neg_zero, map_neg, constantCoeff_X]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : 𝕎 R
n : ℕ
this : (aeval x.coeff) ((bind₁ (W_ R)) (xInTermsOfW p R n)) = (aeval x.coeff) (X n)
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x.ghostFun).coeff n = x.coeff n

Tactic:
simpa +unfoldPartialApp only [aeval_bind₁, aeval_X, ghostFun,
      aeval_wittPolynomial]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
hle : p ^ m ≤ j + 1
⊢ m ≤ n - i ∧ m ≤ j

Tactic:
exact ⟨(Nat.pow_le_pow_iff_right hp.1.one_lt).1 (hle.trans hj),
     Nat.le_of_lt_succ ((m.lt_pow_self hp.1.one_lt).trans_le hle)⟩

Goal state after:
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)

Tactic:
apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ ULift.ringEquiv.symm
      ((eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k)) =
    ULift.ringEquiv.symm
      ((eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k))
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∀ x_1 ∈ Finset.range (n + 1),
    ↑p ^ (x_1 + 1) * x.verschiebungFun.coeff (x_1 + 1) ^ p ^ (n + 1 - (x_1 + 1)) =
      ↑p * (↑p ^ x_1 * x.coeff x_1 ^ p ^ (n - x_1))

Tactic:
rintro i -

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n i : ℕ
⊢ ↑p ^ (i + 1) * x.verschiebungFun.coeff (i + 1) ^ p ^ (n + 1 - (i + 1)) = ↑p * (↑p ^ i * x.coeff i ^ p ^ (n - i))
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n.succ)) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n.succ - 1))

Tactic:
Nat.succ_eq_add_one,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n + 1 - 1))
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R : Type u
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ 0) (wittPolynomial p R n) = 0

Tactic:
by
  rw [← aeval_eq_bind₁, aeval_zero, constantCoeff_wittPolynomial, map_zero]

Goal state after:
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)

Tactic:
apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)
⊢ ULift.ringEquiv.symm
      ((eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k)) =
    ULift.ringEquiv.symm
      ((eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k))
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case neg
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
n : ℕ
hn : ¬P n
⊢ 0 = x.coeff n

Tactic:
· rw [(h n).resolve_right hn]

Goal state after:
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Tactic:
have hx : select P z = x := by
    ext1 n; rw [select, coeff_mk, coeff_mk]
    split_ifs with hn
    · rfl
    · rw [(h n).resolve_right hn]

Goal state after:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
⊢ (x + y).coeff n = x.coeff n + y.coeff n
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
⊢ (∀ i < n, x.coeff i = y.coeff i) ↔ (truncate n) x = (truncate n) y

Tactic:
refine ⟨fun h => ?_, fun h i hi => ?_⟩
    · ext i
      simp [h i]
    · rw [← coeff_truncate x ⟨i, hi⟩, ← coeff_truncate y ⟨i, hi⟩, h]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f 3 - map f ↑k = 3 - ↑k

Tactic:
Polynomial.map_natCast,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f 3 - ↑k = 3 - ↑k
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case zero
x : ℝ
⊢ Real.exp (-(x ^ 2 / 2)) = (aeval x) (hermite 0) * Real.exp (-(x ^ 2 / 2))

Tactic:
hermite_zero,

Goal state after:
case zero
x : ℝ
⊢ Real.exp (-(x ^ 2 / 2)) = (aeval x) (C 1) * Real.exp (-(x ^ 2 / 2))
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).leadingCoeff = (↑d !)⁻¹

Tactic:
leadingCoeff,

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).coeff (preHilbertPoly F d k).natDegree = (↑d !)⁻¹
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ eval (↑n) (preHilbertPoly F d k) = ↑((n - k + d).choose d)

Tactic:
have : (d ! : F) ≠ 0 := by norm_cast; positivity

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ eval (↑n) (preHilbertPoly F d k) = ↑((n - k + d).choose d)
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case inr
n k : ℕ
hnk : Even (n + k)
h_lt : n < k
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Tactic:
simp [Nat.choose_eq_zero_of_lt h_lt, coeff_hermite_of_lt h_lt]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ ((opRingEquiv R) p).leadingCoeff = op (unop p).leadingCoeff

Tactic:
leadingCoeff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ ((opRingEquiv R) p).coeff ((opRingEquiv R) p).natDegree = op (unop p).leadingCoeff
Module: Mathlib.RingTheory.PowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ IsRestricted c f ↔ Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)

Tactic:
rw [IsRestricted, MvPowerSeries.IsRestricted, isRestricted_comp_uniqueEquiv]

Goal state after:
R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ Tendsto ((fun n ↦ ‖(coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())) cofinite (𝓝 0) ↔
    Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ∑ k ∈ range n.succ, (coeff k) (X * largeSchroderSeries) * (coeff (n - k)) largeSchroderSeries =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
Nat.succ_eq_add_one,

Goal state after:
n : ℕ
hn : 0 < n
⊢ ∑ k ∈ range (n + 1), (coeff k) (X * largeSchroderSeries) * (coeff (n - k)) largeSchroderSeries =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ radical n = ∏ p ∈ n.primeFactors, p

Tactic:
by
  simp [radical, primeFactors_eq_natPrimeFactors]

Goal state after:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ f.toFun' (RingCon.ker ↑ψ).Quotient
      ((rTensor M ((↑(quotientKerEquivRangeₐ ψ).symm).comp ψ.rangeRestrict).toLinearMap) q) =
    f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q)

Tactic:
← quotientKerEquivRangeₐ_comp_mkₐ,

Goal state after:
R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ f.toFun' (RingCon.ker ↑ψ).Quotient
      ((rTensor M
          ((↑(quotientKerEquivRangeₐ ψ).symm).comp
              ((↑(quotientKerEquivRangeₐ ψ)).comp (mkₐ R (RingCon.ker ↑ψ)))).toLinearMap)
        q) =
    f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q)