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

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
⊢ ((1 - X) ^ (d + 1) * mk fun n ↦ ↑((d + n).choose d)) = 1

Tactic:
rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mul_comm, mk_one_mul_one_sub_eq_one, one_pow]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s t : SummableFamily Γ R α
⊢ (s + t).hsum = s.hsum + t.hsum

Tactic:
by
  ext g
  simp only [coeff_hsum, coeff_add, add_apply]
  exact finsum_add_distrib (s.finite_co_support _) (t.finite_co_support _)

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ #↑{a} = 1

Tactic:
mk_singleton

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ 1 = 1
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case neg
Γ : 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
⊢ 0 < (1 - (single oinv) r * x).orderTop

Tactic:
· have hr' : IsRegular r := IsUnit.isRegular <| .of_mul_eq_one x.leadingCoeff hr
    have hy' : 0 < (single oinv r * y).order := by
      rw [(order_single_mul_of_isRegular hr' hy)]
      refine pos_of_lt_add_right (a := x.order) ?_
      rw [← add_assoc, add_comm x.order, hxo, zero_add]
      exact order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy
    rw [one_minus_single_neg_mul hr (sub_add_cancel x _).symm _ hxo, orderTop_neg]
    exact zero_lt_orderTop_of_order hy'

Goal state after:
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
hpq : p < q
Q : Ideal S
hPQ : P ≤ Q
hQ : Q.IsPrime
hQq : Q.LiesOver q
h : P = Q
⊢ False

Tactic:
subst Q

Goal state after:
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
hpq : p < q
hPQ : P ≤ P
hQ : P.IsPrime
hQq : P.LiesOver q
⊢ False
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mp.mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
hF : F.IsGabriel
I J : Ideal A
hJ : J ∈ F
htors : F.IsTorsionQuot (OrderDual.ofDual (OrderDual.toDual I)) J
x : A
hx : x ∈ J
K : Ideal A
hK : K ∈ F
hincl : K ≤ Submodule.colon (OrderDual.ofDual (OrderDual.toDual I)) {x}
⊢ Submodule.colon I {x} ∈ F

Tactic:
exact Order.PFilter.mem_of_le hincl hK

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
h' : IsField R
⊢ False

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
⊢ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical

pp: case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
⊢ ringKrullDim R = 1

Tactic:
· exact zero_ne_one ((ringKrullDim_eq_zero_of_isField h') ▸ h)

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
h : ringKrullDim R = 1
⊢ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical

case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
x✝ : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical
⊢ ringKrullDim R = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Nontrivial M
⊢ closedPoint R ∈ Module.support R M

Tactic:
obtain ⟨p, hp⟩ := (Module.nonempty_support_iff (R := R)).mpr ‹_›

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Nontrivial M
p : PrimeSpectrum R
hp : p ∈ Module.support R M
⊢ closedPoint R ∈ Module.support R M
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
a✝ : Nontrivial R
m : Ideal R
hm : m.IsMaximal
⊢ ↑m.height ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

Tactic:
exact height_le_ringKrullDim_quotient_add_spanFinrank <|
    le_trans h <| Ring.jacobson_le_of_isMaximal m

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
this : (RelSeries.head l').asIdeal.LiesOver (RelSeries.last lp).asIdeal
lp' : LTSeries (PrimeSpectrum S)
hlp'len : lp'.length = lp.length
hlp' : RelSeries.last lp' = { asIdeal := (RelSeries.head l').asIdeal, isPrime := ⋯ }
right✝ : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList lp') = RelSeries.toList lp
⊢ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height ≤ P.height

Tactic:
have : (lp'.smash l' hlp').length = lp.length + lq.length := by simp [hlp'len, l']

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
this✝ : (RelSeries.head l').asIdeal.LiesOver (RelSeries.last lp).asIdeal
lp' : LTSeries (PrimeSpectrum S)
hlp'len : lp'.length = lp.length
hlp' : RelSeries.last lp' = { asIdeal := (RelSeries.head l').asIdeal, isPrime := ⋯ }
right✝ : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList lp') = RelSeries.toList lp
this : (RelSeries.smash lp' l' hlp').length = lp.length + lq.length
⊢ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height ≤ P.height
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
⊢ ↑p.length + 1 ≤ ⨆ p, ↑p.length

Tactic:
have le : support R (QuotSMulTop x M) ⊆ support R M := by simp

Goal state after:
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
⊢ ↑p.length + 1 ≤ ⨆ p, ↑p.length
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
q : Submodule R M
hq : q ∈ t
⊢ (q.colon Set.univ).radical ∈ N.associatedPrimes

Tactic:
← ht.image_radical_eq_associated_primes

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
q : Submodule R M
hq : q ∈ t
⊢ (q.colon Set.univ).radical ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (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
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
⊢ Module.Finite R M

Tactic:
have : Fintype (MaximalSpectrum R) := Fintype.ofFinite _
  choose s hs using fun P : MaximalSpectrum R ↦ (H P.1).fg_top
  choose frac hfrac using fun P : MaximalSpectrum R ↦ IsLocalizedModule.surj P.1.primeCompl (f P.1)
  use Finset.biUnion Finset.univ fun P ↦ Finset.image (frac P · |>.1) (s P)
  refine Submodule.eq_top_of_localization_maximal Rₚ Mₚ f _ fun P hP ↦ ?_
  rw [eq_top_iff, ← hs ⟨P, hP⟩, Submodule.localized'_span, Submodule.span_le]
  intro x hx
  lift x to s ⟨P, hP⟩ using hx
  rw [SetLike.mem_coe, ← IsLocalization.smul_mem_iff (s := (frac ⟨P, hP⟩ x).2), hfrac]
  exact Submodule.subset_span ⟨_, by simpa using ⟨_, _, x.2, rfl⟩, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: F : Type u
inst✝ : Field F
P : F[X]
⊢ (ofPowerSeries ℤ F) ↑P = (algebraMap F⟮X⟯ F⸨X⸩) ↑P

Tactic:
by
  simp [coePolynomial, coe_def, ← IsScalarTower.algebraMap_apply]

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ₚ
T : Type u_5
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra Rₚ T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsScalarTower R Rₚ T
Q : Ideal T
inst✝ : Q.LiesOver (maximalIdeal Rₚ)
this : (maximalIdeal Rₚ).LiesOver p
⊢ Q.LiesOver p

Tactic:
exact LiesOver.trans Q (IsLocalRing.maximalIdeal Rₚ) p

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
⊢ Valued.v f ≤ exp (-D)

Tactic:
rw [neg_inj] at hs

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
⊢ Valued.v f ≤ exp (-D)
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
i : n
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R { b // b ≠ i })
he : (↑e.symm).comp Polynomial.CAlgHom = rename Subtype.val
f : S
hf0 : ((↑e.symm).comp Polynomial.CAlgHom).toRingHom f ≠ 0
hif : i ∉ (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f).vars
g : S
hig : i ∉ (((↑e.symm).comp Polynomial.CAlgHom).toRingHom g).vars
h : IsRelPrime (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f) (((↑e.symm).comp Polynomial.CAlgHom).toRingHom g)
⊢ Irreducible (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f * X i + ((↑e.symm).comp Polynomial.CAlgHom).toRingHom g)

Tactic:
refine .of_map (f := e) ?_

Goal state after:
n : Type u_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
i : n
S : Type (max u_4 u_3) := MvPolynomial { j // j ≠ i } R
e : MvPolynomial n R ≃ₐ[R] S[X] :=
  (renameEquiv R (Equiv.optionSubtypeNe i).symm).trans (optionEquivLeft R { b // b ≠ i })
he : (↑e.symm).comp Polynomial.CAlgHom = rename Subtype.val
f : S
hf0 : ((↑e.symm).comp Polynomial.CAlgHom).toRingHom f ≠ 0
hif : i ∉ (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f).vars
g : S
hig : i ∉ (((↑e.symm).comp Polynomial.CAlgHom).toRingHom g).vars
h : IsRelPrime (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f) (((↑e.symm).comp Polynomial.CAlgHom).toRingHom g)
⊢ Irreducible
    (e (((↑e.symm).comp Polynomial.CAlgHom).toRingHom f * X i + ((↑e.symm).comp Polynomial.CAlgHom).toRingHom g))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (PowerSeries.idealX K).intValuation (F - ↑((trunc (d + 1)) F)) < ↑η

Tactic:
← valuation_of_algebraMap (K := K⸨X⸩) (PowerSeries.idealX K) (F - F.trunc (d + 1))

Goal state after:
case h
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : Multiplicative.toAdd (unzero ⋯) ≤ 0
d : ℕ
hd : Multiplicative.toAdd (unzero ⋯) = -↑d
this : Valued.v ((algebraMap K⟦X⟧ K⸨X⸩) (F - ↑((trunc (d + 1)) F))) ≤ ↑η * ↑(Multiplicative.ofAdd (-1))
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(F - ↑((trunc (d + 1)) F)) < ↑η
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h.refine_2
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x✝¹ : K⟮X⟯ × K⟮X⟯
x✝ : x✝¹ ∈ (fun x ↦ x.2 - x.1) ⁻¹' {P | Valued.v P < embedding ↑d}
⊢ (fun x ↦ x.2 - x.1) ((algebraMap K⟮X⟯ K⸨X⸩) x✝¹.1, (algebraMap K⟮X⟯ K⸨X⸩) x✝¹.2) ∈
    {y | Valued.v.restrict (y - 0) < ↑d}

Tactic:
simp only [sub_zero, Set.mem_ofPred_eq]

Goal state after:
case h.refine_2
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x✝¹ : K⟮X⟯ × K⟮X⟯
x✝ : x✝¹ ∈ (fun x ↦ x.2 - x.1) ⁻¹' {P | Valued.v P < embedding ↑d}
⊢ Valued.v.restrict ((algebraMap K⟮X⟯ K⸨X⸩) x✝¹.2 - (algebraMap K⟮X⟯ K⸨X⸩) x✝¹.1) < ↑d
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : n ≤ Fintype.card σ
⊢ Function.Injective
    (⇑↑(renameSymmetricSubalgebra (Fintype.equivFin σ).symm) ∘ ⇑(esymmAlgHom (Fin (Fintype.card σ)) R n))

Tactic:
exact (AlgEquiv.injective _).comp (esymmAlgHom_fin_injective R hn)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: 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

Tactic:
refine subset_trans (fun _ _ ↦ ?_) pre_T

Goal state after:
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}
x✝¹ : K⟮X⟯ × K⟮X⟯
x✝ : x✝¹ ∈ (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' (fun x ↦ x.2 - x.1) ⁻¹' X
⊢ x✝¹ ∈ (fun x ↦ x.2 - x.1) ⁻¹' w✝
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| (substAlgHom ⋯) (r • 1)

Tactic:
AlgHom.map_smul_of_tower,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| r • (substAlgHom ⋯) 1
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
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
rw [← hm, coeff_trunc', if_pos (nsmul_le_nsmul_right h_le p), coeff_expand_smul,
        MvPolynomial.coeff_expand_smul _ hp, coeff_trunc', if_pos h_le]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
⊢ ∃ F, (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) = x

Tactic:
have hval : Valued.v f ≤ 1 := by
    rw [← valuation_compare (K := K) f, hf, RingEquiv.symm_apply_apply,
      ← mem_adicCompletionIntegers]
    exact hx

Goal state after:
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
hval : Valued.v f ≤ 1
⊢ ∃ F, (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) = x
Module: Mathlib.RingTheory.WittVector.WittPolynomial

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

Tactic:
apply sum_congr rfl

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∀ x ∈ range (n + 1), (monomial (single x (p ^ (n - x)))) (↑p ^ x) = C (↑p ^ x) * X x ^ p ^ (n - x)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) ((bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n))

Tactic:
rw [bind₁_bind₁]; exact eval₂Hom_congr (RingHom.ext_rat _ _) rfl rfl

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
ne✝ : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
c : k
left✝ : MvPolynomial.coeff 0 (a - b) * c = 1
eqr : c * MvPolynomial.coeff 0 (a - b) = 1
⊢ c • (a - b) = 1

Tactic:
rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (1 - ∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0

Tactic:
rw [sub_mul, one_mul]

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ C ⅟↑p ^ n - (∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n - x) =
    ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))

Tactic:
apply sum_congr rfl

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ (map (Int.castRingHom ℚ)) (φ k) = (map (Int.castRingHom ℚ)) (wittStructureInt p Φ k)

Tactic:
map_wittStructureInt

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ (map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) k
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 ℚ)
⊢ ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ n)).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
map_wittStructureInt

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
p : ℕ
hp : Fact (Nat.Prime p)
inst✝⁵ : CharP R✝ p
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
inst✝² : PerfectRing R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
f : R →+* S
r : R
n : ℕ
⊢ (fun n ↦ f ((⇑↑(frobeniusEquiv R p).symm)^[n] r)) (n + 1) ^ p = (fun n ↦ f ((⇑↑(frobeniusEquiv R p).symm)^[n] r)) n

Tactic:
← f.map_pow,

Goal state after:
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
p : ℕ
hp : Fact (Nat.Prime p)
inst✝⁵ : CharP R✝ p
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
inst✝² : PerfectRing R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
f : R →+* S
r : R
n : ℕ
⊢ f ((⇑↑(frobeniusEquiv R p).symm)^[n + 1] r ^ p) = (fun n ↦ f ((⇑↑(frobeniusEquiv R p).symm)^[n] r)) n