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
inst✝ : IsInvariant A B G
x : B
N : OpenNormalSubgroup G
hN : ↑N ⊆ ↑(MulAction.stabilizer G x)
⊢ IsIntegral A x

Tactic:
have := (Algebra.IsInvariant.isIntegral A (FixedPoints.subalgebra A B N.1.1) (G ⧸ N.1.1)).1
    ⟨x, fun g ↦ hN g.2⟩

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
inst✝ : IsInvariant A B G
x : B
N : OpenNormalSubgroup G
hN : ↑N ⊆ ↑(MulAction.stabilizer G x)
this : IsIntegral A ⟨x, ⋯⟩
⊢ IsIntegral A 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 : ℕ
n : ℤ
x : V
m : ℤ
h : ¬m = n
⊢ m + ↑k ≠ n + ↑k

Tactic:
lia

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : ¬IsLocalRing R
m₁ m₂ : Ideal R
left✝¹ : m₁.IsMaximal
left✝ : m₂.IsMaximal
hm₁m₂ : m₁ ≠ m₂
e : R ⧸ m₁ ⊓ m₂ ≃+* (R ⧸ m₁) × R ⧸ m₂ := m₁.quotientInfEquivQuotientProd m₂ ⋯
f : R →+* (R ⧸ m₁) × R ⧸ m₂ := e.toRingHom.comp (Ideal.Quotient.mk (m₁ ⊓ m₂))
⊢ ∃ K₁ K₂ x x_1 f, Function.Surjective ⇑f

Tactic:
use R ⧸ m₁, R ⧸ m₂, Ideal.Quotient.field m₁, Ideal.Quotient.field m₂, f

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : ¬IsLocalRing R
m₁ m₂ : Ideal R
left✝¹ : m₁.IsMaximal
left✝ : m₂.IsMaximal
hm₁m₂ : m₁ ≠ m₂
e : R ⧸ m₁ ⊓ m₂ ≃+* (R ⧸ m₁) × R ⧸ m₂ := ⋯
f : R →+* (R ⧸ m₁) × R ⧸ m₂ := ⋯
⊢ Function.Surjective ⇑f
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0

Tactic:
ext
  simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ∃ y, ↑y = n - order x
⊢ order x ≤ n

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ n - order x ∉ Set.range ⇑Nat.castOrderEmbedding

Tactic:
· contrapose h
      simp only [Nat.castOrderEmbedding_apply, Set.mem_range] at h
      lia

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
K : Type u_2
inst✝ : Field K
P : K[X]
hP : P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

Tactic:
rw [hP, Valuation.map_zero, Polynomial.coe_zero, Valuation.map_zero]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
⊢ 0 ≤ D + ↑s

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
⊢ 0 ≤ D - ↑s

Tactic:
lia

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⟧ := ⋯
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
hDs : 0 < D + ↑s
d : ℕ
hd : D + ↑s = ↑d
n : ℕ
hn : n < d
⊢ -↑s + ↑n < D

Tactic:
lia

Goal state after:
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⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : D - ↑s ≤ 0
⊢ 0 ≤ -D + ↑s

Tactic:
lia

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⟧ := ⋯
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : 0 < D - ↑s
d : ℕ
hd : D - ↑s = ↑d
n : ℕ
hn : n < d
⊢ ↑s + ↑n < D

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
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:
exact fun _ => by rw [triv]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
x✝ : ℕ
⊢ ¬↑x✝ = n✝

Tactic:
lia

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
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
this : ∀ (a b : MvPolynomial n R), p = a * b → a.totalDegree ≤ b.totalDegree → IsUnit a ∨ IsUnit b
hle : ¬a.totalDegree ≤ b.totalDegree
⊢ b.totalDegree ≤ a.totalDegree

Tactic:
lia

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
p : MvPolynomial n R
hp : p.totalDegree = 1
hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x
a b : MvPolynomial n R
hab : p = a * b
hle : a.totalDegree ≤ b.totalDegree
ha₀ : a ≠ 0
hb₀ : b ≠ 0
this : a.totalDegree + b.totalDegree = 1
⊢ a.totalDegree = 0

Tactic:
lia

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
i j : n
hj : j ∈ c.support
hji : j ≠ i
⊢ coeff (Finsupp.single i 1) (c j • X j) = 0

Tactic:
rw [coeff_smul, coeff_X, if_neg]

Goal state after:
n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i j : n
hj : j ∈ c.support
hji : j ≠ i
⊢ c j • 0 = 0

case hnc
n : Type u_1
R : Type u_2
inst✝ : CommRing R
c : n →₀ R
i j : n
hj : j ∈ c.support
hji : j ≠ i
⊢ ¬Finsupp.single j 1 = Finsupp.single i 1
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}
⊢ X ∈ nhds 0

Tactic:
· simp only [Valued.mem_nhds, sub_zero, Valuation.restrict_lt_iff_lt_embedding]
        obtain ⟨x, hx⟩ := restrict₀_surjective _ d.1
        use Units.mk0 (Valued.v.restrict (x : K⸨X⸩)) (by
          simp only [ne_eq, map_eq_zero]
          intro h
          simp only [h, map_zero] at hx
          exact Units.ne_zero _ hx.symm)
        simp only [Units.val_mk0, ← Valuation.restrict_lt_iff_lt_embedding,
          X_def, Set.ofPred_subset_ofPred, Valuation.restrict_lt_iff]
        rw [← hx, embedding_restrict₀]
        simp [v_def, valuation_coe_ratFunc]

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

Goal state before:
pp: case right.inr.ind.inr.refine_1
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
hne : p ≠ esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
⊢ leadingCoeff (⇑toLex) p = leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p))

Tactic:
rw [leadingCoeff_esymmAlgHomMonomial t le_rfl]

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

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
⊢ (0, k).1 + (0, k).2 = k ∧ (0, k).1 < k ∧ ¬0 < (0, k).1

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case h
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : ¬a = 0
⊢ {y | Valued.v.restrict (y - a) < ↑(Units.mk0 (Valued.v.restrict a) ⋯)} ⊆
    {x |
      ∀ (a_1 : K⟮X⟯),
        { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm a_1) } = x → Valued.v a_1 = Valued.v a}

Tactic:
simp only [Units.val_mk0, v_def, Set.ofPred_subset_ofPred]

Goal state after:
case h
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : ¬a = 0
⊢ ∀ (a_1 : adicCompletion K⟮X⟯ (idealX K)),
    Valued.v.restrict (a_1 - a) < Valued.v.restrict a →
      ∀ (a_3 : K⟮X⟯),
        { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm a_3) } = a_1 →
          (valuation K⟮X⟯ (idealX K)) a_3 = Valued.v a
Module: Mathlib.RingTheory.Noetherian.Filter

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ EventuallyConst (⇑f) atTop

Tactic:
by
  simp_rw [eventuallyConst_atTop, eq_comm]
  exact (monotone_stabilizes_iff_noetherian.mpr inferInstance) f

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
i : Fin (n + 1)
⊢ f.totalDegree < up

Tactic:
lia

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

Goal state before:
pp: p n : ℕ
⊢ ∑ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) + 0 * X (n + 1) ^ p ^ (n + 1 - (n + 1)) =
    (expand p) (∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i))

Tactic:
zero_mul,

Goal state after:
p n : ℕ
⊢ ∑ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) + 0 =
    (expand p) (∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i))
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I := kerLiftAlg (hom2 f I)
this : Nontrivial (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left✝ : s ≤ d
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ ker (hom2 f I)
injg : Function.Injective ⇑g
intg : g.IsIntegral
comp : (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k (ker (hom2 f I))) = hom2 f I
⊢ s ≤ d + 1

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case succ
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
by_cases eqi : I = 0
    · have bij : Function.Bijective (Quotient.mkₐ k I) :=
        (Quotient.mk_bijective_iff_eq_bot I).mpr eqi
      exact ⟨d + 1, le_rfl, _, bij.1, isIntegral_of_surjective _ bij.2⟩
    · obtain ⟨f, fi, fne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot eqi
      set ϕ := kerLiftAlg <| hom2 f I
      have := Quotient.nontrivial_iff.mpr hi
      obtain ⟨s, _, g, injg, intg⟩ := hd (ker <| hom2 f I) (ker_ne_top <| hom2 f I)
      have comp : (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k <| ker <| hom2 f I) = (hom2 f I) :=
        AlgHom.ext fun a ↦ by
          simp only [AlgHom.coe_comp, Quotient.mkₐ_eq_mk, Function.comp_apply, kerLiftAlg_mk]
      exact ⟨s, by lia, ϕ.comp g, (ϕ.coe_comp  g) ▸ (kerLiftAlg_injective _).comp injg,
        intg.trans _ _ <| (comp ▸ hom2_isIntegral f I fne fi).tower_top _ _⟩

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

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
⊢ i ∈ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars → i ∈ range n

pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ n ∉ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars

Tactic:
all_goals
    intro H
    replace H := vars_sum_subset _ _ H
    rw [mem_biUnion] at H
    rcases H with ⟨j, hj, H⟩
    rw [vars_C_mul] at H
    swap
    · apply pow_ne_zero
      exact mod_cast hp.1.ne_zero
    rw [mem_range] at hj
    replace H := (ih j hj).2 (vars_pow _ _ H)
    rw [mem_range] at H

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i ∈ range n

case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i < n

Tactic:
lia

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

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False

Tactic:
lia

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
i : ℕ
hi : i < n + 1
this : (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)) = ↑p ^ i * x.coeff i ^ p ^ (n - i)
⊢ n + 1 = n - i + 1 + i

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: p : ℕ
M : Type u_2
N : Type u_3
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
inst✝ : CommMonoid N
e : M →* N
x : M
⊢ (coeffMonoidHom N p 0) (((liftMonoidHom p M N) e) x) = e x

Tactic:
simp [liftMonoidHom]

Goal state after:
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
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
⊢ n ≤ m ∨ n = m + 1 ∨ ¬n ≤ m + 1

Tactic:
lia

Goal state after:
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
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n ≤ m
⊢ n ≤ m + 1

Tactic:
lia

Goal state after:
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
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : ¬n ≤ m + 1
⊢ ¬n ≤ m

Tactic:
lia

Goal state after:
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
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : ¬n ≤ m + 1
h1' : ¬n ≤ m
⊢ n - m = n - (m + 1) + 1

Tactic:
lia

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ verschiebung x = frobenius (verschiebung x)

Tactic:
frobenius_zmodp

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ verschiebung x = verschiebung x
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
rw [Finset.mem_range]

Goal state after:
case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ¬0 < n + 1 → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f (dickson k a 0) = dickson k (f a) 0

Tactic:
by
    simp_rw [dickson_zero, Polynomial.map_sub, Polynomial.map_natCast, Polynomial.map_ofNat]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
h_le : k ≤ n
m : ℕ
hm : n - k = m + m
⊢ n = 2 * m + k

Tactic:
lia

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

Goal state before:
pp: n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ n ≤ n + x

Tactic:
lia

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

Goal state before:
pp: n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ n + x - n = x

Tactic:
lia

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

Goal state before:
pp: case refine_2
n : ℕ
⊢ (shiftedLegendre n).coeff n ≠ 0

Tactic:
simp [coeff_shiftedLegendre, (choose_pos (show n ≤ n + n by simp)).ne']

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

Goal state before:
pp: n : ℕ
⊢ (-1) ^ n * (shiftedLegendre n).comp (1 - X) = shiftedLegendre n

Tactic:
refine nat_mul_inj' ?_ (factorial_ne_zero n)

Goal state after:
n : ℕ
⊢ ↑n ! * ((-1) ^ n * (shiftedLegendre n).comp (1 - X)) = ↑n ! * shiftedLegendre n
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : 0 < x
⊢ 0 < x

Tactic:
lia

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ f + 0 = f

Tactic:
by ext; simp only [add_def, add_zero, zero_def]

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

Goal state before:
pp: n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
⊢ 0 < n

Tactic:
lia

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

Goal state before:
pp: n : ℕ
hn : 0 < n
this✝ :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
this :
  (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) =
    ∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder
⊢ n = n - 1 + 1

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ 0 < n

Tactic:
lia

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
inst✝ : IsLocalRing A
hg : (map (IsLocalRing.residue A)) g ≠ 0
h : (coeff ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat) g ∈ IsLocalRing.maximalIdeal A
⊢ (IsLocalRing.residue A) ((coeff ((map (IsLocalRing.residue A)) g).order.toNat) g) = 0

Tactic:
IsLocalRing.residue_eq_zero_iff

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
inst✝ : IsLocalRing A
hg : (map (IsLocalRing.residue A)) g ≠ 0
h : (coeff ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) g).order.toNat) g ∈ IsLocalRing.maximalIdeal A
⊢ (coeff ((map (IsLocalRing.residue A)) g).order.toNat) g ∈ IsLocalRing.maximalIdeal A
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
⊢ ∃ A, ∃ (_ : A.FG), ∃ u, (LinearMap.baseChange (↥A) f) u = 0 ∧ (rTensor M A.val.toLinearMap) u = t

Tactic:
by
  obtain ⟨A, hA, ht_memA⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨u, hu⟩ := _root_.id ht_memA
  have := TensorProduct.Algebra.eq_of_fg_of_subtype_eq hA (t := f.baseChange _ u) (t' := 0)
  simp only [map_zero, exists_and_left] at this
  have hu' : (A.val.toLinearMap.rTensor N) (f.baseChange (↥A) u) = 0 := by
    rw [← ht, ← hu, rTensor_baseChange]
  obtain ⟨B, hB, hAB, hu'⟩ := this hu'
  use B, hB, rTensor M (Subalgebra.inclusion hAB).toLinearMap u
  constructor
  · rw [← rTensor_baseChange, hu']
  · rw [← comp_apply, ← rTensor_comp, ← hu]
    congr

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ ↑p.1 < ((map (IsLocalRing.residue A)) g).order

Tactic:
rw [← ENat.lt_lift_iff (h := order_finite_iff_ne_zero.2 hg), ENat.lift_eq_toNat_of_lt_top]

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ p.1 < ((map (IsLocalRing.residue A)) g).order.toNat
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case refine_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
this : X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = g
⊢ X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = (X ^ n - ↑r) * ↑⋯.unit⁻¹

Tactic:
sub_mul

Goal state after: