mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ q ∈ (span t).minimalPrimes

Tactic:
suffices h : (p.map f).height ≤ 1 by
    have h_lt : q.map f < p.map f := (map_mono hqp.le).lt_of_not_ge fun e ↦ hqp.not_ge <| by
      simpa only [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot, f, mk_ker,
        sup_eq_left.mpr hI'q, sup_eq_left.mpr hI'p] using comap_mono (f := f) e
    have : (q.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])
    have : (p.map f).FiniteHeight := ⟨Or.inr (h.trans_lt (WithTop.coe_lt_top 1)).ne⟩
    have := (height_strict_mono_of_isPrime_of_isPrime h_lt).trans_le h
    rw [Order.lt_one_iff, height_eq_zero_iff] at this
    have := minimalPrimes_comap_of_surjective hf this
    rwa [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot,
      mk_ker, sup_eq_left.mpr hI'q] at this

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
⊢ (map f p).height ≤ 1
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
s : Set R
p : Ideal R
inst✝ : p.IsPrime
hrm : s ⊆ ↑p
⊢ p.height ≤ (map (Quotient.mk (span s)) p).height + s.encard

Tactic:
apply le_trans (Ideal.height_le_height_add_spanFinrank_of_le (I := span s) (p := p) ?_) ?_

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
s : Set R
p : Ideal R
inst✝ : p.IsPrime
hrm : s ⊆ ↑p
⊢ span s ≤ p

R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
s : Set R
p : Ideal R
inst✝ : p.IsPrime
hrm : s ⊆ ↑p
⊢ (map (Quotient.mk (span s)) p).height + ↑(Submodule.spanFinrank (span s)) ≤
    (map (Quotient.mk (span s)) p).height + s.encard
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 : D
⊢ ∀ ⦃y : D⦄, x ∈ R → y ∈ R → x * y = y * x

Tactic:
y

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
⊢ x ∈ R → y ∈ R → x * y = y * x
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
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this : Small.{v, u} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
⊢ Module.Injective (Localization.AtPrime p) (LocalizedModule p.primeCompl ↑M)

Tactic:
have : Module.Injective (Localization.AtPrime p) (M.localizedModule p.primeCompl) := by
        simpa [Module.injective_iff_injective_object] using h ⟨p, hp⟩

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this✝ : Small.{v, u} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
this : Module.Injective (Localization.AtPrime p) ↑(M.localizedModule p.primeCompl)
⊢ Module.Injective (Localization.AtPrime p) (LocalizedModule p.primeCompl ↑M)
Module: Mathlib.RingTheory.LocalRing.Etale

Goal state before:
pp: case refine_1
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
⊢ (aeval ((residue S) β)) (map (residue R) (minpoly R β)) = 0

Tactic:
rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl]

Goal state after:
case refine_1
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
⊢ (residue S) ((aeval β) (minpoly R β)) = 0
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)
m₁ : Ideal R
hm₁ : m₁.IsMaximal
m₂ : Ideal R
hm₂ : m₂.IsMaximal
h : { asIdeal := m₁, isMaximal := hm₁ } ≠ { asIdeal := m₂, isMaximal := hm₂ }
x✝ : m₁ = m₂
⊢ { asIdeal := m₁, isMaximal := hm₁ } = { asIdeal := m₂, isMaximal := hm₂ }

Tactic:
congr

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
n : ℤ
k : ℕ
ih : ∀ (f : V⸨X⸩), ((⇑(derivative R))^[k] f).coeff n = (k.factorial • (hasseDeriv R k) f).coeff n
f : V⸨X⸩
⊢ (((⇑(derivative R))^[k] ∘ ⇑(derivative R)) f).coeff n = ((k + 1).factorial • (hasseDeriv R (k + 1)) f).coeff n

Tactic:
Function.comp_apply,

Goal state after:
case succ
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
n : ℤ
k : ℕ
ih : ∀ (f : V⸨X⸩), ((⇑(derivative R))^[k] f).coeff n = (k.factorial • (hasseDeriv R k) f).coeff n
f : V⸨X⸩
⊢ ((⇑(derivative R))^[k] ((derivative R) f)).coeff n = ((k + 1).factorial • (hasseDeriv R (k + 1)) f).coeff n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ ↑P ≠ 0

Tactic:
simp [hP]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ ↑P ≠ 0

Tactic:
simp [hP]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case negSucc
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((ofPowerSeries ℤ K) PowerSeries.X ^ s.succ) = (exp ↑s.succ)⁻¹

Tactic:
valuation_X_pow,

Goal state after:
case negSucc
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ exp (-↑s.succ) = (exp ↑s.succ)⁻¹
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ exp (-↑d)
hnd : n < d
⊢ (PowerSeries.coeff n) f = 0

Tactic:
apply (PowerSeries.X_pow_dvd_iff).mp _ n hnd

Goal state after:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ exp (-↑d)
hnd : n < d
⊢ PowerSeries.X ^ d ∣ f
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
h : Function.Surjective ⇑f
s : S
⊢ ∃ a, (f.pullbackSnd g) a = s

Tactic:
by simpa [eq_comm] using h (g s)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case coe.ofAdd
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
D : ℤ
hD : ↑(Multiplicative.ofAdd D) ≠ 0
⊢ Valued.v f ≤ ↑(Multiplicative.ofAdd D) ↔ ∀ n < -(↑(Multiplicative.ofAdd D)).log, f.coeff n = 0

Tactic:
← exp,

Goal state after:
case coe.ofAdd
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
D : ℤ
hD : ↑(Multiplicative.ofAdd D) ≠ 0
⊢ Valued.v f ≤ exp D ↔ ∀ n < -(exp D).log, f.coeff n = 0
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.IsMaximal
inst✝¹ : P.IsMaximal
inst✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
⊢ (maximalIdeal Rₚ).inertiaDeg' (Ideal.map (algebraMap S Sₚ) P) = p.inertiaDeg' P

Tactic:
inertiaDeg'_algebraMap,

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.IsMaximal
inst✝¹ : P.IsMaximal
inst✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
⊢ finrank (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P) = p.inertiaDeg' P
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_1
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ (∑ x, m x * w x) • (monomial m) 1 = n • (monomial m) 1

Tactic:
congr

Goal state after:
case refine_1.e_a
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
⊢ ∑ x, m x * w x = n
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : f = 0
⊢ ∃ N, ∀ (g : K⸨X⸩), Valued.v (g - f) ≤ 1 → ∀ n < N, g.coeff n = 0

Tactic:
refine ⟨0, fun x hg ↦ ?_⟩

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) := {P | Valued.v.restrict (P.2 - P.1) < 1}
ζ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf✝ : f ∈ S ∩ T
hf : f = 0
x : K⸨X⸩
hg : Valued.v (x - f) ≤ 1
⊢ ∀ n < 0, x.coeff n = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_1
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝¹ : Fin m
i✝ : ℕ
this : i✝ ≤ m - 1
i : ℕ
hi : i + 1 < m
x✝ : i✝ ≤ i
ih : ∀ (hi : i + 1 < m), (accumulate n m) (invAccumulate n m s) ⟨i + 1, hi⟩ = s ⟨i + 1, hi⟩
him : i < m
⊢ s ⟨i, him⟩ - s ⟨i + 1, hi⟩ + s ⟨i + 1, hi⟩ = s ⟨i, him⟩

Tactic:
exact Nat.sub_add_cancel (hs i.le_succ)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
valuation_X_pow,

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

Goal state before:
pp: case disjoint
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
⊢ (⇑ι '' ↑c.support).PairwiseDisjoint Finsupp.support

Tactic:
ι.injective.injOn.pairwiseDisjoint_image

Goal state after:
case disjoint
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
⊢ (↑c.support).PairwiseDisjoint (Finsupp.support ∘ ⇑ι)
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
rw [← inv_eq_one_div, ← mul_sub, map_mul, map_inv₀,
        ← PowerSeries.coe_X, valuation_X_pow, ← hs, ← RatFunc.coe_coe, ← PowerSeries.coe_sub,
        ← coe_algebraMap, adicValued_apply, valuation_of_algebraMap,
        ← Units.val_mk0 (a := exp f.order) exp_ne_zero, ← hη]

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

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hγ : {x | Valued.v.restrict x < ↑γ} ⊆ T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP : Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) P) < ↑((Units.map ↑embedding) γ)
⊢ (f, (algebraMap K⟮X⟯ K⸨X⸩) P) ∈ (fun x ↦ -x.2 + x.1) ⁻¹' T

Tactic:
apply hγ

Goal state after:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hγ : {x | Valued.v.restrict x < ↑γ} ⊆ T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP : Valued.v (f - (algebraMap K⟮X⟯ K⸨X⸩) P) < ↑((Units.map ↑embedding) γ)
⊢ (fun x ↦ -x.2 + x.1) (f, (algebraMap K⟮X⟯ K⸨X⸩) P) ∈ {x | Valued.v.restrict x < ↑γ}
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case C
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
r : R
⊢ (esymmAlgHom (Fin m) R m) (C r) ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
rw [← algebraMap_eq, AlgHom.commutes]

Goal state after:
case C
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
r : R
⊢ (algebraMap R ↥(symmetricSubalgebra (Fin m) R)) r ∈ (esymmAlgHom (Fin m) R n).range
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
i : MvPowerSeries σ R
⊢ (expand 1 ⋯) i = (AlgHom.id R (MvPowerSeries σ R)) i

Tactic:
simp [expand, subst_self]

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
x✝ : ↥(toModuleCatObj R (ι → M) i)
x : ι → M
hx : x ∈ toModuleCatObj R (ι → M) i
⊢ (fun x ↦ ⟨Pi.single i x, ⋯⟩) ((fun x ↦ ∑ i_1, ↑x i_1) ⟨x, hx⟩) = ⟨x, hx⟩

Tactic:
by
    obtain ⟨y, hy⟩ := mem_toModuleCatObj i |>.1 hx
    rw [single_smul] at hy
    simp [← hy]

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: 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
⊢ (single j i 1 * x) • m = (∑ i_1, x i i_1 • single j i_1 1) • m

Tactic:
congr

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
⊢ single j i 1 * x = ∑ i_1, x i i_1 • single j i_1 1
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ (fun x ↦ 0) n ≤ ‖(coeff n) (f + g)‖ * n.prod fun x1 x2 ↦ |c| x1 ^ x2

pp: case refine_2
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ (‖(coeff n) (f + g)‖ * n.prod fun x1 x2 ↦ |c| x1 ^ x2) ≤
    (‖(coeff n) f‖ * n.prod fun x1 x2 ↦ |c| x1 ^ x2) + ‖(coeff n) g‖ * n.prod fun x1 x2 ↦ |c| x1 ^ x2

Tactic:
· dsimp [Finsupp.prod]; positivity

Goal state after:
case refine_2
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ (‖(coeff n) (f + g)‖ * n.prod fun x1 x2 ↦ |c| x1 ^ x2) ≤
    (‖(coeff n) f‖ * n.prod fun x1 x2 ↦ |c| x1 ^ x2) + ‖(coeff n) g‖ * n.prod fun x1 x2 ↦ |c| x1 ^ x2
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (expand p hp) ↑((MvPolynomial.map (frobenius R p)) ((trunc' R (p • n)) f)) =
    (expand p hp) ((map (frobenius R p)) ↑((trunc' R (p • n)) f))

Tactic:
congr

Goal state after:
Module: Mathlib.RingTheory.Perfectoid.Untilt

Goal state before:
pp: O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) O
x : PreTilt O p
n : ℕ
⊢ untilt ((⇑(frobeniusEquiv (PreTilt O p) p).symm)^[n] x ^ p ^ n) = untilt x

Tactic:
congr

Goal state after:
case e_6
O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) O
x : PreTilt O p
n : ℕ
⊢ (⇑(frobeniusEquiv (PreTilt O p) p).symm)^[n] x ^ p ^ n = x
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ X i ^ 0 = 1

Tactic:
rw [pow_zero]

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

Goal state before:
pp: p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) =
    (algebraMap (ZMod (p ^ (n + 1))) (MvPolynomial ℕ (ZMod (p ^ (n + 1))))) (↑p ^ k) * X k ^ p ^ (n - k + 1)

Tactic:
congr

Goal state after:
case e_a.e_a.e_a
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ n + 1 - k = n - k + 1
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
x : Perfection (R ⧸ I) p
⊢ ∀ (n : ℕ), x.teichmullerAux n ≡ x.teichmullerAux (n + 1) [SMOD I ^ n • ⊤]

Tactic:
by simpa using teichmullerAux_sModEq x

Goal state after:
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
m : ℕ
H : m < n
⊢ constantCoeff (C (↑p ^ m) * xInTermsOfW p R m ^ p ^ (n - m)) = 0

Tactic:
simp only [map_mul, map_pow, map_natCast, IH m H]

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
m : ℕ
H : m < n
⊢ ↑p ^ m * 0 ^ p ^ (n - m) = 0
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittAdd p n) = 0

Tactic:
apply constantCoeff_wittStructureInt p _ _ n
  simp only [add_zero, map_add, constantCoeff_X]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + (n - m) = j + (i + (n - i - m))

Tactic:
tsub_right_comm,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + (n - m) = j + (i + (n - m - i))
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    ((wittPolynomial p ℚ ∘ fun n ↦ n + 1) n -
        ∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      C (⅟↑p ^ n)

Tactic:
Function.comp_apply,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (wittPolynomial p ℚ (n + 1) -
        ∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      C (⅟↑p ^ n)