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

Goal state before:
pp: case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasInjectiveDimensionLE M (n + 1)
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
T : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
T_exact : T.ShortExact
T_exact' : Function.Exact ⇑(ConcreteCategory.hom T.f) ⇑(ConcreteCategory.hom T.g)
TS_exact' :
  Function.Exact
    ⇑((IsLocalizedModule.map S (T.X₁.localizedModuleMkLinearMap S) (T.X₂.localizedModuleMkLinearMap S))
        (ConcreteCategory.hom T.f))
    ⇑((IsLocalizedModule.map S (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S))
        (ConcreteCategory.hom T.g))
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
let TS := T.map (ModuleCat.localizedModuleFunctor S)

Goal state after:
case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasInjectiveDimensionLE M (n + 1)
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
T : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
T_exact : T.ShortExact
T_exact' : Function.Exact ⇑(ConcreteCategory.hom T.f) ⇑(ConcreteCategory.hom T.g)
TS_exact' :
  Function.Exact
    ⇑((IsLocalizedModule.map S (T.X₁.localizedModuleMkLinearMap S) (T.X₂.localizedModuleMkLinearMap S))
        (ConcreteCategory.hom T.f))
    ⇑((IsLocalizedModule.map S (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S))
        (ConcreteCategory.hom T.g))
TS : ShortComplex (ModuleCat (Localization S)) := T.map (localizedModuleFunctor S)
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat R
projective✝ : Projective P
f : P ⟶ M
epi✝ : Epi f
T : ShortComplex (ModuleCat R) := { X₁ := kernel f, X₂ := P, X₃ := M, f := kernel.ι f, g := f, zero := ⋯ }
T_exact : T.ShortExact
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
let TS := T.map (ModuleCat.localizedModuleFunctor S)

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization S)
n : ℕ
ih : ∀ (M : ModuleCat R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat R
inst✝ : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat R
projective✝ : Projective P
f : P ⟶ M
epi✝ : Epi f
T : ShortComplex (ModuleCat R) := { X₁ := kernel f, X₂ := P, X₃ := M, f := kernel.ι f, g := f, zero := ⋯ }
T_exact : T.ShortExact
TS : ShortComplex (ModuleCat (Localization S)) := T.map (localizedModuleFunctor S)
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case neg.convert_10
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
hi : ¬m i = 0
⊢ (weight w) (m - single i 1) + w i = n

Tactic:
← hm,

Goal state after:
case neg.convert_10
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
hi : ¬m i = 0
⊢ (weight w) (m - single i 1) + w i = (weight w) m
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
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P
⊢ ∃ a, (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) a = x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (algebraMapSubmonoid S p.primeCompl) x
  obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := P) (Ideal.Quotient.mk P s)⁻¹
  simp only [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), Quotient.algebraMap_eq, RingHom.comp_apply]
  use x * s'
  rw [← sub_eq_zero, ← map_sub, Quotient.eq_zero_iff_mem]
  have h₀ : (P.map (algebraMap S Sₚ)).IsPrime := isPrime_map_of_liesOver S p Sₚ P
  have h₁ : s.1 ∉ P := (Set.disjoint_left.mp <| disjoint_primeCompl_of_liesOver P p) s.prop
  have h₂ : algebraMap S Sₚ s ∉ Ideal.map (algebraMap S Sₚ) P := by
    rwa [← mem_comap, comap_map_eq_self_of_isMaximal _ h₀.ne_top]
  refine (h₀.mem_or_mem ?_).resolve_left h₂
  rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case left
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
this : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < ⋯.choose, coeff hℱ d = f.coeff d
⊢ ⋂ n, ⋂ (_ : n < ℓ), φ n ∈ ℱ

Tactic:
rw [Filter.eventually_iff] at this

Goal state after:
case left
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun d ↦ {f | coeff hℱ d = f.coeff d}
intersec₁ : ⋂ n ∈ Set.Iio D, φ n ⊆ {x | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose
N : ℤ := max ℓ D
intersec₂ : ⋂ n ∈ Set.Iio D, φ n ⊇ (⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n
this : {x | ∀ d < ⋯.choose, coeff hℱ d = x.coeff d} ∈ ℱ
⊢ ⋂ n, ⋂ (_ : n < ℓ), φ n ∈ ℱ
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
a b : MvPolynomial n R
hab : p = a * b
hle : a.totalDegree ≤ b.totalDegree
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Goal state after:
case inl
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
b : MvPolynomial n R
hab : p = 0 * b
hle : totalDegree 0 ≤ b.totalDegree
⊢ IsUnit 0 ∨ IsUnit b

case inr
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
a b : MvPolynomial n R
hab : p = a * b
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2.ht
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
j : Fin n
hj : m ≤ ↑j
⊢ (0 - if hi : ↑j + 1 < m then s ⟨↑j + 1, hi⟩ else 0) = 0

Tactic:
Nat.zero_sub

Goal state after:
case refine_2.ht
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝ : Fin m
i : ℕ
this✝ : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
j : Fin n
hj : m ≤ ↑j
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hp
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ (sumSMulX c).totalDegree = 1

pp: case hp'
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i (sumSMulX c)) → IsUnit x

Tactic:
· apply le_antisymm
    · simp only [sumSMulX, Finsupp.linearCombination_apply, Finsupp.sum]
      apply totalDegree_finsetSum_le
      intros
      apply le_trans (totalDegree_smul_le ..)
      simp
    · rw [← not_lt, Nat.lt_one_iff, totalDegree_eq_zero_iff]
      intro h
      obtain ⟨i, hi⟩ := hc_nonempty
      simp only [Finsupp.mem_support_iff] at hi
      specialize h (Finsupp.single i 1) (by
        rwa [mem_support_iff, coeff_sumSMulX]) i
      simp only [Finsupp.single_eq_same, one_ne_zero] at h

Goal state after:
case hp'
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i (sumSMulX c)) → IsUnit x
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

Tactic:
have : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1 := by exact algebraMap.coe_one

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
this : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
m : ℕ
inst✝ : CommSemiring R
i : ℕ
him : i ≤ m
⊢ Monic (⇑toLex) (esymm (Fin m) R i)

Tactic:
by
  cases i with
  | zero =>
    rw [esymm_zero]
    exact monic_one toLex.injective
  | succ i =>
    nontriviality R
    exact (supDegree_monic_esymm him).2

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case isPrimitive
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
r : R
hr : ∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d (sumSMulXSMulY c)
i : n
⊢ r ∣ c i

Tactic:
simpa [hcoeff] using hr (ι i)

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

Goal state before:
pp: case add_single.hq
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst✝ : Nontrivial R
i : Fin n
b✝ : ℕ
f✝ : Fin n →₀ ℕ
a✝¹ : i ∉ f✝.support
a✝ : b✝ ≠ 0
ih : ⇑(ofLex (supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) f✝ r))) = (accumulate n m) ⇑f✝
this : ↑i < m
⊢ Monic (⇑toLex) (esymm (Fin m) R (↑i + 1) ^ b✝)

Tactic:
exact (monic_esymm this).pow toLex_add toLex.injective

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

Goal state before:
pp: case right.inr.ind.inr.refine_2
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
hne : p ≠ esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
this : supDegree (⇑toLex) (p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) < supDegree (⇑toLex) p
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

Tactic:
specialize ih _ this _ (Subalgebra.sub_mem _ hp <| isSymmetric_esymmAlgHomMonomial _ _) _ rfl

Goal state after:
case right.inr.ind.inr.refine_2
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
hne : p ≠ esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
this : supDegree (⇑toLex) (p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) < supDegree (⇑toLex) p
⊢ p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p) ≠ 0

case right.inr.ind.inr.refine_2
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
ih : ⟨p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p), ⋯⟩ ∈ (esymmAlgHom (Fin n) R n).range
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
hne : p ≠ esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
this : supDegree (⇑toLex) (p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) < supDegree (⇑toLex) p
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := ⋯
X_def : X = {f | Valued.v f < embedding ↑d}
x : K⟮X⟯
hx : (restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x = ↑d
⊢ {y | Valued.v y < embedding ↑(Units.mk0 (Valued.v.restrict ((algebraMap K⟮X⟯ K⸨X⸩) x)) ⋯)} ⊆ X

Tactic:
simp only [Units.val_mk0, ← Valuation.restrict_lt_iff_lt_embedding,
          X_def, Set.ofPred_subset_ofPred, Valuation.restrict_lt_iff]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < embedding ↑d}
X_def : X = {f | Valued.v f < embedding ↑d}
x : K⟮X⟯
hx : (restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x = ↑d
⊢ ∀ (a : K⸨X⸩), Valued.v a < Valued.v ((algebraMap K⟮X⟯ K⸨X⸩) x) → Valued.v a < embedding ↑d
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
⊢ (coeff d) ((expand p hp) φ) = 0

Tactic:
← hm,

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
⊢ (coeff (p • m)) ((expand p hp) φ) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
m : σ →₀ ℕ
hm : p • m = n
⊢ (coeff n) ((expand p hp) ↑φ) = MvPolynomial.coeff n ((MvPolynomial.expand p) φ)

Tactic:
← hm,

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
m : σ →₀ ℕ
hm : p • m = n
⊢ (coeff (p • m)) ((expand p hp) ↑φ) = MvPolynomial.coeff (p • m) ((MvPolynomial.expand p) φ)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
⊢ (coeff n) ((expand p hp) ↑φ) = MvPolynomial.coeff n ((MvPolynomial.expand p) φ)

Tactic:
obtain ⟨m, hm⟩ : ∃ m, p • m = n := ⟨n.mapRange (fun a ↦ a / p) (by simp),
      by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
    rw [← hm, coeff_expand_smul p hp _ _, φ.coeff_expand_smul _ hp, φ.coeff_coe]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : m ≤ n
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
← hm,

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : m ≤ n
⊢ MvPolynomial.coeff (p • m) ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff (p • m) ((MvPolynomial.expand p) ((trunc' R n) φ))
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
not_le : ¬p • m ≤ p • n
⊢ (if d ≤ p • n then (coeff d) ((expand p hp) φ) else 0) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
← hm,

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
not_le : ¬p • m ≤ p • n
⊢ (if p • m ≤ p • n then (coeff (p • m)) ((expand p hp) φ) else 0) =
    MvPolynomial.coeff (p • m) ((MvPolynomial.expand p) ((trunc' R n) φ))
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
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
⊢ Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)

Tactic:
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 ↦ ?_

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ (T1 f c).comp (T1 f (-c)) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)

Tactic:
comp_aeval,

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ (MvPolynomial.aeval fun i ↦
      (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i)) =
    AlgHom.id k (MvPolynomial (Fin (n + 1)) k)
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff

Tactic:
simp only [map_add, map_sum]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) (h v)) +
        ∑ x ∈ f.support \ {v}, (MvPolynomial.finSuccEquiv k n) ((T f) (h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* Perfection N p
m : M
n : ℕ
⊢ (coeffMonoidHom N p n)
      (((fun f ↦ { toFun := fun r ↦ ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ })
          ((coeffMonoidHom N p 0).comp f))
        m) =
    (coeffMonoidHom N p n) (f m)

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.coe_mk, OneHom.coe_mk,
      coeffMonoidHom_mk]

Goal state after:
M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* Perfection N p
m : M
n : ℕ
⊢ (coeffMonoidHom N p 0) (f ((powMulEquiv M (p ^ n)).symm m)) = (coeffMonoidHom N p n) (f m)
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
⊢ (↑p).coeff i = if i = 1 then 1 else 0

Tactic:
by
  split_ifs with hi
  · simpa only [hi, pow_one] using coeff_p_pow p R 1
  · simpa only [pow_one] using coeff_p_pow_eq_zero p R hi

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝
⊢ ((⇑verschiebung)^[k + 1] x).coeff (k✝ + (k + 1)) = x.coeff k✝

Tactic:
rw [iterate_succ_apply', Nat.add_succ, verschiebung_coeff_succ]; exact ih

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n) = X n ^ p

Tactic:
by
  rw [frobeniusPoly, map_add, map_pow, map_mul, map_X, map_C]
  simp only [Int.cast_natCast, add_zero, eq_intCast, ZMod.natCast_self, zero_mul, C_0]

Goal state after: