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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 + -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ a ≡ a₀ [SMOD I]

Tactic:
← add_zero a₀

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 + -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ a ≡ a₀ + 0 [SMOD I]
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
U : Set ↑(limit P.diagram).toProfinite.toTop
s : Set ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux P.diagram
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ : (a : OpenNormalSubgroup ↑P.toProfinite.toTop) → Set ↑(P.diagram.obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
⊢ IsOpen (⋂ i, ↑↑(↑i).toOpenSubgroup)

Tactic:
exact isOpen_iInter_of_finite fun i => i.1.1.isOpen'

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
x : R
hx : (Quotient.mk I) x ∈ ↑p'
⊢ (Quotient.mk I) x ∈ ⇑(Quotient.mk I) '' ↑p

Tactic:
exact ⟨x, by simpa [hrp, sup_of_le_left, p'] using hx⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case e'_4.e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := ⋯
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := ⋯
e_2✝ : Quotient.commSemiring I = CommRing.toCommSemiring
⊢ map (Quotient.mk I) (span ↑o) = span ↑s

Tactic:
simp [Ideal.map_span, ← himgo]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀✝ : p₀ < p₁
h₁✝ : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o ↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm : closedPoint (Localization.AtPrime p₂.asIdeal) = e.symm ⟨p₂, ⋯⟩
q : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)
hxq : (algebraMap R (Localization.AtPrime p₂.asIdeal)) x ∈ (e.symm (e q)).asIdeal
h₀ : e.symm ⟨p₀, ⋯⟩ < e.symm (e q)
h₁ : (e.symm (e q)).asIdeal < maximalIdeal (Localization.AtPrime p₂.asIdeal)
h : e.symm (e q) < e.symm ⟨p₂, ⋯⟩
⊢ ↑(e q) < p₂

Tactic:
rwa [OrderIso.lt_iff_lt, Subtype.mk_lt_mk] at h

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case e'_3
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := ⋯
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this✝ : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := ⋯
this : span ↑t = map (algebraMap R S) (span ↑s) ⊔ span ↑o
e_2✝ : Quotient.commSemiring (map (algebraMap R S) p) = CommRing.toCommSemiring
⊢ map (Quotient.mk (map (algebraMap R S) p)) (span ↑o) = span ↑s'

Tactic:
simp [Ideal.map_span, ← himgo]

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case neg
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
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
⊢ (mkLinearMap S M).range ≤ localized₀ S (mkLinearMap S M) q

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
case neg
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
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
x : M
⊢ (mkLinearMap S M) x ∈ localized₀ S (mkLinearMap S M) q
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.h
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
⊢ ⟨y, hy⟩ ∈ Subring.center ↥R

Tactic:
let R_dr : DivisionRing R := Fintype.divisionRingOfIsDomain R

Goal state after:
case intro.h
n : ℕ
IH : ∀ m < n, ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D), card D = m → Subring.center D = ⊤
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
val✝ : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ ⟨y, hy⟩ ∈ Subring.center ↥R
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
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
S_exact : S.ShortExact
Sp : (m : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization m.asIdeal.primeCompl)) :=
  fun m ↦ S.map (localizedModuleFunctor m.asIdeal.primeCompl)
⊢ HasInjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)

Tactic:
have Sp_exact (m : MaximalSpectrum R) : (Sp m).ShortExact :=
      S_exact.map_of_exact (ModuleCat.localizedModuleFunctor m.1.primeCompl)

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
S_exact : S.ShortExact
Sp : (m : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization m.asIdeal.primeCompl)) :=
  fun m ↦ S.map (localizedModuleFunctor m.asIdeal.primeCompl)
Sp_exact : ∀ (m : MaximalSpectrum R), (Sp m).ShortExact
⊢ HasInjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
⊢ injectiveDimension M = ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl)

Tactic:
by
  have aux (n : ℕ) : injectiveDimension M ≤ n ↔ ⨆ (m : MaximalSpectrum R), injectiveDimension
    (M.localizedModule m.1.primeCompl) ≤ n := by
    simp only [injectiveDimension_le_iff, iSup_le_iff]
    exact M.hasInjectiveDimensionLE_iff_forall_maximalSpectrum n
  refine eq_of_forall_ge_iff (fun N ↦ ?_)
  induction N with
  | bot =>
    simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp⟩
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
⊢ ∃ m ∈ M, n ∣ m

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
this : Fintype ι
⊢ ∃ m ∈ M, n ∣ m
Module: Mathlib.RingTheory.Localization.Pi

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst✝⁵ : (i : ι) → CommSemiring (R i)
inst✝⁴ : (i : ι) → CommSemiring (S i)
inst✝³ : (i : ι) → Algebra (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst✝² : ∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)
inst✝¹ : ∀ (i : ι), Ring.KrullDimLE 0 (R i)
inst✝ : ∀ (i : ι), IsLocalRing (R i)
⊢ Surjective ⇑(RingHom.pi fun i ↦ (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i))

Tactic:
apply Surjective.piMap (fun i ↦ ?_)
  by_cases h₀ : (0 : R i) ∈ (M.map (Pi.evalRingHom R i))
  · have := uniqueOfZeroMem h₀ (S := (S i))
    exact surjective_to_subsingleton (algebraMap (R i) (S i))
  · exact (IsLocalization.atUnits _ _ (by simpa)).surjective

Goal state after:
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 : 0 < HahnSeries.order f
⊢ Valued.v f ≤ exp (-D)

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat <| neg_nonpos_of_nonneg ord_nonpos.le
    rw [neg_inj] at hs
    rw [← f.single_order_mul_powerSeriesPart, hs, map_mul, valuation_single_zpow, mul_comm,
      ← le_mul_inv_iff₀, ← exp_neg, ← exp_add, neg_neg]
    · by_cases! hDs : D - s ≤ 0
      · apply le_trans ((PowerSeries.idealX K).valuation_le_one F)
        rw [← log_le_iff_le_exp one_ne_zero, log_one]
        lia
      · obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le hDs.le
        rw [← neg_neg (-D + ↑s), ← sub_eq_neg_add, neg_sub, 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 (s + n)
        lia
    · simp [ne_eq, zero_lt_iff]

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

Goal state before:
pp: n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
⊢ Irreducible (f * X i + g)

Tactic:
let S := MvPolynomial { j // j ≠ i } R

Goal state after:
n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : MvPolynomial n R
i : n
hf0 : f ≠ 0
hif : i ∉ f.vars
hig : i ∉ g.vars
h : IsRelPrime f g
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
⊢ Irreducible (f * X i + g)
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i : n
⊢ coeff (Finsupp.single i 1) (c.sum fun i a ↦ a • X i) = c i

Tactic:
Finsupp.sum,

Goal state after:
n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i : n
⊢ coeff (Finsupp.single i 1) (∑ a ∈ c.support, c a • X a) = c i
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
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)) ⋯
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

Tactic:
obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt F (η * γ)

Goal state after:
case pos
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) < ↑(η * γ)
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ pairMap σ (pairMap σ t) = t

Tactic:
pairMap,

Goal state after:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h : (pairMap σ t).2 ∈ (pairMap σ t).1 then ((pairMap σ t).1.erase (pairMap σ t).2, (pairMap σ t).2)
    else (cons (pairMap σ t).2 (pairMap σ t).1 h, (pairMap σ t).2)) =
    t
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, weight σ R k (A, j) =
    ∑ t ∈ pairs σ k with #t.1 < k, weight σ R k t

Tactic:
sum_filter_pairs_eq_sum_filter_antidiagonal_powersetCard_sum σ R k

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, weight σ R k (A, j) =
    ∑ a ∈ antidiagonal k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j, weight σ R k (A, j)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : 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
⊢ ¬p • m ≤ p • n

Tactic:
obtain ⟨i, hi⟩ : ∃ i, m i > n i := by
          by_contra! hc
          exact h_le (Finsupp.coe_le_coe.mp hc)

Goal state after:
σ : 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
i : σ
hi : m i > n i
⊢ ¬p • m ≤ p • n
Module: Mathlib.RingTheory.Nilpotent.GeometricallyReduced

Goal state before:
pp: k : Type u_3
A : Type u_4
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
e : (p : Ideal k) → [inst : p.IsPrime] → AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
  fun p [p.IsPrime] ↦
    have this := ⋯;
    IsAlgClosure.equiv k (AlgebraicClosure k) (AlgebraicClosure p.ResidueField)
⊢ IsGeometricallyReduced k A ↔ IsReduced (AlgebraicClosure k ⊗[k] A)

Tactic:
refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨fun p hp ↦ ?_⟩⟩

Goal state after:
case refine_1
k : Type u_3
A : Type u_4
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
e : (p : Ideal k) → [inst : p.IsPrime] → AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
  fun p [p.IsPrime] ↦
    have this := ⋯;
    IsAlgClosure.equiv k (AlgebraicClosure k) (AlgebraicClosure p.ResidueField)
x✝ : IsGeometricallyReduced k A
h : ∀ (p : Ideal k) [inst : p.IsPrime], IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)
⊢ IsReduced (AlgebraicClosure k ⊗[k] A)

case refine_2
k : Type u_3
A : Type u_4
inst✝² : Field k
inst✝¹ : Ring A
inst✝ : Algebra k A
e : (p : Ideal k) → [inst : p.IsPrime] → AlgebraicClosure k ≃ₐ[k] AlgebraicClosure p.ResidueField :=
  fun p [p.IsPrime] ↦
    have this := ⋯;
    IsAlgClosure.equiv k (AlgebraicClosure k) (AlgebraicClosure p.ResidueField)
h : IsReduced (AlgebraicClosure k ⊗[k] A)
p : Ideal k
hp : p.IsPrime
⊢ IsReduced (AlgebraicClosure p.ResidueField ⊗[k] A)
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
a : M
this : 0 ≤ C a
⊢ ‖∑ 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)

Tactic:
(nonempty_antidiagonal _).norm_sum_le_sup'_norm,

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
this : 0 ≤ C a
⊢ ((antidiagonal a).sup' ⋯ fun x ↦ ‖f x.1 * g x.2‖) * C a ≤
    (antidiagonal a).sup' ⋯ fun i ↦ ‖f i.1‖ * C i.1 * (‖g i.2‖ * C i.2)
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
σ : Type u_2
inst✝ : IsUltrametricDist R
c : σ → ℝ
f g : MvPowerSeries σ R
hf : IsRestricted c f
hg : IsRestricted c g
⊢ IsRestricted c (f * g)

Tactic:
rw [← isRestricted_abs_iff, IsRestricted] at *
  exact tendsto_antidiagonal (by simp [Finsupp.prod_add_index', pow_add]) hf hg

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : Field K
a : K
⊢ (powerSeriesRingEquiv K) ((algebraMap K K⟦X⟧) a) = (algebraMap K ↥(adicCompletionIntegers K⟮X⟯ (idealX K))) a

Tactic:
PowerSeries.algebraMap_eq,

Goal state after:
R : Type u_1
K : Type u_2
inst✝ : Field K
a : K
⊢ (powerSeriesRingEquiv K) (PowerSeries.C a) = (algebraMap K ↥(adicCompletionIntegers K⟮X⟯ (idealX K))) a
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ constantCoeff (xInTermsOfW p R n) = 0

Tactic:
xInTermsOfW_eq,

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ constantCoeff ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * C (⅟↑p ^ n)) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
⊢ xInTermsOfW p R 0 = X 0

Tactic:
xInTermsOfW_eq,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
⊢ (X 0 - ∑ i ∈ range 0, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (0 - i)) * C (⅟↑p ^ 0) = X 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ range (n + 1)

Tactic:
xInTermsOfW_eq,

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ n ∈ ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n)).vars ∧
    ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n)).vars ⊆ range (n + 1)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun i ↦ (expand p) ((rename (Prod.mk i)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) =
    (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ (bind₁ fun i ↦ (expand p) ((rename fun i_1 ↦ (i, i_1)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) =
    (bind₁ fun i ↦ (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)

Tactic:
rw [key]

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun i ↦ (expand p) ((rename (Prod.mk i)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) =
    (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    (bind₁ fun i ↦ (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ xInTermsOfW p R n * C (↑p ^ n) = X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)

Tactic:
xInTermsOfW_eq,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * C (⅟↑p ^ n) * C (↑p ^ n) =
    X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (bind₁ (W_ R)) (xInTermsOfW p R n) = X n

Tactic:
xInTermsOfW_eq,

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (bind₁ (W_ R)) ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * C (⅟↑p ^ n)) = X n
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ (x + y).ghostFun = x.ghostFun + y.ghostFun

Tactic:
by
  ghost_fun_tac X 0 + X 1, ![x.coeff, y.coeff]

Goal state after: