mathlib-initiative/mathlib-tactics huggingface dataset:
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
a : ℕ × ℕ
ha : a.1 + a.2 = k
left✝ : a.1 < k
ha0 : ¬0 < a.1
⊢ a = (0, k)

Tactic:
← ha,

Goal state after:
σ : 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
a : ℕ × ℕ
ha : a.1 + a.2 = k
left✝ : a.1 < k
ha0 : ¬0 < a.1
⊢ a = (0, a.1 + a.2)
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) (h v)) +
        ∑ x ∈ f.support \ {v}, (MvPolynomial.finSuccEquiv k n) ((T f) (h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff

Tactic:
rw [add_comm]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h x))).degree < ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).degree
⊢ (∑ x ∈ f.support \ {v}, (MvPolynomial.finSuccEquiv k n) ((T f) (h x)) +
        (MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((T f) (h v))).leadingCoeff
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ φ n = (bind₁ φ) ((bind₁ (W_ ℚ)) (xInTermsOfW p ℚ n))

Tactic:
bind₁_wittPolynomial_xInTermsOfW p,

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ φ n = (bind₁ φ) (X n)
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittNeg p 0 = -X (0, 0)

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittNeg, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero,
    map_neg, bind₁_X_right, map_wittStructureInt]

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 : ℕ
⊢ i ∈ Finset.range (n + 1) → ↑p ^ (n + 1) ∣ (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))

Tactic:
hi

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ↑p ^ (n + 1) ∣ (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))
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, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
⊢ i ∈ Finset.range n →
    (map (Int.castRingHom ℚ)) (C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
      C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)

Tactic:
hi

Goal state after:
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 × ℕ →₀ ℕ
i : ℕ
hi : i ∈ Finset.range n
⊢ (map (Int.castRingHom ℚ)) (C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ Function.Injective ⇑(Int.castRingHom ℚ)

Tactic:
intro m n

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
m n : ℤ
⊢ (Int.castRingHom ℚ) m = (Int.castRingHom ℚ) n → m = n
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
⊢ Function.Injective ⇑(Int.castRingHom ℚ)

Tactic:
intro m n

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n✝ : ℕ
m n : ℤ
⊢ (Int.castRingHom ℚ) m = (Int.castRingHom ℚ) n → m = 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
⊢ IsPoly p fun R _Rcr ↦ verschiebungFun

Tactic:
by
  use verschiebungPoly
  simp only [aeval_verschiebung_poly', forall₃_true_iff]

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
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
inst✝² : PerfectRing R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
f : R →+* Perfection S p
r : R
n : ℕ
⊢ (coeff S p n) (f ((⇑(frobenius R p))^[n] ((⇑(frobeniusEquiv R p).symm)^[n] r))) = (coeff S p n) (f r)

Tactic:
Function.RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm R p) n

Goal state after:
R✝ : Type u_1
inst✝⁶ : CommSemiring R✝
p : ℕ
hp : Fact (Nat.Prime p)
inst✝⁵ : CharP R✝ p
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
inst✝² : PerfectRing R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
f : R →+* Perfection S p
r : R
n : ℕ
⊢ (coeff S p n) (f r) = (coeff S p n) (f r)
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
i : ℕ
⊢ i ∈ range n →
    C (↑p ^ i) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ i) ^ 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))))

Tactic:
hi

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
i : ℕ
hi : i ∈ range n
⊢ C (↑p ^ i) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ i) ^ 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.Frobenius

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

Tactic:
rw [coeff_frobenius]
  let : Algebra (ZMod p) R := ZMod.algebra _ _
  -- outline of the calculation, proofs follow below
  calc
    aeval (fun k => x.coeff k) (frobeniusPoly p n) =
        aeval (fun k => x.coeff k)
          (MvPolynomial.map (Int.castRingHom (ZMod p)) (frobeniusPoly p n)) := ?_
    _ = aeval (fun k => x.coeff k) (X n ^ p : MvPolynomial ℕ (ZMod p)) := ?_
    _ = x.coeff n ^ p := ?_
  · conv_rhs => rw [aeval_eq_eval₂Hom, eval₂Hom_map_hom]
    apply eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
  · rw [frobeniusPoly_zmod]
  · rw [map_pow, aeval_X]

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

Goal state before:
pp: case calc_1
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) =
    ((⇑verschiebung)^[i + j] ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y)).coeff (i + j)

Tactic:
rw [iterate_verschiebung_mul]

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'

Tactic:
by
  classical
  have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
    by_contra! hall
    apply hx
    ext i
    simp only [hall, zero_coeff]
  let n := Nat.find hex
  use n, x.shift n
  refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩
  exact Nat.find_min hex hi

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung)^[nb] wb ≠ 0
⊢ wa.coeff 0 ^ p ^ nb * wb.coeff 0 ^ p ^ na ≠ coeff 0 (na + nb)

Tactic:
zero_coeff

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung)^[nb] wb ≠ 0
⊢ wa.coeff 0 ^ p ^ nb * wb.coeff 0 ^ p ^ na ≠ 0
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : ∀ i < m, x.coeff i = 0
i : ℕ
⊢ i < n → x.coeff i = 0

Tactic:
hi

Goal state after:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : ∀ i < m, x.coeff i = 0
i : ℕ
hi : i < n
⊢ x.coeff i = 0
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ((teichmuller p) 0).coeff 0 = coeff 0 0

Tactic:
zero_coeff

Goal state after:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ((teichmuller p) 0).coeff 0 = 0
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n✝ : ℕ
⊢ ((teichmuller p) 0).coeff (n✝ + 1) = coeff 0 (n✝ + 1)

Tactic:
zero_coeff

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n✝ : ℕ
⊢ ((teichmuller p) 0).coeff (n✝ + 1) = 0
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ init n x + tail n x = x

Tactic:
by
  simp only [init, tail, ← not_lt, select_add_select_not]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ (⇑verschiebung)^[n] (x.shift n) =
    (⇑verschiebung)^[n] ((⇑frobenius)^[n] ((⇑(frobeniusEquiv p k).symm)^[n] (x.shift n)))

Tactic:
by
      congr
      rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]
      · rw [← WittVector.frobeniusEquiv_apply, ← RingEquiv.coe_trans]
        simp
      · rw [Function.Commute, Function.Semiconj, ← WittVector.frobeniusEquiv_apply]
        simp only [RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply, implies_true]

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : ℕ → 𝕎 k
n : ℕ
h : ∀ {m n : ℕ}, m ≤ n → ∀ i < m, (x m).coeff i = (x n).coeff i
i : ℕ
⊢ i < n → (x n).coeff i = (mk p fun n ↦ (x (n + 1)).coeff n).coeff i

Tactic:
hi

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : ℕ → 𝕎 k
n : ℕ
h : ∀ {m n : ℕ}, m ≤ n → ∀ i < m, (x m).coeff i = (x n).coeff i
i : ℕ
hi : i < n
⊢ (x n).coeff i = (mk p fun n ↦ (x (n + 1)).coeff n).coeff i
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 : ℕ
⊢ i < n + 1 →
    x.coeff i = (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i).coeff i

Tactic:
hi

Goal state after:
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
⊢ x.coeff i = (∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i).coeff i
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (2 + n) = X * dickson k a (2 + n - 1) - C a * dickson k a (2 + n - 2)

Tactic:
rw [add_comm]

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (n + 2) = X * dickson k a (n + 2 - 1) - C a * dickson k a (n + 2 - 2)
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 : ℕ
⊢ ↑p ^ (n + 1) ∣ x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i

Tactic:
by
  rw [← Ideal.mem_span_singleton, mem_span_p_pow_iff_le_coeff_eq_zero,
      ← le_coeff_eq_iff_le_sub_coeff_eq_zero]
  intro i hi
  rw [WittVector.sum_coeff_eq_coeff_sum]
  · rw [Finset.sum_eq_add_sum_sdiff_singleton_of_mem (Finset.mem_Iic.mpr (Nat.lt_succ_iff.mp hi))]
    let g := fun x : ℕ ↦ (0 : R)
    rw [Finset.sum_congr rfl (g := g)]
    · simp [g]
    · intro b hb
      simp only [Finset.mem_sdiff, Finset.mem_Iic, Finset.mem_singleton] at hb
      exact teichmuller_mul_pow_coeff_of_ne _ (Ne.intro hb.2).symm
  · refine fun n ↦ ⟨fun ⟨a, _, ha⟩ ⟨b, _, hb⟩ ↦ ?_⟩
    ext
    dsimp only [ne_eq, Set.mem_ofPred_eq]
    rw [← Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) ha]
    exact Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) hb

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑2 = 1

Tactic:
norm_num

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
⊢ eval (x + y) (3 - ↑1) = 1 + 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : PowerSeries.constantCoeff h ∉ I
eq : f = ↑g * h
this : Nontrivial R
mapf : (PowerSeries.map (Ideal.Quotient.mk I)) f = ↑(X ^ g.natDegree) * (PowerSeries.map (Ideal.Quotient.mk I)) h
i : ℕ
⊢ i < g.natDegree → (PowerSeries.coeff i) ((PowerSeries.map (Ideal.Quotient.mk I)) f) = 0

Tactic:
hi

Goal state after:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : PowerSeries.constantCoeff h ∉ I
eq : f = ↑g * h
this : Nontrivial R
mapf : (PowerSeries.map (Ideal.Quotient.mk I)) f = ↑(X ^ g.natDegree) * (PowerSeries.map (Ideal.Quotient.mk I)) h
i : ℕ
hi : i < g.natDegree
⊢ (PowerSeries.coeff i) ((PowerSeries.map (Ideal.Quotient.mk I)) f) = 0
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑1 = Chebyshev.C R ↑0

Tactic:
norm_num

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑2 = Chebyshev.S R ↑0

Tactic:
norm_num

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
⊢ ∃ K x, ∃ (_ : CharP K p), Infinite K

Tactic:
let f : ZMod p →+* K := (algebraMap _ (FractionRing _)).comp C

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
⊢ ∃ K x, ∃ (_ : CharP K p), Infinite K
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∃ K x, ∃ (_ : CharP K p), Infinite K

Tactic:
let K := FractionRing (Polynomial (ZMod p))
    let f : ZMod p →+* K := (algebraMap _ (FractionRing _)).comp C
    have : CharP K p := by
      rw [← f.charP_iff_charP]
      infer_instance
    have : Infinite K :=
      Infinite.of_injective (algebraMap (Polynomial (ZMod p)) (FractionRing (Polynomial (ZMod p))))
        (IsFractionRing.injective _ _)
    refine ⟨K, ?_, ?_, ?_⟩ <;> infer_instance

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

Goal state before:
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:
intro h
    rw [← Set.infinite_univ_iff] at H
    apply H
    -- To each `x` of the form `x = y + y⁻¹`
    -- we `bind` the set of `y` that solve the equation `x = y + y⁻¹`.
    -- For every `x`, that set is finite (since it is governed by a quadratic equation).
    -- For the moment, we claim that all these sets together cover `K`.
    suffices (Set.univ : Set K) =
        ⋃ x ∈ { x : K | ∃ y : K, x = y + y⁻¹ ∧ y ≠ 0 }, { y | x = y + y⁻¹ ∨ y = 0 }  by
      rw [this]
      clear this
      refine h.biUnion fun x _ => ?_
      -- The following quadratic polynomial has as solutions the `y` for which `x = y + y⁻¹`.
      let φ : K[X] := X ^ 2 - C x * X + 1
      have hφ : φ ≠ 0 := by
        intro H
        have : φ.eval 0 = 0 := by rw [H, eval_zero]
        simpa [φ, eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, eval_mul,
          mul_zero, sq, zero_add, one_ne_zero]
      classical
        convert! (φ.roots ∪ {0}).toFinset.finite_toSet using 1
        ext1 y
        simp only [φ, Multiset.mem_toFinset, Set.mem_ofPred_eq, Finset.mem_coe, Multiset.mem_union,
          mem_roots hφ, IsRoot, eval_add, eval_sub, eval_pow, eval_mul, eval_X, eval_C, eval_one,
          Multiset.mem_singleton]
        by_cases hy : y = 0
        · simp only [hy, or_true]
        apply or_congr _ Iff.rfl
        rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel₀ hy]
        apply eq_iff_eq_cancel_right.mpr
        ring
    -- Finally, we prove the claim that our finite union of finite sets covers all of `K`.
    apply (Set.eq_univ_of_forall _).symm
    intro x
    simp only [exists_prop, Set.mem_iUnion, Ne, Set.mem_ofPred_eq]
    by_cases hx : x = 0
    · simp only [hx, and_true, inv_zero, or_true]
      exact ⟨_, 1, rfl, one_ne_zero⟩
    · simp only [hx, or_false, exists_eq_right]
      exact ⟨_, rfl, hx⟩

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

Goal state before:
pp: case inr.inr
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ False

Tactic:
· exact z_ne_zero (eq_zero_of_pow_eq_zero (by rwa [key, add_self_eq_zero] at h2))

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

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, (coeff i) f ∈ I
hg : ∀ i ≤ n, (coeff i) g ∈ J
i : ℕ
hi : i ≤ n
⊢ (coeff i) (f * g) ∈ I * J

Tactic:
rw [coeff_mul]

Goal state after:
A : Type u_1
inst✝ : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, (coeff i) f ∈ I
hg : ∀ i ≤ n, (coeff i) g ∈ J
i : ℕ
hi : i ≤ n
⊢ ∑ p ∈ Finset.antidiagonal i, (coeff p.1) f * (coeff p.2) g ∈ I * J
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
x : ↑(f.rootSet S)
hx : g • x ≠ x
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = Equiv.swap (g • x) x

Tactic:
ext z

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := ⋯
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
x : ↑(f.rootSet S)
hx : g • x ≠ x
z : ↑(f.rootSet S)
⊢ ↑(((MulAction.toPermHom G ↑(f.rootSet S)) g) z) = ↑((Equiv.swap (g • x) x) z)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ -1 • f.toFun' S m + -↑n • f.toFun' S m = -↑n • f.toFun' S m + -1 • f.toFun' S m

Tactic:
rw [add_comm]

Goal state after: