mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
i : σ
hi : ¬p ∣ n i
⊢ (coeff n) ((expand p hp) ↑φ) = MvPolynomial.coeff n ((MvPolynomial.expand p) φ)

Tactic:
rw [coeff_expand_of_not_dvd p hp _ hi, MvPolynomial.coeff_expand_of_not_dvd _ hi]

Goal state after:
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
d : σ →₀ ℕ
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

Tactic:
by_cases! h : ∀ i, p ∣ d i

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))

case neg
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∃ i, ¬p ∣ d i
⊢ MvPolynomial.coeff d ((trunc' R (p • n)) ((expand p hp) φ)) =
    MvPolynomial.coeff d ((MvPolynomial.expand p) ((trunc' R n) φ))
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
let : UniformSpace (ratfuncAdicComplPkg (K := K).space) :=
      ratfuncAdicComplPkg.uniformStruct

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
i : Fin n
x✝ : i ∈ Finset.univ
⊢ v i.succ * (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ up ^ ↑i.succ).natDegree = up ^ ↑i.succ * v i.succ

Tactic:
by
    rw [add_comm (Polynomial.C _), natDegree_X_pow_add_C, mul_comm]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : NeZero p
n : ℕ
⊢ (W_ R n).vars ⊆ range (n + 1)

Tactic:
rw [← map_wittPolynomial p (Int.castRingHom R), ← wittPolynomial_vars p ℤ]

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : NeZero p
n : ℕ
⊢ ((map (Int.castRingHom R)) (W_ ℤ n)).vars ⊆ (W_ ℤ n).vars
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * -∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0

Tactic:
mul_neg,

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ -(⅟↑p ^ n * ∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
⊢ (X 0 - 0) * 1 = X 0

Tactic:
mul_one,

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
⊢ X 0 - 0 = X 0
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) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ Ideal.map (T f) I =
    Ideal.map (↑(MvPolynomial.finSuccEquiv k n).symm) (Ideal.map (MvPolynomial.finSuccEquiv k n) (Ideal.map (T f) I))

Tactic:
by
  set g := (finSuccEquiv k n)
  have : g.symm.toRingEquiv.toRingHom.comp g = RingHom.id _ :=
    g.toRingEquiv.symm_toRingHom_comp_toRingHom
  calc
    _ = Ideal.map ((RingHom.id _).comp <| T f) I := by rw [id_comp, Ideal.map_coe]
    _ = (I.map (T f)).map (RingHom.id _) := by simp only [← Ideal.map_map, Ideal.map_coe]
    _ = (I.map (T f)).map (g.symm.toAlgHom.toRingHom.comp g) :=
      congrFun (congrArg Ideal.map this.symm) (I.map (T f))
    _ = _ := by simp [← Ideal.map_map, Ideal.map_coe]

Goal state after:
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
⊢ (Ideal.Quotient.mk I) ((teichmuller p I) x) = (coeff (R ⧸ I) p 0) x

Tactic:
by
  have := teichmuller_sModEq <| Ideal.Quotient.mk_out <| coeff _ p 0 x
  simp_rw [zero_add, pow_one] at this
  simpa [SModEq.idealQuotientMk] using this

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ (map f) x = 0 ↔ ∀ (n : ℕ), f (x.coeff n) = 0

Tactic:
refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : (map f) x = 0
n : ℕ
⊢ f (x.coeff n) = 0

case refine_2
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : ∀ (n : ℕ), f (x.coeff n) = 0
⊢ (map f) x = 0
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑((Int.castRingHom ℚ)
            (coeff c
              ((bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) (W_ ℤ n)) Φ -
                ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))) /
          ↑↑(p ^ n)).num =
    (Int.castRingHom ℚ)
        (coeff c
          ((bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) (W_ ℤ n)) Φ -
            ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))) /
      ↑↑(p ^ n)

Tactic:
rw [← Rat.den_eq_one_iff, eq_intCast, Rat.den_div_intCast_eq_one_iff]

Goal state after:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ∣
    coeff c
      ((bind₁ fun i ↦ (rename fun i_1 ↦ (i, i_1)) (W_ ℤ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))

case h.hn
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ≠ 0
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C 1 * X n ^ p + C (↑p * 1) * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)

Tactic:
mul_one,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C 1 * X n ^ p + C ↑p * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
⊢ verschiebungFun 0 = 0

Tactic:
ext ⟨⟩ <;> rw [verschiebungFun_coeff]

Goal state after:
case zero
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
⊢ (if 0 = 0 then 0 else coeff 0 (0 - 1)) = coeff 0 0

case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n✝ : ℕ
⊢ (if n✝ + 1 = 0 then 0 else coeff 0 (n✝ + 1 - 1)) = coeff 0 (n✝ + 1)
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ (x * ↑n + x * 1).coeff k = (aeval x.coeff) ((fun k ↦ (bind₁ (Function.uncurry ![wittMulN p n, X])) (wittAdd p k)) k)

Tactic:
mul_one,

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ (x * ↑n + x).coeff k = (aeval x.coeff) ((fun k ↦ (bind₁ (Function.uncurry ![wittMulN p n, X])) (wittAdd p k)) k)
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)) +
            (X i ^ p) ^ p ^ (n - i) * 1) *
        C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n + 1 - 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:
mul_one,

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)) +
            (X i ^ p) ^ p ^ (n - i)) *
        C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n + 1 - 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))))
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 y : 𝕎 R
i j : ℕ
⊢ ((⇑verschiebung)^[i] x * (⇑verschiebung)^[j] y).coeff (i + j) = x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i

Tactic:
calc
    _ = (verschiebung^[i + j] (frobenius^[j] x * frobenius^[i] y)).coeff (i + j) := ?_
    _ = (frobenius^[j] x * frobenius^[i] y).coeff 0 := ?_
    _ = (frobenius^[j] x).coeff 0 * (frobenius^[i] y).coeff 0 := ?_
    _ = _ := ?_
  · rw [iterate_verschiebung_mul]
  · convert! iterate_verschiebung_coeff (p := p) (R := R) _ _ _ using 2
    rw [zero_add]
  · apply mul_coeff_zero
  · simp only [iterate_frobenius_coeff]

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

Goal state before:
pp: case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ x.coeff ↑⟨i, hi⟩ = x.coeff i

Tactic:
Fin.val_mk

Goal state after:
case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ x.coeff i = x.coeff i
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
hp : Nat.Prime p
⊢ IsDomain (PreTilt O p)

Tactic:
have : Nontrivial (PreTilt O p) := ⟨(CharP.nontrivial_of_char_ne_one hp.ne_one).1⟩

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
hp : Nat.Prime p
this : Nontrivial (PreTilt O p)
⊢ IsDomain (PreTilt O p)
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
⊢ (factorPowSucc 𝔭 (n + 1)).comp (fontaineThetaModPPow R p (n + 1)) = fontaineThetaModPPow R p n

Tactic:
apply eq_of_apply_teichmuller_eq ((factorPowSucc _ _).comp (fontaineThetaModPPow R p (n + 1)))
    (fontaineThetaModPPow R p n)

Goal state after:
case hp
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
⊢ IsNilpotent ↑p

case h
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
⊢ ∀ (x : R♭),
    ((factorPowSucc 𝔭 (n + 1)).comp (fontaineThetaModPPow R p (n + 1))) ((teichmuller p) x) =
      (fontaineThetaModPPow R p n) ((teichmuller p) x)
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n : ℕ
⊢ (hermite (n + 1)).coeff 0 = -(hermite n).coeff 1

Tactic:
by
  simp [coeff_derivative]

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

Goal state before:
pp: case zero
k : ℕ
⊢ (hermite 0).coeff (0 + k + 1) = 0

Tactic:
exact coeff_C

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

Goal state before:
pp: case zero
⊢ (hermite 0).coeff 0 = 1

Tactic:
exact coeff_C

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 : Infinite K
⊢ map (ZMod.castHom ⋯ K) (dickson 1 1 p) = map (ZMod.castHom ⋯ K) (X ^ p)

Tactic:
map_dickson,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 ((ZMod.castHom ⋯ K) 1) p = map (ZMod.castHom ⋯ K) (X ^ p)
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0} ⊆ {x | eval x (dickson 1 ((ZMod.castHom ⋯ K) 1) p) = eval x (X ^ p)}

pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Infinite

Tactic:
· rintro _ ⟨x, rfl, hx⟩
    simp only [eval_X, eval_pow, Set.mem_ofPred_eq, ZMod.cast_one', add_pow_char,
      dickson_one_one_eval_add_inv _ _ (mul_inv_cancel₀ hx), ZMod.castHom_apply]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
have hp : p ≠ 0 := by
    intro h
    rw [h] at hh
    exact hh (hilbertPoly_zero_left d)

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

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

Tactic:
rw [Finset.mem_range] at hm

Goal state after:
case e_a.a.h
n m : ℕ
hm : m < n + 1
⊢ m ≤ n
Module: Mathlib.RingTheory.PowerSeries.Catalan

Goal state before:
pp: n : ℕ
⊢ (coeff n) (catalanSeries ^ 2 * X + 1) = (coeff n) catalanSeries

Tactic:
cases n with
  | zero => simp
  | succ n =>
    simp_rw [add_comm, map_add, coeff_one, if_neg n.succ_ne_zero, zero_add, coeff_succ_mul_X, sq,
      coeff_mul, catalanSeries_coeff, catalan_succ']

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

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

Tactic:
simp only [coeff_largeSchroderSeries, coeff_X_mul_largeSchroderSeries n hn, tsub_self,
    largeSchroder_zero, mul_one]

Goal state after:
n : ℕ
hn : 0 < n
⊢ ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder + (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inr.refine_1
z : ℤ
hz : z ≠ 0
p : ℕ
x✝ : Prime ↑p ∧ 0 ≤ ↑p ∧ ↑p ∣ z
pp : Nat.Prime p
dp : p ∣ z.natAbs
⊢ ∃ a ∈ z.natAbs.primeFactors, Nat.castEmbedding.toFun a = ↑p

Tactic:
exact ⟨p, by simp_all, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
⊢ Free R M

Tactic:
have surjg : Function.Surjective g := by
    apply g.surjective_of_surjective_comp_mkQ (Ideal.span {x}) lejac
    rwa [Submodule.ideal_span_singleton_smul x ⊤, hg]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
⊢ Free R M
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
⊢ s + g * -(s₁ * ↑⋯.unit⁻¹) = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹

Tactic:
mul_neg,

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

Goal state before:
pp: case inl
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
f : A[X] ⧸ Ideal.span {g}
h✝ : Subsingleton A
this : Subsingleton A[X]
⊢ (⇑(Ideal.Quotient.mk (Ideal.span {g})) ∘ ⇑⋯.mod')
      ((↑↑(Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯).toRingHom).toFun f) =
    f

Tactic:
have : Subsingleton (A[X] ⧸ Ideal.span {g}) := Quot.Subsingleton

Goal state after:
case inl
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
f : A[X] ⧸ Ideal.span {g}
h✝ : Subsingleton A
this✝ : Subsingleton A[X]
this : Subsingleton (A[X] ⧸ Ideal.span {g})
⊢ (⇑(Ideal.Quotient.mk (Ideal.span {g})) ∘ ⇑⋯.mod')
      ((↑↑(Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯).toRingHom).toFun f) =
    f
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg : ¬(map (IsLocalRing.residue A)) g ≠ 0
⊢ Polynomial.degree 0 < ↑((map (IsLocalRing.residue A)) g).order.toNat

Tactic:
nontriviality A

Goal state after:
case neg
A : Type u_1
inst✝³ : CommRing A
inst✝² : IsLocalRing A
f g : A⟦X⟧
inst✝¹ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg : ¬(map (IsLocalRing.residue A)) g ≠ 0
inst✝ : Nontrivial A
⊢ Polynomial.degree 0 < ↑((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⁻¹ = g * 1 + ↑r * ↑⋯.unit⁻¹
⊢ g = ↑f * ↑⋯.unit⁻¹

Tactic:
mul_one,

Goal state after:
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⁻¹ = g + ↑r * ↑⋯.unit⁻¹
⊢ g = ↑f * ↑⋯.unit⁻¹