mathlib-initiative/mathlib-tactics huggingface dataset:
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:
← log_le_iff_le_exp one_ne_zero,

Goal state after:
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 : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
hDs : D + ↑s ≤ 0
⊢ log 1 ≤ -(D + ↑s)
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
h₀ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : ↑s ∉ P
h₂ : (algebraMap S Sₚ) ↑s ∉ Ideal.map (algebraMap S Sₚ) P
⊢ (algebraMap S Sₚ) ↑s * (algebraMap S Sₚ) (x * s') - mk' Sₚ (↑s * x) s ∈ Ideal.map (algebraMap S Sₚ) P

Tactic:
mk'_mul_cancel_left,

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs : (Ideal.Quotient.mk P) s' = ((Ideal.Quotient.mk P) ↑s)⁻¹
h₀ : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : ↑s ∉ P
h₂ : (algebraMap S Sₚ) ↑s ∉ Ideal.map (algebraMap S Sₚ) P
⊢ (algebraMap S Sₚ) ↑s * (algebraMap S Sₚ) (x * s') - (algebraMap S Sₚ) x ∈ Ideal.map (algebraMap S Sₚ) P
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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = ↑s
hDs : D - ↑s ≤ 0
⊢ 1 ≤ exp (-D + ↑s)

Tactic:
← log_le_iff_le_exp one_ne_zero,

Goal state after:
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
⊢ log 1 ≤ -D + ↑s
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
Sₚ : Type u_4
inst✝³ : CommRing Sₚ
inst✝² : Algebra S Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝ : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
h₁ : (Ideal.Quotient.mk P) ↑s ≠ 0
⊢ (equivQuotientMapOfIsMaximal p Sₚ P) ((Ideal.Quotient.mk P) ↑s) ≠ 0

Tactic:
rwa [RingEquiv.map_ne_zero_iff]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
refine ⟨0, fun x hg ↦ ?_⟩
      rw [hf, sub_zero] at hg
      exact (valuation_le_iff_coeff_lt_eq_zero K).mp hg

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

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

Tactic:
rw [accumulate_rec (him.trans_le hmn) hi, ih hi, invAccumulate, dif_pos him, dif_pos hi]

Goal state after:
case refine_1
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝¹ : Fin m
i✝ : ℕ
this : i✝ ≤ m - 1
i : ℕ
hi : i + 1 < m
x✝ : i✝ ≤ i
ih : ∀ (hi : i + 1 < m), (accumulate n m) (invAccumulate n m s) ⟨i + 1, hi⟩ = s ⟨i + 1, hi⟩
him : i < m
⊢ s ⟨↑⟨i, ⋯⟩, him⟩ - s ⟨↑⟨i, ⋯⟩ + 1, hi⟩ + s ⟨i + 1, hi⟩ = s ⟨i, him⟩
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hp.a
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
⊢ (sumSMulX c).totalDegree ≤ 1

pp: case a
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
⊢ 1 ≤ (sumSMulX c).totalDegree

Tactic:
· simp only [sumSMulX, Finsupp.linearCombination_apply, Finsupp.sum]
      apply totalDegree_finsetSum_le
      intros
      apply le_trans (totalDegree_smul_le ..)
      simp

Goal state after:
case a
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
⊢ 1 ≤ (sumSMulX c).totalDegree
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 : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
⊢ Irreducible (sumSMulXSMulY c)

Tactic:
have aux : sumSMulXSMulY c = .ofCoeff (c.embDomain ι) := by
    rw [← Finsupp.sum_single (Finsupp.embDomain _ _)]
    simp [Finsupp.sum_embDomain, sumSMulXSMulY, X, monomial_mul,
      Finsupp.linearCombination_apply, smul_monomial, ι]
    rfl

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
⊢ Irreducible (sumSMulXSMulY c)
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
⊢ Valued.v.restrict x ≠ 0

Tactic:
by
        rw [Valuation.restrict_def, ne_eq, restrict₀_eq_zero_iff]; simp [hx]

Goal state after:
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 ⇑(esymmAlgHom σ R n)

Tactic:
rw [← rename_esymmAlgHom (Fintype.equivFin σ).symm, AlgHom.coe_comp]

Goal state after:
σ : 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))
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : Fintype.card σ ≤ n
⊢ Function.Surjective ⇑(esymmAlgHom σ R n)

Tactic:
rw [← rename_esymmAlgHom (Fintype.equivFin σ).symm, AlgHom.coe_comp]

Goal state after:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : Fintype.card σ ≤ n
⊢ Function.Surjective
    (⇑↑(renameSymmetricSubalgebra (Fintype.equivFin σ).symm) ∘ ⇑(esymmAlgHom (Fin (Fintype.card σ)) R n))
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ m i
⊢ (coeff m) ((expand p hp) φ) = 0

Tactic:
by
  classical
  contrapose! h
  simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp)] at h
  obtain ⟨d, hd⟩ : ∃ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) ≠ 0 := by
    by_contra! hc
    rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h
    contradiction
  have : (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
  rw [this, coeff_monomial] at hd
  have meq : m = p • d := by
    by_contra hc
    rw [if_neg hc] at hd
    contradiction
  simp [meq]

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
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
x : adicCompletion K⟮X⟯ (idealX K)
hx : Valued.v x = γ
⊢ {x_1 | Valued.v.restrict x_1 < ↑(Units.mk0 (Valued.v.restrict x) ⋯)} ⊆ {t | Valued.v t < γ}

Tactic:
simp [Units.val_mk0, Valuation.restrict_lt_iff, hx]

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
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
⊢ ∀ᶠ (b : adicCompletion K⟮X⟯ (idealX K)) in 𝓝 a,
    ∀ (a_1 : K⟮X⟯),
      { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm a_1) } = b → Valued.v a_1 = Valued.v a

Tactic:
Filter.Eventually,

Goal state after:
case neg
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
⊢ {x |
      ∀ (a_1 : K⟮X⟯),
        { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm a_1) } = x → Valued.v a_1 = Valued.v a} ∈
    𝓝 a
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
⊢ ∀ (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

Tactic:
rintro y val_y b rfl

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
b : K⟮X⟯
val_y :
  Valued.v.restrict ({ toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm b) } - a) <
    Valued.v.restrict a
⊢ (valuation K⟮X⟯ (idealX K)) b = Valued.v a
Module: Mathlib.RingTheory.WittVector.WittPolynomial

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

Tactic:
C_0,

Goal state after:
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))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i ↦ {i})

Tactic:
intro a b h

Goal state after:
case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
a b : ℕ
h : a ≠ b
⊢ Function.onFun Disjoint (fun i ↦ {i}) a b
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: 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
i : ℕ
hi : i ∈ (W_ ℚ n).vars
⊢ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
    (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))

Tactic:
rw [wittPolynomial_vars, Finset.mem_range] at hi

Goal state after:
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
i : ℕ
hi : i < n + 1
⊢ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
    (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ x.verschiebungFun.coeff 0 = 0

Tactic:
verschiebungFun_coeff,

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ (if 0 = 0 then 0 else x.coeff (0 - 1)) = 0
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∑ k ∈ Finset.range (n + 1), ↑p ^ (k + 1) * x.verschiebungFun.coeff (k + 1) ^ p ^ (n + 1 - (k + 1)) +
      ↑p ^ 0 * x.verschiebungFun.coeff 0 ^ p ^ (n + 1 - 0) =
    ↑p * ∑ i ∈ Finset.range (n + 1), ↑p ^ i * x.coeff i ^ p ^ (n - i)

Tactic:
verschiebungFun_coeff,

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∑ k ∈ Finset.range (n + 1), ↑p ^ (k + 1) * x.verschiebungFun.coeff (k + 1) ^ p ^ (n + 1 - (k + 1)) +
      ↑p ^ 0 * (if 0 = 0 then 0 else x.coeff (0 - 1)) ^ p ^ (n + 1 - 0) =
    ↑p * ∑ i ∈ Finset.range (n + 1), ↑p ^ i * x.coeff i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.Identities

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

Tactic:
rw [pow_succ, ← mul_assoc, ← add_assoc, mul_charP_coeff_succ, pow_succ, pow_mul]

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ n).coeff (m + n) ^ p = (x.coeff m ^ p ^ n) ^ p
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPoly p n) = frobeniusPolyRat p n

Tactic:
rw [frobeniusPoly, map_add, map_mul, map_pow, map_C, map_X, eq_intCast, Int.cast_natCast,
    frobeniusPolyRat]
  refine Nat.strong_induction_on n ?_; clear n
  intro n IH
  rw [xInTermsOfW_eq]
  simp only [map_sum, map_sub, map_mul, map_pow (bind₁ _), bind₁_C_right]
  have h1 : (p : ℚ) ^ n * ⅟(p : ℚ) ^ n = 1 := by rw [← mul_pow, mul_invOf_self, one_pow]
  rw [bind₁_X_right, Function.comp_apply, wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ,
    sum_range_succ, tsub_self, add_tsub_cancel_left, pow_zero, pow_one, pow_one, sub_mul, add_mul,
    add_mul, mul_right_comm, mul_right_comm (C ((p : ℚ) ^ (n + 1))), ← C_mul, ← C_mul, pow_succ',
    mul_assoc (p : ℚ) ((p : ℚ) ^ n), h1, mul_one, C_1, one_mul, add_comm _ (X n ^ p), add_assoc,
    ← add_sub, add_right_inj, frobeniusPolyAux_eq, map_sub, map_X, mul_sub, sub_eq_add_neg,
    add_comm _ (C (p : ℚ) * X (n + 1)), ← add_sub,
    add_right_inj, neg_eq_iff_eq_neg, neg_sub, eq_comm]
  simp only [map_sum, mul_sum, sum_mul, ← sum_sub_distrib]
  apply sum_congr rfl
  intro i hi
  rw [mem_range] at hi
  rw [← IH i hi]
  clear IH
  rw [add_comm (X i ^ p), add_pow, sum_range_succ', pow_zero, tsub_zero, Nat.choose_zero_right,
    one_mul, Nat.cast_one, mul_one, mul_add, add_mul, Nat.succ_sub (le_of_lt hi),
    Nat.succ_eq_add_one (n - i), pow_succ', pow_mul, add_sub_cancel_right, mul_sum, sum_mul]
  apply sum_congr rfl
  intro j hj
  rw [mem_range] at hj
  rw [map_mul, map_mul, map_pow, map_pow, map_pow, map_pow, map_pow, map_C, map_X, mul_pow]
  rw [mul_comm (C (p : ℚ) ^ i), mul_comm _ ((X i ^ p) ^ _), mul_comm (C (p : ℚ) ^ (j + 1)),
    mul_comm (C (p : ℚ))]
  simp only [mul_assoc]
  apply congr_arg
  apply congr_arg
  rw [← C_eq_coe_nat]
  simp only [← map_pow, ← C_mul]
  rw [C_inj]
  simp only [invOf_eq_inv, eq_intCast, inv_pow, Int.cast_natCast, Nat.cast_mul, Int.cast_mul]
  rw [Rat.natCast_div _ _ (map_frobeniusPoly.key₁ p (n - i) j hj)]
  push_cast
  linear_combination (norm := skip) -p / p ^ n / p ^ (n - i - v p (j + 1))
    * (p ^ (n - i)).choose (j + 1) * congr((p : ℚ) ^ $(map_frobeniusPoly.key₂ p hi.le hj))
  field [hp.1.ne_zero]

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n : ℕ
⊢ ((map (_root_.frobenius R p)) ((map ↑(_root_.frobeniusEquiv R p).symm) f)).coeff n = f.coeff n

Tactic:
exact frobenius_apply_frobeniusEquiv_symm R p _

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n : ℕ
⊢ (frobenius ((map ↑(_root_.frobeniusEquiv R p).symm) f)).coeff n = f.coeff n

Tactic:
rw [frobenius_eq_map_frobenius]
      exact frobenius_apply_frobeniusEquiv_symm R p _

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

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
⊢ (verschiebung (x.shift k.succ)).coeff 0 = (x.shift k).coeff 0

Tactic:
rw [verschiebung_coeff_zero, shift_coeff, h]
    apply Nat.lt_succ_self

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : TruncatedWittVector p n₃ R
⊢ (truncate h1) ((truncate h2) x) = (truncate ⋯) x

Tactic:
obtain ⟨x, rfl⟩ := WittVector.truncate_surjective (p := p) n₃ R x

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : 𝕎 R
⊢ (truncate h1) ((truncate h2) ((WittVector.truncate n₃) x)) = (truncate ⋯) ((WittVector.truncate n₃) x)
Module: Mathlib.RingTheory.Perfectoid.BDeRham

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) R
⊢ IsUnit (((algebraMap R (Localization.Away ↑p)).comp (fontaineTheta R p)) ↑p)

Tactic:
by simpa using IsLocalization.Away.algebraMap_isUnit (p : R)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
g : ℕ → R := fun x ↦ 0
b : ℕ
hb : b ≤ n ∧ ¬b = i
⊢ ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ b) (x.coeff b)) * ↑p ^ b).coeff i = g b

Tactic:
exact teichmuller_mul_pow_coeff_of_ne _ (Ne.intro hb.2).symm

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
⊢ x ∈ ⋃ x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}, {y | x = y + y⁻¹ ∨ y = 0}

Tactic:
simp only [exists_prop, Set.mem_iUnion, Ne, Set.mem_ofPred_eq]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
i : ↥p.support
⊢ eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)

Tactic:
rw [preHilbertPoly_eq_choose_sub_add _ _ (h_le i), Nat.sub_add_comm (h_le i)]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : Rᵐᵒᵖ
n : ℕ
⊢ op ((monomial n) (unop r)) = op (C (unop r) * X ^ n)

Tactic:
C_mul_X_pow_eq_monomial

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : Rᵐᵒᵖ
n : ℕ
⊢ op ((monomial n) (unop r)) = op ((monomial n) (unop r))
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case h.right
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
n : ℕ
hn : n ∈ Set.Ioi (max N p.natDegree)
⊢ ↑n ∈ {x | eval x h = eval x (p.hilbertPoly d)}

Tactic:
simp only [Set.mem_Ioi, sup_lt_iff, Set.mem_ofPred_eq] at hn ⊢

Goal state after:
case h.right
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
n : ℕ
hn : N < n ∧ p.natDegree < n
⊢ eval (↑n) h = eval (↑n) (p.hilbertPoly d)
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
⊢ False

Tactic:
replace h3 : z ^ 3 = 1 := by
    linear_combination (1 - z - z ^ 2 - z ^ n) * h1 + (z ^ n - 2) * h2

Goal state after:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Catalan

Goal state before:
pp: ⊢ constantCoeff catalanSeries = 1

Tactic:
rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply]
  simp only [catalanSeries_coeff, catalan_zero]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
Q : { Q // Q.FG }
u : M ⊗[R] ↥↑Q
p : M
n : ↥↑Q
⊢ ((AlgebraTensorModule.curry
          (↑(directLimit R M N) ∘ₗ
            Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q))
        p)
      n =
    ((AlgebraTensorModule.curry (lTensor M (↑Q).subtype)) p) n

Tactic:
simp [Submodule.FG.lTensor.directLimit, Submodule.FG.directLimit]

Goal state after: