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

Goal state before:
pp: case succ
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
n : ℕ
h : ↑n ! * dp R n x = dp R 1 x ^ n
⊢ ↑(n + 1)! * dp R (n + 1) x = ↑n ! * ↑((n + 1).choose n) * dp R (n + 1) x

Tactic:
← Nat.cast_mul

Goal state after:
case succ
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
n : ℕ
h : ↑n ! * dp R n x = dp R 1 x ^ n
⊢ ↑(n + 1)! * dp R (n + 1) x = ↑(n ! * (n + 1).choose n) * dp R (n + 1) x
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔ ε ∣ x

Tactic:
dvd_def,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ TrivSqZeroExt.fst x = 0 ↔ ∃ c, x = ε * c
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x a : A
ha : a ∈ I
b : A
hb : b ∈ J
m : ℕ
hm : m ≠ 0
⊢ hI.dpow m (b * a) ∈ I * J

Tactic:
hI.dpow_mul ha,

Goal state after:
case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x a : A
ha : a ∈ I
b : A
hb : b ∈ J
m : ℕ
hm : m ≠ 0
⊢ b ^ m * hI.dpow m a ∈ I * J
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Submodule.map (↑P.h1CotangentEquivCotangent) (H1Cotangent.δ R P.Ring S).ker = Submodule.map h1Cotangentι ⊤

Tactic:
Submodule.map_top,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Submodule.map (↑P.h1CotangentEquivCotangent) (H1Cotangent.δ R P.Ring S).ker = h1Cotangentι.range
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d : ℕ
h : 0 < d
⊢ ↑(invOneSubPow S d) = mk fun n ↦ ↑((d - 1 + n).choose (d - 1))

Tactic:
rw [← Nat.sub_one_add_one_eq_of_pos h, invOneSubPow, add_tsub_cancel_right]

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
f : PowerSeries R
g : Γ
hg : ¬g = 0
⊢ (powerSeriesFamily 0 f).hsum.coeff g = (PowerSeries.constantCoeff f • 1).coeff g

Tactic:
rw [coeff_hsum, finsum_eq_zero_of_forall_eq_zero
      fun n ↦ (by by_cases hn : n = 0 <;> simp [hg, hn])]
    simp [hg]

Goal state after:
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp [coeff_index_single_X]

Goal state after:
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, subst_add .X_X, Fin.isValue, subst_X .X_X,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, subst_mul .X_X]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
aux₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
aux₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
⊢ (⋃ a, ((⇑s - ⇑s') a).support).IsPWO

Tactic:
simp_rw [sub_eq_add_neg]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
⊢ (⋃ a, ((⇑s + -⇑s') a).support).IsPWO
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
g : Γ
⊢ {a | ((⇑s - ⇑s') a).coeff g ≠ 0}.Finite

Tactic:
simp_rw [sub_eq_add_neg]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
g : Γ
⊢ {a | ((⇑s + -⇑s') a).coeff g ≠ 0}.Finite
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries = F.zeroX

Tactic:
by
      have : ![0, 0] = (0 : Fin 2 → PowerSeries R) := by ext x : 1; fin_cases x <;> rfl
      simp [← F.assoc', this, subst_zero_of_constantCoeff_zero F.zero_constantCoeff,
        PowerSeries.HasSubst.X', PowerSeries.HasSubst]

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
i : ℕ
h✝ : ¬0 < x.orderTop
⊢ (0 ^ i).cardSupp ≤ x.cardSupp ^ i

Tactic:
cases i

Goal state after:
case neg.zero
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h✝ : ¬0 < x.orderTop
⊢ (0 ^ 0).cardSupp ≤ x.cardSupp ^ 0

case neg.succ
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h✝ : ¬0 < x.orderTop
n✝ : ℕ
⊢ (0 ^ (n✝ + 1)).cardSupp ≤ x.cardSupp ^ (n✝ + 1)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
hp✝ : maximalIdeal R ∈ I.minimalPrimes
hp : maximalIdeal R ∈ {p | I.IsMinimalPrime p}
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Ideal.comap (algebraMap R (R ⧸ I)) J = maximalIdeal R

Tactic:
Set.mem_ofPred

Goal state after:
case e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
hp✝ : maximalIdeal R ∈ I.minimalPrimes
hp : I.IsMinimalPrime (maximalIdeal R)
J : Ideal (R ⧸ I)
prime : J.IsPrime
⊢ Ideal.comap (algebraMap R (R ⧸ I)) J = maximalIdeal R
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝ : p.IsPrime
this : (map f p).IsPrime
r : Ideal (R ⧸ span t)
x✝ : (fun q ↦ q.IsPrime ∧ map f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map f (span {x}) ≤ r
| p

Tactic:
rw [← sup_eq_left.mpr hI'p, ← (span t).mk_ker, RingHom.ker_eq_comap_bot,
      ← comap_map_of_surjective f hf p]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
f : R →+* R ⧸ span t := Quotient.mk (span t)
hf : Function.Surjective ⇑f
hI'q : span t ≤ q
hI'p : span t ≤ p
this✝ : p.IsPrime
this : (map f p).IsPrime
r : Ideal (R ⧸ span t)
x✝ : (fun q ↦ q.IsPrime ∧ map f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map f (span {x}) ≤ r
| comap f (map f p)
Module: Mathlib.RingTheory.KrullDimension.Module

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
this : Nonempty ↑(support R M)
⊢ supportDim R M ≠ ⊥

Tactic:
simp [supportDim]

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

Goal state before:
pp: 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 ∈ 𝔪
⊢ ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪

Tactic:
by
  by_cases hn : x ∈ p₀.1
  · exact ⟨p₁, h₀.le hn, h₀, h₁⟩
  let e := p₀.1.primeSpectrumQuotientOrderIsoZeroLocus.symm
  obtain ⟨q, hq⟩ := (p₀.1 + span {x}).nonempty_minimalPrimes <|
    sup_le (IsLocalRing.le_maximalIdeal_of_isPrime p₀.1) ((span_singleton_le_iff_mem 𝔪).mpr hx)
      |>.trans_lt (IsMaximal.isPrime' 𝔪).1.lt_top |>.ne
  let q : PrimeSpectrum R := ⟨q, hq.1.1⟩
  have : q.1.IsPrime := q.2
  have hxq : x ∈ q.1 := le_sup_right.trans hq.1.2 (mem_span_singleton_self x)
  refine ⟨q, hxq, lt_of_le_not_ge (le_sup_left.trans hq.1.2) fun h ↦ hn (h hxq), ?_⟩
  refine lt_of_le_of_ne (IsLocalRing.le_maximalIdeal_of_isPrime q.1) fun hqm ↦ ?_
  have h : (e ⟨q, le_sup_left.trans hq.1.2⟩).1.height ≤ 1 :=
    map_height_le_one_of_mem_minimalPrimes hq
  simp_rw [show q = closedPoint R from PrimeSpectrum.ext hqm] at h
  have hph : (e ⟨p₁, h₀.le⟩).1.height ≤ 0 :=
    Order.lt_one_iff_nonpos.mp (height_le_iff.mp h _ inferInstance (by simpa using h₁))
  refine not_lt_zero (a := (e ⟨p₀, le_refl p₀⟩).1.height) (height_le_iff.mp hph _ inferInstance ?_)
  simpa using h₀

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : LTSeries (PrimeSpectrum R)
x : R
hx : x ∈ (RelSeries.last p).asIdeal
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧
      p.length = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q

Tactic:
generalize hp : p.length = n
  induction n generalizing p with
  | zero =>
    use RelSeries.singleton _ p.last
    simp only [RelSeries.singleton_toFun, hx, RelSeries.singleton_length, RelSeries.head,
      RelSeries.last_singleton, and_true, true_and]
    rw [show 0 = Fin.last p.length from Fin.zero_eq_mk.mpr hp, RelSeries.last]
  | succ n hn => ?_
  by_cases h0 : n = 0
  · use p
    have h1 : 1 = Fin.last p.length := by
      rw [Fin.last, hp, h0, zero_add]
      exact Fin.natCast_eq_mk (Nat.one_lt_succ_succ 0)
    simpa [h1, hp] using! hx
  obtain ⟨q, hxq, h2, hq⟩ : ∃ q : PrimeSpectrum R, x ∈ q.1 ∧ p ⟨p.length - 2, _⟩ < q ∧ q < p.last :=
    (p ⟨p.length - 1, p.length.sub_lt_succ 1⟩).exist_mem_one_of_mem_two
      (p.strictMono (Nat.pred_lt (by simpa [hp]))) (p.strictMono (Nat.pred_lt (by simp [hp]))) hx
  obtain ⟨Q, hx, hQ, hh, hl⟩ := hn (p.eraseLast.eraseLast.snoc q h2) (by simpa using! hxq) <| by
    simpa [hp] using! Nat.succ_pred_eq_of_ne_zero h0
  have h1 : 1 < Q.length + 1 := Nat.lt_of_sub_ne_zero (hQ.symm.trans_ne h0)
  have h : 1 = (1 : Fin (Q.length + 1)).castSucc := by simp [Fin.one_eq_mk_of_lt h1]
  exact ⟨Q.snoc p.last (by simpa [← hl] using! hq), by simpa [h], by simpa, by simp [← hh], by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : f n = N ∨ N + a ^ n • ⊤ = N
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N

Tactic:
rw [add_eq_sup, sup_eq_left] at h

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : f n = N ∨ a ^ n • ⊤ ≤ N
⊢ b ∈ N ∨ ∃ n, a ^ n • ⊤ ≤ N
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case bot
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
⊢ injectiveDimension M ≤ ⊥ → injectiveDimension (M.localizedModule S) ≤ ⊥

Tactic:
simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]

Goal state after:
case bot
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
⊢ Subsingleton ↑M → Subsingleton (LocalizedModule S ↑M)
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : IsLocalIso R S
⊢ IsLocalIso R T

Tactic:
algebraize [e.toAlgHom.toRingHom]
  have : IsStandardOpenImmersion S T := .of_bijective e.bijective
  exact .trans _ S _

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart = x

Tactic:
by
  ext n
  rw [← sub_add_cancel n x.order, coeff_single_mul_add, sub_add_cancel, one_mul]
  by_cases h : x.order ≤ n
  · rw [Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h), coeff_coe_powerSeries,
      powerSeriesPart_coeff, ← Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h),
      add_sub_cancel]
  · rw [ofPowerSeries_apply, embDomain_of_notMem_range]
    · contrapose! h
      exact order_le_of_coeff_ne_zero h.symm
    · contrapose h
      simp only [Nat.castOrderEmbedding_apply, Set.mem_range] at h
      lia

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
cases i

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

case negSucc
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a✝ : ℕ
⊢ ((ofPowerSeries ℤ R) f).coeff (Int.negSucc a✝) = if Int.negSucc a✝ < 0 then 0 else (coeff (Int.negSucc a✝).natAbs) f
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 * f) ≤ exp (-↑s + -D)

Tactic:
exp_add,

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 ((single ↑s) 1 * f) ≤ exp (-↑s) * exp (-D)
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 (↑s + -D)

Tactic:
exp_add,

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 * exp (-D)
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝² : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this✝ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
R₂ : Type u_2 := Localization.AtPrime P
this : Algebra R₂ R₁ := algebraOfLiesOver P (Ideal.map (algebraMap S Sₚ) P)
⊢ IsLocalization.AtPrime R₁ P

Tactic:
convert isLocalization_isLocalization_atPrime_isLocalization
      (algebraMapSubmonoid S p.primeCompl) R₁ (P.map (algebraMap S Sₚ))

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝² : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this✝ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
R₂ : Type u_2 := Localization.AtPrime P
this : Algebra R₂ R₁ := algebraOfLiesOver P (Ideal.map (algebraMap S Sₚ) P)
⊢ P = comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) P)
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
⊢ ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i (sumSMulX c)) → IsUnit x

Tactic:
intro r hr

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
r : R
hr : ∀ (i : n →₀ ℕ), r ∣ coeff i (sumSMulX c)
⊢ IsUnit r
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 →₀ ℕ := ⋯
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), (∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d (sumSMulXSMulY c)) → IsUnit r

Tactic:
intro r hr

Goal state after:
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)
⊢ IsUnit r
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsPrecomplete I R
x : Perfection (R ⧸ I) p
y : R
n : ℕ
h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x
⊢ x.teichmullerFun ≡ y ^ p ^ n [SMOD I ^ (n + 1)]

Tactic:
have := (exists_teichmullerFun x).choose_spec (n + 1)
  rw [smul_eq_mul, Ideal.mul_top] at this
  exact this.symm.trans <| .pow_pow_add_one (I.natCast_mem_of_charP_quotient p) (m := n) <| by
    simp [SModEq.idealQuotientMk, h]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : ℤ
⊢ i.castDef.ghostFun = ↑i

Tactic:
cases i

Goal state after:
case ofNat
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
a✝ : ℕ
⊢ (Int.ofNat a✝).castDef.ghostFun = ↑(Int.ofNat a✝)

case negSucc
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
a✝ : ℕ
⊢ (Int.negSucc a✝).castDef.ghostFun = ↑(Int.negSucc a✝)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))

Tactic:
Finset.mem_range,

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k < n + 1
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ 0)) = (Int.castRingHom ℚ) (constantCoeff Φ)

Tactic:
← constantCoeff_map,

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ 0)) = (Int.castRingHom ℚ) (constantCoeff Φ)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ n)) = (Int.castRingHom ℚ) 0

Tactic:
← constantCoeff_map,

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ n)) = (Int.castRingHom ℚ) 0
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < v ↑p
| v ↑p

Tactic:
rw [← rpow_one (v p)]

Goal state after:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < v ↑p
| v ↑p ^ 1