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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
f : R[X]
hf : f.Monic
a₀ : R
h₂ : IsUnit (Polynomial.eval a₀ (derivative f))
H :
  (residue R) (Polynomial.eval a₀ f) = 0 →
    (residue R) (Polynomial.eval a₀ (derivative f)) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = (residue R) a₀
h₁ : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ f) = 0
aux : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f)) = 0 → False
a : R
ha₁ : f.IsRoot a
ha₂ : (residue R) a - (residue R) a₀ = 0
⊢ (Ideal.Quotient.mk (maximalIdeal R)) (a - a₀) = 0

Tactic:
← map_sub

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
f : R[X]
hf : f.Monic
a₀ : R
h₂ : IsUnit (Polynomial.eval a₀ (derivative f))
H :
  (residue R) (Polynomial.eval a₀ f) = 0 →
    (residue R) (Polynomial.eval a₀ (derivative f)) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = (residue R) a₀
h₁ : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ f) = 0
aux : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f)) = 0 → False
a : R
ha₁ : f.IsRoot a
ha₂ : (residue R) (a - a₀) = 0
⊢ (Ideal.Quotient.mk (maximalIdeal R)) (a - a₀) = 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
oinv : Γ
hxo : oinv + x.order = 0
⊢ 1 - ((single oinv) r * y + (single (oinv + x.order)) (r * x.leadingCoeff)) = -((single oinv) r * y)

Tactic:
hr,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
oinv : Γ
hxo : oinv + x.order = 0
⊢ 1 - ((single oinv) r * y + (single (oinv + x.order)) 1) = -((single oinv) r * y)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ (single 0) (r * x.leadingCoeff) = 1

Tactic:
hr,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := x - (single x.order) x.leadingCoeff
hy : y = 0
⊢ (single 0) 1 = 1
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
⊢ IsUnit x

Tactic:
by
  obtain _ | _ := subsingleton_or_nontrivial R
  · exact isUnit_of_subsingleton x
  · refine isUnit_of_isUnit_leadingCoeff_AddUnitOrder ?_ ?_
    · rw [(x.orderTop_self_sub_one_pos_iff.mp h).2]
      exact isUnit_one
    · have := (x.orderTop_self_sub_one_pos_iff.mp h).1
      rw [← order_eq_orderTop_of_ne_zero
        (fun h ↦ WithTop.top_ne_zero (orderTop_eq_top.mpr h ▸ this)), WithTop.coe_eq_zero] at this
      rw [this]
      exact isAddUnit_zero

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ.refine_1
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')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k ∈ Finset.range 2, ((taylor (c n)) f).coeff k * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
    I ^ (n + 1 + 1)

Tactic:
rw [← one_add_one_eq_two, Finset.sum_range_succ, Finset.range_one, Finset.sum_singleton,
            taylor_coeff_zero, taylor_coeff_one, pow_zero, pow_one, mul_one, mul_neg,
            mul_left_comm, Ring.mul_inverse_cancel _ (hf'c n), mul_one, add_neg_cancel]
          exact Ideal.zero_mem _

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
⊢ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) ≤ I

pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
⊢ x ∈ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal))

Tactic:
· rw [Pi.ker_ringHom]
    refine le_trans ?_ I.iInf_ker_le
    simp only [le_iInf_iff]
    exact fun i hi hle ↦ iInf_le_of_le ⟨⟨i, hi⟩, hle⟩ le_rfl

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
⊢ x ∈ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal))
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
⊢ ∃ x s', x ∉ s' ∧ s = insert x s' ∧ x ∉ q

Tactic:
by
        have : ¬(s : Set R) ⊆ q := by
          rw [← span_le]
          exact fun e ↦ lt_irrefl _ ((hp.2 ⟨hq, e⟩ hpq.le).trans_lt hpq)
        obtain ⟨x, hxt, hxq⟩ := Set.not_subset.mp this
        exact ⟨x, _, fun e ↦ (Finset.mem_erase.mp e).1 rfl, (Finset.insert_erase hxt).symm, hxq⟩

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
m : Ideal R
inst✝ : m.IsMaximal
h : ¬IsField R
⊢ m.height ≤ 1

pp: case refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
m : Ideal R
inst✝ : m.IsMaximal
h : ¬IsField R
⊢ 1 ≤ m.height

Tactic:
· suffices h : (m.height : WithBot ℕ∞) ≤ 1 by norm_cast at h
    rw [← IsPrincipalIdealRing.ringKrullDim_eq_one _ h]
    exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
m : Ideal R
inst✝ : m.IsMaximal
h : ¬IsField R
⊢ 1 ≤ m.height
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ (t.inf fun i ↦ comap (mkLinearMap S M) ((localized₀FrameHom S (mkLinearMap S M)) i)) = ⨅ q ∈ s, q

Tactic:
localized₀FrameHom_apply

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
s : Finset (Submodule R M)
hs : s ⊆ t
hs' : Finset.image (fun q ↦ (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ (t.inf fun i ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i)) = ⨅ q ∈ s, q
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
inst✝ : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing (Rₚ P)
this✝¹ : IsNoetherianRing R
this✝ : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
⊢ IsPrincipalIdealRing R

Tactic:
have dedekind : IsDedekindDomain R := { maximalOfPrime := this _ }

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : Finite (MaximalSpectrum R)
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
inst✝ : IsDomain R
hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing (Rₚ P)
this✝¹ : IsNoetherianRing R
this✝ : IsIntegrallyClosed R
this : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
dedekind : IsDedekindDomain R
⊢ IsPrincipalIdealRing R
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
⊢ Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S)

Tactic:
have : Module.Free R S := Module.free_of_flat_of_isLocalRing

Goal state after:
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
this : Module.Free R S
⊢ Module.finrank R S = Module.finrank (ResidueField R) (ResidueField S)
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case refine_2
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[β] = ⊤
h : (minpoly R β).Monic
⊢ (map (residue R) (minpoly R β)).natDegree ≤ (minpoly (ResidueField R) ((residue S) β)).natDegree

Tactic:
have : Module.Free R S := Module.free_of_flat_of_isLocalRing

Goal state after:
case refine_2
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[β] = ⊤
h : (minpoly R β).Monic
this : Module.Free R S
⊢ (map (residue R) (minpoly R β)).natDegree ≤ (minpoly (ResidueField R) ((residue S) β)).natDegree
Module: Mathlib.RingTheory.LocalRing.NonLocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
tfae_1_to_2 : ¬IsLocalRing R → Nontrivial (MaximalSpectrum R)
tfae_2_to_3 : Nontrivial (MaximalSpectrum R) → ∃ m₁ m₂, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂
⊢ [¬IsLocalRing R, Nontrivial (MaximalSpectrum R), ∃ m₁ m₂, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂].TFAE

Tactic:
tfae_have 3 → 1
  | ⟨m₁, m₂, ⟨hm₁, hm₂, h⟩⟩ => fun _ ↦ h <| (eq_maximalIdeal hm₁).trans (eq_maximalIdeal hm₂).symm

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
tfae_1_to_2 : ¬IsLocalRing R → Nontrivial (MaximalSpectrum R)
tfae_2_to_3 : Nontrivial (MaximalSpectrum R) → ∃ m₁ m₂, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂
tfae_3_to_1 : (∃ m₁ m₂, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂) → ¬IsLocalRing R
⊢ [¬IsLocalRing R, Nontrivial (MaximalSpectrum R), ∃ m₁ m₂, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂].TFAE
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (single ↑n) 1 = (ofPowerSeries ℤ R) (PowerSeries.X ^ n)

Tactic:
ofPowerSeries_X_pow

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (single ↑n) 1 = (single ↑n) 1
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
d : ℕ
hd : D + ↑s = ↑d
⊢ Valued.v ((single ↑s) 1) * Valued.v f ≤ exp (-↑s) * exp (-D)

Tactic:
← ofPowerSeries_X_pow s,

Goal state after:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
d : ℕ
hd : D + ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) (PowerSeries.X ^ s)) * Valued.v f ≤ exp (-↑s) * exp (-D)
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: case h
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
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
h₀ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : ↑s ∉ P
h₂ : (algebraMap S Sₚ) ↑s ∉ Ideal.map (algebraMap S Sₚ) P
⊢ (algebraMap S Sₚ) ↑s * ((algebraMap S Sₚ) (x * s') - mk' Sₚ x s) ∈ Ideal.map (algebraMap S Sₚ) P

Tactic:
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.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
⊢ (Ideal.map (algebraMap S Sₚ) P).ramificationIdx Rₚ = P.ramificationIdx R

Tactic:
have := liesOver_map_of_liesOver p Rₚ Sₚ P
  have := IsLocalization.liesOver_map_of_isPrime_disjoint (algebraMapSubmonoid S p.primeCompl) Sₚ
    (Set.disjoint_image_left.mpr (Set.disjoint_compl_left_iff_subset.mpr hPp.over.ge))
  have := isPrime_map_of_liesOver S p Sₚ P
  rw [ramificationIdx_eq (maximalIdeal Rₚ) (P.map (algebraMap S Sₚ)), ramificationIdx_eq p P]
  let R₁ := Localization.AtPrime (P.map (algebraMap S Sₚ))
  let R₂ := Localization.AtPrime P
  let : Algebra R₂ R₁ := Localization.AtPrime.algebraOfLiesOver P (P.map (algebraMap S Sₚ))
  have : IsLocalization.AtPrime R₁ P := by
    convert isLocalization_isLocalization_atPrime_isLocalization
      (algebraMapSubmonoid S p.primeCompl) R₁ (P.map (algebraMap S Sₚ))
    rw [← Ideal.under_def, ← Ideal.over_def (P.map (algebraMap S Sₚ)) P]
  have h : Function.Bijective (algebraMap R₂ R₁) :=
    (Localization.algEquiv P.primeCompl R₁).bijective
  have key : p.map (algebraMap R R₂) =
      ((maximalIdeal Rₚ).map (algebraMap Rₚ R₁)).comap (algebraMap R₂ R₁) := by
    rw [← IsLocalization.AtPrime.map_eq_maximalIdeal p, p.map_map, ← IsScalarTower.algebraMap_eq,
      IsScalarTower.algebraMap_eq R R₂ R₁, ← p.map_map, comap_map_of_bijective _ h]
  rw [Module.length_quotient, Module.length_quotient, key, coheight_comap_of_surjective _ h.2]

Goal state after:
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) (sumSMulX c) = c i

Tactic:
sumSMulX,

Goal state after:
n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i : n
⊢ coeff (Finsupp.single i 1) ((Finsupp.linearCombination R X) c) = c i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
r : R
⊢ (algebraMap R (MvPolynomial σ R)) r = C r

Tactic:
algebraMap_eq

Goal state after:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
r : R
⊢ C r = C r
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
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ

Tactic:
set η : ℤᵐ⁰ˣ := Units.mk0 (exp f.order) coe_ne_zero
      with hη

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)) ⋯
⊢ ∃ Q, Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) Q) < ↑γ
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) F = (single ↑s) 1 * f
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

Tactic:
← ofPowerSeries_X_pow s,

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) F = (ofPowerSeries ℤ K) (PowerSeries.X ^ s) * f
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) (RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h : t.2 ∈ t.1
⊢ pairMap σ t = (t.1.erase t.2, t.2)

Tactic:
by
  simp [pairMap, h]

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

Goal state before:
pp: σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h : t.2 ∉ t.1
⊢ pairMap σ t = (cons t.2 t.1 h, t.2)

Tactic:
by
  simp [pairMap, h]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ antidiagonal k
⊢ ∑ y, ∑ x ∈ powersetCard a.1 univ, ((-1) ^ #x * ∏ a ∈ x, X a) * X y ^ (k - #x) =
    ∑ i, (∑ i ∈ powersetCard a.1 univ, (-1) ^ a.1 * ∏ a ∈ i, X a) * X i ^ a.2

Tactic:
refine sum_congr rfl fun x _ ↦ ?_

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ antidiagonal k
x : σ
x✝ : x ∈ univ
⊢ ∑ x_1 ∈ powersetCard a.1 univ, ((-1) ^ #x_1 * ∏ a ∈ x_1, X a) * X x ^ (k - #x_1) =
    (∑ i ∈ powersetCard a.1 univ, (-1) ^ a.1 * ∏ a ∈ i, X a) * X x ^ a.2
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ (-1) ^ (k + 1) * ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      -1 * (-1) ^ k * ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0

Tactic:
← pow_one (-1 : MvPolynomial σ R)

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ (-1) ^ (k + 1) * ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      (-1) ^ 1 * (-1) ^ k * ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    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
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : m ≤ n
⊢ (coeff m) φ = MvPolynomial.coeff (p • m) ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
MvPolynomial.coeff_expand_smul _ hp,

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
⊢ (coeff m) φ = MvPolynomial.coeff m ((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
⊢ 0 = MvPolynomial.coeff (p • m) ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
MvPolynomial.coeff_expand_smul _ hp,

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
⊢ 0 = MvPolynomial.coeff m ((trunc' R n) φ)
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

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

Tactic:
rw [← isRestricted_abs_iff, IsRestricted] at *
  refine tendsto_const_nhds.squeeze (add_zero (0 : ℝ) ▸ hf.add hg) (fun n ↦ ?_) fun n ↦ ?_
  · dsimp [Finsupp.prod]; positivity -- TODO: add positivity extension for Finsupp.prod
  rw [← add_mul]
  exact mul_le_mul_of_nonneg_right (norm_add_le ..) (by dsimp [Finsupp.prod]; positivity)

Goal state after: