mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℕ
hp : p.length = n
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧ n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q

Tactic:
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 => ?_

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧
      n + 1 = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
⊢ supportDim R M ≤ supportDim R (QuotSMulTop x M) + 1

Tactic:
by
  nontriviality M
  refine iSup_le_iff.mpr (fun p ↦ ?_)
  wlog hxp : x ∈ p.last.1.1 generalizing p
  · obtain ⟨p, hle, hm⟩ := exists_ltSeries_support_isMaximal_last_of_ltSeries_support p
    have hj : (annihilator R M).jacobson ≤ p.last.1.1 :=
      sInf_le ⟨mem_support_iff_of_finite.mp p.last.2, inferInstance⟩
    exact (Nat.cast_le.mpr hle).trans <| this _ (hj h)
  -- `q` is a chain of primes such that `x ∈ q 1`, `p.length = q.length` and `p.head = q.head`.
  obtain ⟨q, hxq, hq, h0, _⟩ : ∃ q : LTSeries (PrimeSpectrum R), _ ∧ _ ∧ p.head = q.head ∧ _ :=
    exist_ltSeries_mem_one_of_mem_last (p.map Subtype.val (fun ⦃_ _⦄ lt ↦ lt)) hxp
  by_cases hp0 : p.length = 0
  · have hb : supportDim R (QuotSMulTop x M) ≠ ⊥ :=
      (supportDim_ne_bot_iff_nontrivial R (QuotSMulTop x M)).mpr <|
        Submodule.Quotient.nontrivial_iff.mpr <|
          (Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator h).symm
    rw [hp0, ← WithBot.coe_unbot (supportDim R (QuotSMulTop x M)) hb]
    exact WithBot.coe_le_coe.mpr zero_le
  -- Let `q' i := q (i + 1)`, then `q'` is a chain of prime ideals in `Supp(M/xM)`.
  let q' : LTSeries (support R (QuotSMulTop x M)) := {
    length := p.length - 1
    toFun := by
      intro ⟨i, hi⟩
      have hi : i + 1 < q.length + 1 :=
        Nat.succ_lt_succ (hi.trans_eq ((Nat.sub_add_cancel (Nat.pos_of_ne_zero hp0)).trans hq))
      exact ⟨q ⟨i + 1, hi⟩, by simpa using!
        ⟨mem_support_mono (by simpa [h0] using! q.monotone (Fin.zero_le _)) p.head.2, q.monotone
          ((Fin.natCast_eq_mk (Nat.lt_of_add_left_lt hi)).trans_le (Nat.le_add_left 1 i)) hxq⟩⟩
    step := by exact fun _ ↦ q.strictMono (by simp)
  }
  grw [le_tsub_add (b := p.length) (a := 1), Nat.cast_add_one, supportDim, Order.krullDim,
    ← le_iSup _ q']

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
J : Submodule R M
hJ : J ∈ s
y : Submodule R M
hy : y ∈ s
⊢ (y.colon Set.univ).radical = (J.colon Set.univ).radical → y.IsPrimary

Tactic:
simp [hs' hy]

Goal state after:
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: case H
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → CommRing (S i)
inst✝² : (i : ι) → Algebra R (S i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsLocalIso R (S i)
this : (i : ι) → Algebra ((i : ι) → S i) (S i) := ⋯
i : ι
⊢ RingHom.ker (algebraMap ((j : ι) → S j) (S i)) = Ideal.span {1 - Pi.single i 1}

pp: case H'
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → CommRing (S i)
inst✝² : (i : ι) → Algebra R (S i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsLocalIso R (S i)
this : (i : ι) → Algebra ((i : ι) → S i) (S i) := ⋯
i : ι
⊢ Function.Surjective ⇑(algebraMap ((j : ι) → S j) (S i))

Tactic:
· apply RingHom.ker_evalRingHom

Goal state after:
case H'
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → CommRing (S i)
inst✝² : (i : ι) → Algebra R (S i)
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), IsLocalIso R (S i)
this : (i : ι) → Algebra ((i : ι) → S i) (S i) := ⋯
i : ι
⊢ Function.Surjective ⇑(algebraMap ((j : ι) → S j) (S i))
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
P✝ : Ideal A
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.LiesOver P
σ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q
N N' : OpenNormalSubgroup G
i : N ⟶ N'
h : FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup ≤ FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup
x : G
hx : ↑x ∈ MulAction.stabilizer (G ⧸ ↑N.toOpenSubgroup) (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q)
hx' :
  (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }).comp
      ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup)) Q) P (G ⧸ ↑N.toOpenSubgroup))
          ⟨↑x, hx⟩) =
    (↑σ).comp
      (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N.toOpenSubgroup).subtype ⋯;
      { toRingHom := __RingHom, commutes' := ⋯ })
g : ↥(FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup)
⊢ ((let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup).subtype ⋯;
          { toRingHom := __RingHom, commutes' := ⋯ }).comp
        ↑((stabilizerHom (under (↥(FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup)) Q) P (G ⧸ ↑N'.toOpenSubgroup))
            ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑↑⟨⟨↑x, hx⟩, hx'⟩, ⋯⟩))
      ((mk (under (↥(FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup)) Q)) g) =
    ((↑σ).comp
        (let __RingHom := quotientMap Q (FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup).subtype ⋯;
        { toRingHom := __RingHom, commutes' := ⋯ }))
      ((mk (under (↥(FixedPoints.subalgebra A B ↥↑N'.toOpenSubgroup)) Q)) g)

Tactic:
exact DFunLike.congr_fun hx' (Ideal.Quotient.mk _ (Subalgebra.inclusion h g))

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
⊢ BddBelow (Function.support fun n ↦ Ring.choose (n + ↑k) k • f.coeff (n + ↑k))

Tactic:
refine ⟨f.order - k, fun x h ↦ ?_⟩

Goal state after:
R✝ : Type u_1
R : Type u_2
V : Type u_3
inst✝² : AddCommGroup V
inst✝¹ : Semiring R
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
x : ℤ
h : x ∈ Function.support fun n ↦ Ring.choose (n + ↑k) k • f.coeff (n + ↑k)
⊢ order f - ↑k ≤ x
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • (hasseDeriv R (k + l)) f).coeff n

Tactic:
by
  rw [coeff_nsmul]
  simp only [hasseDeriv_coeff, Pi.smul_apply, Nat.cast_add]
  rw [smul_smul, mul_comm, ← Ring.choose_add_smul_choose (n + k), add_assoc, Nat.choose_symm_add,
    smul_assoc]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
⊢ x.coeff (order x + ↑(n - order x).natAbs) = x.coeff n

Tactic:
← Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h),

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
⊢ x.coeff (order x + (n - order x)) = x.coeff n
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 : Q.LiesOver p
⊢ (comap (algebraMap S T) Q).LiesOver p

Tactic:
exact comap_liesOver Q p <| IsScalarTower.toAlgHom R S T

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v f ≤ 1 ↔ ∃ F, (ofPowerSeries ℤ K) F = f

Tactic:
rw [valuation_le_iff_coeff_lt_log_eq_zero _ one_ne_zero, log_one, neg_zero]

Goal state after:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∀ n < 0, f.coeff n = 0) ↔ ∃ F, (ofPowerSeries ℤ K) F = f
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:
by
  rw [inertiaDeg'_algebraMap, inertiaDeg'_algebraMap]
  refine Algebra.finrank_eq_of_equiv_equiv (equivQuotMaximalIdeal p Rₚ).symm
    (equivQuotientMapOfIsMaximal p Sₚ P).symm ?_
  ext x
  exact algebraMap_equivQuotMaximalIdeal_symm_apply p Rₚ Sₚ P x

Goal state after:
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})
⊢ ∀ x ∈ (fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n}, ∑ i, w i • (X i * (pderiv i) x) = n • x

Tactic:
rintro _ ⟨m, hm, rfl⟩
    simp_rw [single_eq_monomial, X_mul_pderiv_monomial, smul_smul, ← sum_smul, mul_comm (w _)]
    congr
    rwa [Set.mem_ofPred, weight_apply, sum_fintype] at hm
    intro; apply zero_smul

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

Goal state before:
pp: case refine_4
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})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : ∑ i, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ x, w x • (X x * r • (pderiv x) p) = n • r • p

Tactic:
nsmul_eq_mul,

Goal state after:
case refine_4
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})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : ∑ i, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ x, ↑(w x) * (X x * r • (pderiv x) p) = ↑n * r • p
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hU₁ : {y | Valued.v.restrict (y - limit hℱ) < ↑γ} ⊆ U
this : ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ {y | Valued.v.restrict (y - limit hℱ) < ↑γ}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Tactic:
apply this.mono fun _ hf ↦ hU₁ hf

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case mpr.refine_1
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < embedding ↑d}
X_def : X = {f | Valued.v f < embedding ↑d}
⊢ ∃ γ, {y | Valued.v y < embedding ↑γ} ⊆ X

Tactic:
obtain ⟨x, hx⟩ := restrict₀_surjective _ d.1

Goal state after:
case mpr.refine_1
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < embedding ↑d}
X_def : X = {f | Valued.v f < embedding ↑d}
x : K⟮X⟯
hx : (restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x = ↑d
⊢ ∃ γ, {y | Valued.v y < embedding ↑γ} ⊆ X
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ antidiagonal k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ (p : Finset σ × σ), p ∈ {t ∈ pairs σ k | #t.1 = a.1} ↔ p.1 ∈ powersetCard a.1 univ ∧ p.2 ∈ univ

Tactic:
simp only [mem_filter, mem_powersetCard_univ, mem_univ, and_true, and_iff_right_iff_imp]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ antidiagonal k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ (p : Finset σ × σ), #p.1 = a.1 → p ∈ pairs σ k
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
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
m : σ →₀ ℕ
hm : p • m = n
⊢ (coeff (p • m)) ((expand p hp) ↑φ) = MvPolynomial.coeff (p • m) ((MvPolynomial.expand p) φ)

Tactic:
coeff_expand_smul p hp _ _,

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
m : σ →₀ ℕ
hm : p • m = n
⊢ (coeff m) ↑φ = MvPolynomial.coeff (p • m) ((MvPolynomial.expand p) φ)
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✝ : IsAdicComplete I R
x : Perfection (R ⧸ I) p
y : R
h : ∃ N, ∀ n ≥ N, ∃ z, (Ideal.Quotient.mk I) z = (coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]
⊢ x.teichmullerFun = y

Tactic:
obtain ⟨N, h⟩ := h
  refine (IsHausdorff.eq_iff_smodEq (I := I)).mpr fun n ↦ ?_
  rw [smul_eq_mul, Ideal.mul_top]
  obtain hn | hn := le_total n N
  · obtain ⟨z, hz₁, hz₂⟩ := h N le_rfl
    exact ((teichmullerFun_sModEq hz₁).trans hz₂).mono <| Ideal.pow_le_pow_right (by omega)
  · obtain ⟨z, hz₁, hz₂⟩ := h n hn
    exact ((teichmullerFun_sModEq hz₁).trans hz₂).mono <| Ideal.pow_le_pow_right (by omega)

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case zero
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
⊢ False

Tactic:
have eq := eq_C_of_isEmpty (a - b)

Goal state after:
case zero
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))
⊢ False
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
⊢ wittOne p n = 0

Tactic:
by
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittOne, wittStructureRat, map_zero, map_one, map_wittStructureInt]
  induction n using Nat.strong_induction_on with | h n IH => ?_
  rw [xInTermsOfW_eq]
  simp only [map_mul, map_sub, map_sum, map_pow, bind₁_X_right,
    bind₁_C_right]
  rw [sub_mul, one_mul]
  rw [Finset.sum_eq_single 0]
  · simp only [one_mul, pow_zero]
    simp only [one_pow, one_mul, xInTermsOfW_zero, sub_self, bind₁_X_right]
  · intro i hin hi0
    rw [Finset.mem_range] at hin
    rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero]
  · grind

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

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℤ (n + 1))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))

Tactic:
map_bind₁

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ (bind₁ fun i ↦ (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((rename fun i_1 ↦ (i, i_1)) (W_ ℤ (n + 1))))
      ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
this : (bind₁ (xInTermsOfW p R)) (W_ R n) = X n
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x).ghostFun n = x n

Tactic:
apply_fun aeval x at this

Goal state after:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
this : (aeval x) ((bind₁ (xInTermsOfW p R)) (W_ R n)) = (aeval x) (X n)
⊢ ((fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) x).ghostFun n = x n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m : ℕ
hmn : m ≤ n
⊢ (coeffMonoidHom M p n) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p (n - m + m)) ((⇑(powMonoidHom p))^[m] f)

Tactic:
Nat.sub_add_cancel hmn

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m : ℕ
hmn : m ≤ n
⊢ (coeffMonoidHom M p n) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p n) ((⇑(powMonoidHom p))^[m] f)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
r : M
n : ℕ
⊢ (fun n ↦ f ((powMulEquiv M (p ^ n)).symm r)) (n + 1) ^ p = (fun n ↦ f ((powMulEquiv M (p ^ n)).symm r)) n

Tactic:
rw [← map_pow, powMulEquiv_pow, pow_succ, MulAut.mul_def, MulEquiv.symm_trans_apply,
          powMulEquiv_symm_pow_p, ← powMulEquiv_pow]

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
m n : ℕ
⊢ (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n

Tactic:
by
  induction n generalizing m with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, ← mul_assoc, ← add_assoc, mul_charP_coeff_succ, pow_succ, pow_mul]
    congr
    exact ih

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m : ℕ
h : m < n + 1
⊢ ((⇑verschiebung)^[n + 1] x).coeff m = 0

Tactic:
iterate_succ_apply'

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → ((⇑verschiebung)^[n] x).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (verschiebung ((⇑verschiebung)^[n] x)).coeff m = 0
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ψ (Polynomial.map ι f))
⊢ Irreducible f

Tactic:
replace hi := hm.map ι |>.irreducible_of_irreducible_map _ _ hi

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
⊢ Irreducible f
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case e_a.a
n m : ℕ
hm : m ∈ range (n + 1)
⊢ ↑(n.choose m) * (-1) ^ m * X ^ (m + n) = n.choose m • (-1) ^ m * X ^ (n + m)

pp: case e_a.a.h
n m : ℕ
hm : m ∈ range (n + 1)
⊢ m ≤ n

Tactic:
nsmul_eq_mul,

Goal state after:
case e_a.a
n m : ℕ
hm : m ∈ range (n + 1)
⊢ ↑(n.choose m) * (-1) ^ m * X ^ (m + n) = ↑(n.choose m) * (-1) ^ m * X ^ (n + m)

case e_a.a.h
n m : ℕ
hm : m ∈ range (n + 1)
⊢ m ≤ n
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : -1 * z ^ 0 + -1 * z ^ 1 + 1 * z ^ n = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
replace h1 : z ^ n = z + 1 := by linear_combination h1

Goal state after:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
h1 : z ^ n = z + 1
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n k : ℕ
⊢ (∑ k ∈ range (n + 1), C ((-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)) * X ^ k).coeff k =
    (-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)

Tactic:
finsetSum_coeff

Goal state after:
n k : ℕ
⊢ ∑ b ∈ range (n + 1), (C ((-1) ^ b * ↑(n.choose b) * ↑((n + b).choose n)) * X ^ b).coeff k =
    (-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ (Subalgebra.toSubmodule A).subtype p ∈ P₁

Tactic:
simp only [coe_subtype, Submodule.map_sup, P₁]
        exact Submodule.mem_sup_left ⟨p, hp, rfl⟩

Goal state after: