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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Tactic:
intro σ

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
⊢ ∃ a, (stabilizerHom Q P G) a = σ
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
coeff_single_mul_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
⊢ 1 * ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff (n - order x + order x)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : Field K
⊢ Ideal.span {X} ≠ ⊥

Tactic:
ne_eq,

Goal state after:
R : Type u_1
K : Type u_2
inst✝ : Field K
⊢ ¬Ideal.span {X} = ⊥
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
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
⊢ Multiset.count (Ideal.span {Polynomial.X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count (idealX K).asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑P}))

pp: case neg.hI
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
⊢ Ideal.span {↑P} ≠ 0

pp: case neg.hJ
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
⊢ (idealX K).asIdeal.IsPrime

pp: case neg.hJ₀
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
⊢ (idealX K).asIdeal ≠ ⊥

Tactic:
on_goal 1 => convert! (normalized_count_X_eq_of_coe hP).symm

Goal state after:
case e'_2
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
⊢ Multiset.count (Ideal.span {Polynomial.X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)

case e'_3
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
⊢ Multiset.count (idealX K).asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑P})) =
    Multiset.count X (UniqueFactorizationMonoid.normalizedFactors ↑P)

case neg.hI
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
⊢ Ideal.span {↑P} ≠ 0

case neg.hJ
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
⊢ (idealX K).asIdeal.IsPrime

case neg.hJ₀
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
⊢ (idealX K).asIdeal ≠ ⊥
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
rwa [← log_le_iff_le_exp one_ne_zero, le_neg, log_one, neg_zero]

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

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

Tactic:
over_def P p

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
⊢ under Rₚ (Ideal.map (algebraMap S Sₚ) P) = Ideal.map (algebraMap R Rₚ) (under R P)
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ₚ)
x : Rₚ ⧸ maximalIdeal Rₚ
⊢ (algebraMap (R ⧸ p) (S ⧸ P)) ((equivQuotMaximalIdeal p Rₚ).symm x) =
    (equivQuotientMapOfIsMaximal p Sₚ P).symm
      ((algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) x)

Tactic:
by
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  obtain ⟨x, s, rfl⟩ := mk'_surjective p.primeCompl x
  simp [equivQuotMaximalIdeal_symm_apply_mk, map_mul, Quotient.algebraMap_mk_of_liesOver,
    IsLocalization.algebraMap_mk' S Rₚ Sₚ]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
d n : ℤ
f g : K⸨X⸩
H : Valued.v (g - f) ≤ exp (-d)
triv : ¬g = f
⊢ n < d → g.coeff n = f.coeff n

Tactic:
intro hn
    apply eq_of_sub_eq_zero
    rw [← HahnSeries.coeff_sub]
    apply coeff_zero_of_lt_valuation K H hn

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : MvPolynomial n R
nontrivial : f.support.Nontrivial
d : n →₀ ℕ
hd : d ∈ f.support
i : n
hdi : d i = 1
disjoint : (↑f.support).PairwiseDisjoint Finsupp.support
isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r
hfd : coeff d f ≠ 0
d₀ : n →₀ ℕ := Finsupp.erase i d
φ : MvPolynomial n R := (monomial d₀) (coeff d f)
ψ : MvPolynomial n R := f - φ * X i
hf : f = φ * X i + ψ
⊢ φ * X i = (monomial (Finsupp.erase i d + Finsupp.single i (d i))) (coeff d f)

Tactic:
simp [φ, monomial_add_single, hdi, d₀]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
r : R
⊢ esymmAlgHomMonomial σ 0 r = C r

Tactic:
rw [esymmAlgHomMonomial, monomial_zero', esymmAlgHom_apply, aeval_C, algebraMap_eq]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ Irreducible (sumSMulX c)

Tactic:
by
  apply irreducible_of_totalDegree_eq_one
  · apply le_antisymm
    · simp only [sumSMulX, Finsupp.linearCombination_apply, Finsupp.sum]
      apply totalDegree_finsetSum_le
      intros
      apply le_trans (totalDegree_smul_le ..)
      simp
    · rw [← not_lt, Nat.lt_one_iff, totalDegree_eq_zero_iff]
      intro h
      obtain ⟨i, hi⟩ := hc_nonempty
      simp only [Finsupp.mem_support_iff] at hi
      specialize h (Finsupp.single i 1) (by
        rwa [mem_support_iff, coeff_sumSMulX]) i
      simp only [Finsupp.single_eq_same, one_ne_zero] at h
  · intro r hr
    apply hc_gcd
    intro i
    simpa [coeff_sumSMulX] using hr (Finsupp.single i 1)

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: 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⟯
hx : Valued.v x = embedding ↑d
⊢ (restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x ≠ 0

Tactic:
ne_eq,

Goal state after:
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⟯
hx : Valued.v x = embedding ↑d
⊢ ¬(restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x = 0
Module: Mathlib.RingTheory.MvPowerSeries.Expand

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

Tactic:
ext d
  by_cases! h : ∀ i, p ∣ d i
  · obtain ⟨m, hm⟩ : ∃ m, p • m = d := ⟨d.mapRange (fun a ↦ a / p) (by simp),
      by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
    by_cases h_le : m ≤ n
    · 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]
    · have not_le : ¬ p • m ≤ p • n := by
        obtain ⟨i, hi⟩ : ∃ i, m i > n i := by
          by_contra! hc
          exact h_le (Finsupp.coe_le_coe.mp hc)
        have : ¬ p • m i ≤ p • n i := by
          simp [Nat.mul_lt_mul_of_pos_left hi (p.ne_zero_iff_zero_lt.mp hp)]
        exact Not.intro fun a ↦ this (a i)
      rw [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg h_le]
  · obtain ⟨i, hi⟩ := h
    rw [MvPolynomial.coeff_expand_of_not_dvd _ hi]
    by_cases hd : d ≤ p • n
    · rw [coeff_trunc', if_pos hd, coeff_expand_of_not_dvd _ hp _ hi]
    rw [coeff_trunc', if_neg hd]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v { toCompletion := (LaurentSeriesPkg K).compare ratfuncAdicComplPkg f } = Valued.v f

Tactic:
rw [adicCompletion.valued_ofCompletion]

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) = Valued.v f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
x : ratfuncAdicComplPkg.space
h_cont : Continuous ⇑Valued.v
⊢ Tendsto (⇑Valued.v) (Filter.comap ratfuncAdicComplPkg.coe (𝓝 x)) (𝓝 (Valued.v x))

Tactic:
exact (h_cont.continuousAt.tendsto.comp tendsto_comap).congr
      Valued.valuedCompletion_apply

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)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
⊢ ↑p ^ (n + 1) ∣ (ghostComponent n) x

Tactic:
WittVector.ghostComponent_apply,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
⊢ ↑p ^ (n + 1) ∣ (aeval x.coeff) (W_ ℤ n)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n j : ℕ
hj : j < p ^ n
⊢ ↑(n - v p (j + 1)) ≤ emultiplicity p ((p ^ n).choose (j + 1))

Tactic:
rw [hp.out.emultiplicity_choose_prime_pow hj j.succ_ne_zero]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ (C (↑p ^ i) *
            ∑ k ∈ range (p ^ (n - i)),
              (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (k + 1) *
                  (X i ^ p) ^ (p ^ (n - i) - (k + 1)) *
                ↑((p ^ (n - i)).choose (k + 1))) *
          C (⅟↑p ^ n) +
        C (↑p ^ i) * (X i ^ p) ^ p ^ (n - i) * C (⅟↑p ^ n) -
      C (↑p ^ i) * (X i ^ p) ^ p ^ (n - i) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))

Tactic:
add_sub_cancel_right,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ (C (↑p ^ i) *
        ∑ k ∈ range (p ^ (n - i)),
          (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (k + 1) *
              (X i ^ p) ^ (p ^ (n - i) - (k + 1)) *
            ↑((p ^ (n - i)).choose (k + 1))) *
      C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))
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 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0
s : O
hy : (Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0
h1p : 0 < 1 / ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0

Tactic:
rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_pow] at hx hy

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 : (Ideal.Quotient.mk (Ideal.span {↑p})) (r ^ p) ≠ 0
s : O
hy : (Ideal.Quotient.mk (Ideal.span {↑p})) (s ^ p) ≠ 0
h1p : 0 < 1 / ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case calc_2
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (⇑verschiebung)^[i] (x * (⇑frobenius)^[i] ((⇑verschiebung)^[j] y)) =
    (⇑verschiebung)^[i] (x * (⇑verschiebung)^[j] ((⇑frobenius)^[i] y))

Tactic:
verschiebung_frobenius_comm.iterate_iterate

Goal state after:
case calc_2
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (⇑verschiebung)^[i] (x * (⇑frobenius)^[i] ((⇑verschiebung)^[j] y)) =
    (⇑verschiebung)^[i] (x * (⇑frobenius)^[i] ((⇑verschiebung)^[j] y))
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case succ
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff n) f ≠ 0
k : ℕ
ih :
  (coeff (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (Nat.find h + k + 1)) f
⊢ ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Tactic:
have h1 : (Ideal.Quotient.mk _ x : ModP O p) ≠ 0 := hx.symm ▸ hfn

Goal state after:
case succ
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff n) f ≠ 0
k : ℕ
ih :
  (coeff (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
⊢ ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n : ℕ
⊢ (hermite n).degree = ↑n

Tactic:
rw [degree_eq_of_le_of_coeff_ne_zero]

Goal state after:
case pn
n : ℕ
⊢ (hermite n).degree ≤ ↑n

case p1
n : ℕ
⊢ (hermite n).coeff n ≠ 0
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
⊢ b = c

Tactic:
let trinomial (r : R) : R[X] := a • X ^ 2 + r • X + C a

Goal state after:
R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
⊢ b = c
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
heq : 1 - PowerSeries.X = ↑(1 - X)
⊢ (PowerSeries.coeff n) (↑p * ↑(1 - X) * ↑(invOneSubPow F (d + 1))) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Tactic:
← coe_mul,

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
heq : 1 - PowerSeries.X = ↑(1 - X)
⊢ (PowerSeries.coeff n) (↑(p * (1 - X)) * ↑(invOneSubPow F (d + 1))) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d e : ℕ
he : (p * (1 - X) ^ e).hilbertPoly (d + e) = p.hilbertPoly d
⊢ (p * (1 - X) ^ (e + 1)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d

Tactic:
rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Semiring A
I : Ideal A
f g : A⟦X⟧
inst✝ : I.IsTwoSided
hf : ∀ (i : ℕ), (coeff i) f ∈ I
⊢ ∀ (i : ℕ), (coeff i) (f * g) ∈ I

Tactic:
simpa only [Ideal.IsTwoSided.mul_one] using
    coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (J := 1) (g := g) hf (by simp)

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

Goal state before:
pp: case hS1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
⊢ ∀ σ ∈ ⋃ m, ↑(Ideal.inertia G m.asIdeal),
    (MulAction.toPermHom G ↑(f.rootSet S)) σ = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) σ).IsSwap

Tactic:
intro σ

Goal state after:
case hS1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
σ : G
⊢ σ ∈ ⋃ m, ↑(Ideal.inertia G m.asIdeal) →
    (MulAction.toPermHom G ↑(f.rootSet S)) σ = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) σ).IsSwap
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k : ℕ
hq : ∀ {i : ℕ}, i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat → (coeff i) (f - g * H.seq f k) ∈ I ^ k
i : ℕ
hi : i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) (f - g * H.seq f (k + 1)) ∈ I ^ (k + 1)

Tactic:
seq

Goal state after:
case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k : ℕ
hq : ∀ {i : ℕ}, i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat → (coeff i) (f - g * H.seq f k) ∈ I ^ k
i : ℕ
hi : i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i)
      (f -
        g *
          (H.seq f k +
            (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * H.seq f k)) * ↑⋯.unit⁻¹)) ∈
    I ^ (k + 1)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
i✝ i : ℕ
⊢ (coeff i) (↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q) ∈ I * I ^ k

Tactic:
refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (fun i ↦ ?_) ih _

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
i✝¹ i✝ i : ℕ
⊢ (coeff i) ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) ∈ I
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
a : A[X]
ha : a ∈ Ideal.span {g}
b : A[X]
hb : b * g = a
⊢ ↑b * ↑g = ↑a

Tactic:
simp [← hb]

Goal state after: