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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ (∑ᶠ (i : β), if h : i ∈ Set.range ⇑f then (s (Classical.choose ⋯)).coeff g else 0) = ∑ᶠ (i : α), (s i).coeff g

Tactic:
exact finsum_emb_domain f fun a => (s a).coeff g

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Semiring Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsStrictOrderedRing Γ
σ : Type u_3
inst✝ : Finite σ
f g : R⟦σ →₀ ℕ⟧
n : σ →₀ ℕ
⊢ (MvPowerSeries.coeff n) (f * g).coeff = (MvPowerSeries.coeff n) (f.coeff * g.coeff)

Tactic:
change (f * g).coeff n = _
      simp_rw [coeff_mul]
      refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
        sum_filter_ne_zero _
      ext m
      simp only [and_congr_left_iff, Finset.mem_antidiagonal, mem_filter, mem_support,
        HasAntidiagonal.mem_antidiagonal]
      rintro h
      rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case pos.refine_2.succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
n : ℕ
hn : n + 1 ∈ {a | ((fun n ↦ x ^ n) a).coeff y ≠ 0}
⊢ n + 1 ∈ (Nat.succ '' ⋃ i ∈ ↑(antidiagonal ⋯ hpwo y), {a | ((fun n ↦ x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}

Tactic:
obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn
      refine Set.mem_union_left _ ⟨n, Set.mem_iUnion.2 ⟨⟨j, i⟩, Set.mem_iUnion.2 ⟨?_, hi⟩⟩, rfl⟩
      simp only [mem_coe, mem_antidiagonal, mem_support, ne_eq, Set.mem_iUnion]
      exact ⟨hj, ⟨n, hi⟩, add_comm j i⟩

Goal state after:
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
hr' : IsRegular r
⊢ x.order < x.order + (oinv + y.order)

Tactic:
← add_assoc,

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
hr' : IsRegular r
⊢ x.order < x.order + oinv + y.order
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra.HasGoingUp R S
p q : Ideal R
inst✝² : q.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hle : p ≤ q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
by
  rcases eq_or_ne p q with rfl | h
  · use P
  · rw [P.over_def p] at hle h
    exact Algebra.HasGoingUp.exists_ideal_ge_liesOver_of_lt P (lt_of_le_of_ne hle h)

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ
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)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ c m ≡ c (m + (k + 1)) [SMOD I ^ m]

Tactic:
← add_assoc,

Goal state after:
case succ
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)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ c m ≡ c (m + k + 1) [SMOD I ^ m]
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case h.succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this✝ : p.IsPrime
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
this :
  ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
    p ∈ (span ↑s).minimalPrimes →
      p.IsPrime →
        ∀ (n : ℕ),
          (∀ 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) →
            s.card ≤ n + 1 → (∃ (x : IsLocalRing R), p = maximalIdeal R) → p.height ≤ ↑(n + 1)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ p.height ≤ ↑(n + 1)

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this : p.IsPrime
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
hR : ∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ p.height ≤ ↑(n + 1)

Tactic:
· rw [← Localization.AtPrime.under_maximalIdeal (I := p)] at hp ⊢
        rw [IsLocalization.height_under p.primeCompl]
        rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp
        exact this _ (s.image (algebraMap R (Localization p.primeCompl))) (by simpa using hp)
          inferInstance _ H (Finset.card_image_le.trans hn) ⟨inferInstance, rfl⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
this : p.IsPrime
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
hR : ∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ p.height ≤ ↑(n + 1)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case h
n : ℕ
H :
  ∀ m < n,
    ∀ {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
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
hn : s.card ≤ n
this : p.IsPrime
⊢ p.height ≤ ↑n

Tactic:
cases n with

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this : p'.IsMaximal
⊢ P.height = p.height + 1

Tactic:
let P' : Ideal Rₚ[X] := P.map (algebraMap R[X] Rₚ[X])

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this✝ : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (algebraMap R[X] Rₚ[X]) P
⊢ P.height = p.height + 1
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
⊢ ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪

Tactic:
have : q.1.IsPrime := q.2

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
⊢ ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
⊢ p.length.sub 1 ≠ 0

Tactic:
by simpa [hp]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
⊢ p.length.sub 0 ≠ 0

Tactic:
by simp [hp]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this✝ : Nonempty ↑(support R M)
this : Nonempty ↑(support R (QuotSMulTop x M))
p : LTSeries ↑(support R (QuotSMulTop x M))
hp : ↑(RelSeries.head p) ∈ support R M ∧ x ∈ ↑(↑(RelSeries.head p)).asIdeal
le : support R (QuotSMulTop x M) ⊆ support R M
q : LTSeries ↑(support R M) := p.map (Set.MapsTo.restrict id (support R (QuotSMulTop x M)) (support R M) le) ⋯
r✝ : Ideal R
hrm : r✝ ∈ (annihilator R M).minimalPrimes
hr✝ : r✝ ≤ (↑(RelSeries.head q)).asIdeal
r : ↑(support R M) := ⟨{ asIdeal := r✝, isPrime := ⋯ }, ⋯⟩
hr : r < RelSeries.head q
⊢ ↑p.length + 1 = ↑(RelSeries.cons q r hr).length

Tactic:
simp [q]

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

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

Tactic:
intro hβ_gen
    rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
    intro x
    obtain ⟨s, rfl⟩ := residue_surjective (R := S) x
    obtain ⟨p, rfl⟩ := hβ_gen s
    exact ⟨p.map (residue R), by
      rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl p β]⟩

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

Goal state before:
pp: case pos
ι : 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)
i : ι
h₀ : 0 ∈ Submonoid.map (Pi.evalRingHom R i) M
⊢ Surjective (↑↑(algebraMap (R i) (S i))).1

Tactic:
have := uniqueOfZeroMem h₀ (S := (S i))
    exact surjective_to_subsingleton (algebraMap (R i) (S i))

Goal state after:
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 : 0 < HahnSeries.order f
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 (-(D - ↑s))

Tactic:
neg_sub,

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 : 0 < HahnSeries.order f
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 - D)
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
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : 0 < D - ↑s
d : ℕ
hd : D - ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (- -(↑s - D))

Tactic:
neg_sub,

Goal state after:
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
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : 0 < D - ↑s
d : ℕ
hd : D - ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ exp (-(D - ↑s))
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
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
h₂ : (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) (mk' Sₚ x s) *
      (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) =
    (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) x)

Tactic:
equivQuotientMapOfIsMaximal_apply_mk,

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
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)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
h₂ : (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) (mk' Sₚ x s) *
      (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) ((algebraMap S Sₚ) ↑s) =
    (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) x)
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
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
h₂ : (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0
⊢ (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) x = (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) x)

Tactic:
equivQuotientMapOfIsMaximal_apply_mk,

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
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)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
h₂ : (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0
⊢ (algebraMap S (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) x =
    (Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) ((algebraMap S Sₚ) x)
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
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.LaurentSeries

Goal state before:
pp: case mpr
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}
⊢ ∃ t,
    (∃ t_1 ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
      (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ S

Tactic:
refine ⟨(fun x : K⸨X⸩ × K⸨X⸩ ↦ x.snd - x.fst) ⁻¹' X, ⟨X, ?_⟩, ?_⟩

Goal state after:
case mpr.refine_1
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 ∈ nhds 0 ∧ (fun x ↦ x.2 - x.1) ⁻¹' X ⊆ (fun x ↦ x.2 - x.1) ⁻¹' X

case mpr.refine_2
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}
⊢ (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' (fun x ↦ x.2 - x.1) ⁻¹' X ⊆ S
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case inl
σ : 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
h3 : 1 ≤ #t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - #t.1 + 1)) +
      (-1) ^ (#t.1 - 1) * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) =
    0

Tactic:
rw [← tsub_tsub_assoc h.left h3, ← neg_neg ((-1 : MvPolynomial σ R) ^ (#t.1 - 1)),
      h2 (#t.1 - 1), Nat.sub_add_cancel h3]

Goal state after:
case inl
σ : 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
h3 : 1 ≤ #t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) +
      -(-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#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
d : σ →₀ ℕ
r : R
⊢ (algebraMap R (MvPowerSeries σ R)) r * ∏ a ∈ d.support, (X a ^ p) ^ d a = C r * (p • d).prod fun s e ↦ X s ^ e

Tactic:
Finsupp.prod_of_support_subset _ Finsupp.support_smul

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
d : σ →₀ ℕ
r : R
⊢ (algebraMap R (MvPowerSeries σ R)) r * ∏ a ∈ d.support, (X a ^ p) ^ d a = C r * ∏ x ∈ d.support, X x ^ (p • d) x

case h
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
d : σ →₀ ℕ
r : R
⊢ ∀ i ∈ d.support, X i ^ 0 = 1
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: case e_a
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
i1 j1 : ι
⊢ ∑ j_1, single j i 1 i1 j_1 * x j_1 j1 = ∑ c, single j c (x i c) i1 j1

Tactic:
rw [Finset.sum_eq_single_of_mem (a := i) (by simp) (fun b _ hb ↦ by simp [single, Ne.symm hb])]

Goal state after:
case e_a
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
i1 j1 : ι
⊢ single j i 1 i1 i * x i j1 = ∑ c, single j c (x i c) i1 j1
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case neg
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
· obtain ⟨f, fi, fne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot eqi
      set ϕ := kerLiftAlg <| hom2 f I
      have := Quotient.nontrivial_iff.mpr hi
      obtain ⟨s, _, g, injg, intg⟩ := hd (ker <| hom2 f I) (ker_ne_top <| hom2 f I)
      have comp : (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k <| ker <| hom2 f I) = (hom2 f I) :=
        AlgHom.ext fun a ↦ by
          simp only [AlgHom.coe_comp, Quotient.mkₐ_eq_mk, Function.comp_apply, kerLiftAlg_mk]
      exact ⟨s, by lia, ϕ.comp g, (ϕ.coe_comp  g) ▸ (kerLiftAlg_injective _).comp injg,
        intg.trans _ _ <| (comp ▸ hom2_isIntegral f I fne fi).tower_top _ _⟩

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
← vars_map_of_injective _ this,

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ n)).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)