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

Goal state before:
pp: case e'_4
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ Cardinal.toENat (Submodule.spanRank I) = ↑(Submodule.spanFinrank I)

Tactic:
simpa [Submodule.fg_iff_spanRank_eq_spanFinrank] using (IsNoetherian.noetherian I)

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ Ring.jacobson R
⊢ ringKrullDim (QuotSMulTop x R) + 1 = ringKrullDim R

Tactic:
by
  rw [← supportDim_quotient_eq_ringKrullDim, ← supportDim_self_eq_ringKrullDim]
  exact supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson reg
    ((annihilator R R).ringJacobson_le_jacobson hx)

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
⊢ ringKrullDim (R ⧸ ofList rs) + ↑rs.length = ringKrullDim R

Tactic:
have eq : ofList rs = ofList rs • (⊤ : Ideal R) := by simp

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
eq : ofList rs = ofList rs • ⊤
⊢ ringKrullDim (R ⧸ ofList rs) + ↑rs.length = ringKrullDim R
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case pos
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
a : ↥S
ha : (mkLinearMap S M) b = (mkLinearMap S M) (a • x)
c : ↥S
hc : c • b = c • a • x
hb : c • b ∈ q
⊢ x ∈ q

Tactic:
hc,

Goal state after:
case pos
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
hq : (q.colon Set.univ).radical = ↑p
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
a : ↥S
ha : (mkLinearMap S M) b = (mkLinearMap S M) (a • x)
c : ↥S
hc : c • b = c • a • x
hb : c • a • x ∈ q
⊢ x ∈ q
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
h✝ : InfIrred N
a : R
b : M
hab : a • b ∈ N
n : ℕ
x : R
y : M
h : y ∈ {x | a ^ n • x ∈ N}
⊢ x • y ∈ {x | a ^ n • x ∈ N}

Tactic:
by simp [smul_comm _ x, N.smul_mem x h]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
⊢ ∀ (I : Ideal Rₛ), Function.Surjective ⇑(LinearMap.lcomp Rₛ Mₛ (Submodule.subtype I))

Tactic:
intro Iₛ g

Goal state after:
R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
Iₛ : Ideal Rₛ
g : ↥Iₛ →ₗ[Rₛ] Mₛ
⊢ ∃ a, (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype Iₛ)) a = g
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
⊢ ((algebraMap R Rₛ) ↑a * IsLocalization.mk' Rₛ 1 a) •
      (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype)
        ((mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ) g') =
    (algebraMap R Rₛ) ↑a • g

Tactic:
algebraMap_smul,

Goal state after:
R : Type u
inst✝¹⁴ : CommRing R
M : Type v
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
S : Submonoid R
inst✝¹¹ : Small.{v, u} R
inst✝¹⁰ : IsNoetherianRing R
Rₛ : Type u'
inst✝⁹ : Small.{v', u'} Rₛ
inst✝⁸ : CommRing Rₛ
inst✝⁷ : Algebra R Rₛ
Mₛ : Type v'
inst✝⁶ : AddCommGroup Mₛ
inst✝⁵ : Module R Mₛ
inst✝⁴ : Module Rₛ Mₛ
inst✝³ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : IsLocalizedModule S f
inst✝ : Injective R M
MB : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  ↑a • g =
    (mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ)
      ((LinearMap.lcomp R M I.subtype) g', a).1
⊢ ((algebraMap R Rₛ) ↑a * IsLocalization.mk' Rₛ 1 a) •
      (LinearMap.lcomp Rₛ Mₛ (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I).subtype)
        ((mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ) g') =
    ↑a • g
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n

Tactic:
ofPowerSeries_apply,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ (embDomain Nat.castOrderEmbedding (HahnSeries.toPowerSeries.symm x.powerSeriesPart)).coeff (n - order x) = x.coeff n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.negSucc a✝) = if Int.negSucc a✝ < 0 then 0 else (coeff (Int.negSucc a✝).natAbs) f

Tactic:
ofPowerSeries_apply,

Goal state after:
case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ (embDomain Nat.castOrderEmbedding (HahnSeries.toPowerSeries.symm f)).coeff (Int.negSucc a✝) =
    if Int.negSucc a✝ < 0 then 0 else (coeff (Int.negSucc a✝).natAbs) f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
hDs : 0 < D + ↑s
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-(D + ↑s))

Tactic:
obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le hDs.le
        rw [hd]
        apply (intValuation_le_iff_coeff_lt_eq_zero K F).mpr
        intro n hn
        rw [powerSeriesPart_coeff f n, hs]
        apply h_val_f
        lia

Goal state after:
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✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝³ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝² : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
R₂ : Type u_2 := Localization.AtPrime P
this✝ : Algebra R₂ R₁ := algebraOfLiesOver P (Ideal.map (algebraMap S Sₚ) P)
this : IsLocalization.AtPrime R₁ P
h : Function.Bijective ⇑(algebraMap R₂ R₁)
⊢ Ideal.map (algebraMap R R₂) p =
    comap (algebraMap R₂ R₁) (Ideal.map (algebraMap Rₚ R₁) (Ideal.map (algebraMap R Rₚ) p))

Tactic:
p.map_map,

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✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝³ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝² : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
R₂ : Type u_2 := Localization.AtPrime P
this✝ : Algebra R₂ R₁ := algebraOfLiesOver P (Ideal.map (algebraMap S Sₚ) P)
this : IsLocalization.AtPrime R₁ P
h : Function.Bijective ⇑(algebraMap R₂ R₁)
⊢ Ideal.map (algebraMap R R₂) p = comap (algebraMap R₂ R₁) (Ideal.map ((algebraMap Rₚ R₁).comp (algebraMap R Rₚ)) p)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

Tactic:
by
  by_cases! h_neg : 1 < η
  · use 0
    simpa using (intValuation_le_one (PowerSeries.idealX K) F).trans_lt h_neg
  · rw [← Units.val_le_val, Units.val_one, ← WithZero.coe_one, ← coe_unzero η.ne_zero,
      coe_le_coe, ← Multiplicative.toAdd_le, toAdd_one] at h_neg
    obtain ⟨d, hd⟩ := Int.exists_eq_neg_ofNat h_neg
    use F.trunc (d + 1)
    have : Valued.v ((ofPowerSeries ℤ K) (F - (trunc (d + 1) F))) ≤
      (Multiplicative.ofAdd (-(d + 1 : ℤ))) := by
      apply (intValuation_le_iff_coeff_lt_eq_zero K _).mpr
      simpa only [map_sub, sub_eq_zero, Polynomial.coeff_coe, coeff_trunc] using
        fun _ h ↦ (if_pos h).symm
    rw [neg_add, ofAdd_add, ← hd, ofAdd_toAdd, WithZero.coe_mul, coe_unzero,
      ← coe_algebraMap] at this
    rw [← valuation_of_algebraMap (K := K⸨X⸩) (PowerSeries.idealX K) (F - F.trunc (d + 1))]
    apply lt_of_le_of_lt this
    rw [← mul_one (η : ℤᵐ⁰), mul_assoc, one_mul]
    gcongr
    · exact zero_lt_iff.2 η.ne_zero
    rw [← WithZero.coe_one, coe_lt_coe, ofAdd_neg, Right.inv_lt_one_iff, ← ofAdd_zero,
      Multiplicative.ofAdd_lt]
    exact Int.zero_lt_one

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

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ #t.1) +
      (∏ a ∈ t.1, X a) * (X t.2 * X t.2 ^ (k - (#t.1 + 1)) * (-1) ^ (#t.1 + 1)) =
    0

Tactic:
nth_rewrite 2 [← pow_one (X t.snd)]

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ #t.1) +
      (∏ a ∈ t.1, X a) * (X t.2 ^ 1 * X t.2 ^ (k - (#t.1 + 1)) * (-1) ^ (#t.1 + 1)) =
    0
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
this : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ := Finsupp.mapRange (fun n ↦ n / p) ⋯ d
hd : (coeff m) φ ≠ 0
eq_aux : p • m = d
⊢ d ∈ (fun x ↦ p • x) '' Function.support φ

Tactic:
coeff_apply

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
d : σ →₀ ℕ
this : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ := Finsupp.mapRange (fun n ↦ n / p) ⋯ d
hd : φ m ≠ 0
eq_aux : p • m = d
⊢ d ∈ (fun x ↦ p • x) '' Function.support φ
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg.a
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd₁ : (coeff d) φ ≠ 0
hd₂ : ↑(Finsupp.degree d) = φ.order
this : p • φ.order = ↑(Finsupp.degree (p • d))
⊢ ((expand p hp) φ).order ≤ ↑(Finsupp.degree (p • d))

Tactic:
exact order_le <| (coeff_expand_smul p hp φ _) ▸ hd₁

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
f g : M → S
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
⊢ Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)

Tactic:
by
  wlog hC' : 0 ≤ C generalizing C
  · rw [tendsto_zero_iff_norm_tendsto_zero]
    simpa using this (C := |C|) (by simp [hC]) (by simpa using hf.norm)
      (by simpa using hg.norm) (fun _ => by simp)
  refine .squeeze tendsto_const_nhds
    (tendsto_sup'_antidiagonal_cofinite (tendsto_mul_cofinite_nhds_zero hf hg))
    (fun x ↦ mul_nonneg (by simp) (hC' x)) fun a ↦ ?_
  have : 0 ≤ C a := hC' a
  grw [(nonempty_antidiagonal _).norm_sum_le_sup'_norm, Finset.sup'_mul₀ this]
  refine Finset.sup'_mono_fun fun x hx ↦ ?_
  grw [mul_mul_mul_comm, ← hC, Finset.mem_antidiagonal.mp hx, ← norm_mul_le]

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ (m • x).coeff n = peval (wittNSMul p m n) ![x.coeff]

Tactic:
by
  simp [(· • ·), SMul.smul, eval, Matrix.cons_fin_one]

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℤ
x : 𝕎 R
n : ℕ
⊢ (m • x).coeff n = peval (wittZSMul p m n) ![x.coeff]

Tactic:
by
  simp [(· • ·), SMul.smul, eval, Matrix.cons_fin_one]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: p : ℕ
inst✝¹¹ : Fact (Nat.Prime p)
R : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CharP R p
P✝ : Type u₃
inst✝⁸ : CommSemiring P✝
inst✝⁷ : CharP P✝ p
inst✝⁶ : PerfectRing P✝ p
inst✝⁵ : PerfectRing R p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* S
⊢ (π.comp ↑m.equiv.symm).comp ((Perfection.lift p R S) f) = f

Tactic:
comp_symm_equiv'

Goal state after:
p : ℕ
inst✝¹¹ : Fact (Nat.Prime p)
R : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CharP R p
P✝ : Type u₃
inst✝⁸ : CommSemiring P✝
inst✝⁷ : CharP P✝ p
inst✝⁶ : PerfectRing P✝ p
inst✝⁵ : PerfectRing R p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* S
⊢ (Perfection.coeff S p 0).comp ((Perfection.lift p R S) f) = f
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
hp : Nat.Prime p
this : Nontrivial (PreTilt O p)
a✝ b✝ : PreTilt O p
hfg : (val K v O hv p) a✝ ≠ 0 ∧ (val K v O hv p) b✝ ≠ 0
⊢ (val K v O hv p) (a✝ * b✝) ≠ 0

Tactic:
rw [Valuation.map_mul]

Goal state after:
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
hp : Nat.Prime p
this : Nontrivial (PreTilt O p)
a✝ b✝ : PreTilt O p
hfg : (val K v O hv p) a✝ ≠ 0 ∧ (val K v O hv p) b✝ ≠ 0
⊢ (val K v O hv p) a✝ * (val K v O hv p) b✝ ≠ 0
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: case insert
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
hind :
  (∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}) →
    ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n : ℕ
⊢ (∑ s ∈ insert a S', x s).coeff n = ∑ s ∈ insert a S', (x s).coeff n

Tactic:
have : (∀ (n : ℕ), Subsingleton {r | r ∈ S' ∧ (x r).coeff n ≠ 0}) := by
      refine fun n ↦ ⟨fun b c ↦ ?_⟩
      ext
      exact congrArg (fun x ↦ x.1) <|
          (h n).allEq ⟨b.1, S'.subset_insert a b.2.1, b.2.2⟩ ⟨c.1, S'.subset_insert a c.2.1, c.2.2⟩
    replace hind := hind this
    simp only [ha, not_false_eq_true, Finset.sum_insert]
    have : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0 := by
      simp only [hind]
      by_contra! ⟨m, hma, hmS'⟩
      have := Finset.sum_eq_zero.mt hmS'
      push Not at this
      choose b hb hb' using this
      have : a = b :=
        congrArg (fun x ↦ x.1) <|
          (h m).allEq ⟨a, S'.mem_insert_self a, hma⟩ ⟨b, S'.mem_insert_of_mem hb, hb'⟩
      exact ha (this ▸ hb)
    rw [coeff_add_of_disjoint n _ _ this, hind n]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ dickson 2 1 1 = Chebyshev.S R ↑1

Tactic:
rw [dickson_one, Nat.cast_one, Chebyshev.S_one]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ ((q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p).hilbertPoly d).natDegree =
    d - rootMultiplicity 1 p - 1

Tactic:
← Nat.sub_add_cancel (le_of_lt hpd),

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
⊢ ((q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p).hilbertPoly
        (d - rootMultiplicity 1 p + rootMultiplicity 1 p)).natDegree =
    d - rootMultiplicity 1 p - 1
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
trinomial_mirror zero_lt_one hn (-1 : ℤˣ).ne_zero (1 : ℤˣ).ne_zero

Goal state after:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : (aeval z) (trinomial 0 (n - 1 + 0) n ↑1 ↑(-1) ↑(-1)) = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
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ₐ φ))
⊢ (rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (rTensor N ψ.toLinearMap) (f.toFun' B q)

Tactic:
have ht : (h.comp φ.range.val).comp (quotientKerEquivRangeₐ φ).toAlgHom =
      ψ.range.val.comp ((quotientKerEquivRangeₐ ψ).toAlgHom.comp θ) := by
    simp only [θ, ← AlgHom.comp_assoc, ← hh']
    simp [AlgHom.comp_assoc]

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 θ)
⊢ (rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (rTensor N ψ.toLinearMap) (f.toFun' B q)