mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : t ∈ ↑p.support
s : Fin n →₀ ℕ
hs : s ∈ ↑p.support
he :
  (supDegree ⇑toLex ∘ fun i ↦ ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) t =
    (supDegree ⇑toLex ∘ fun i ↦ ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) s
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s

Tactic:
rw [mem_coe, mem_support_iff] at ht hs

Goal state after:
case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he :
  (supDegree ⇑toLex ∘ fun i ↦ ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) t =
    (supDegree ⇑toLex ∘ fun i ↦ ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) s
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s
Module: Mathlib.RingTheory.LaurentSeries

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

Tactic:
embedding_restrict₀

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

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

Tactic:
sub_zero,

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

Goal state before:
pp: case h.right
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
a : K⟮X⟯
x✝ : a ∈ (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) ⁻¹' {t | Valued.v t < γ}
⊢ a ∈ ⇑Valued.v ⁻¹' Set.Iio γ

Tactic:
rw [Set.mem_preimage, Set.mem_Iio, ← Valued.valuedCompletion_apply a]

Goal state after:
case h.right
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
a : K⟮X⟯
x✝ : a ∈ (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) ⁻¹' {t | Valued.v t < γ}
⊢ Valued.v ↑a < γ
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✝ : IsPrecomplete I R
x : Perfection (R ⧸ I) p
y : R
n : ℕ
h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x
this : x.teichmullerAux (n + 1) ≡ ⋯.choose [SMOD I ^ (n + 1)]
⊢ Quotient.out ((coeff (R ⧸ I) p n) x) ≡ y [SMOD I]

Tactic:
simp [SModEq.idealQuotientMk, h]

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

Goal state before:
pp: case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (W_ R n - ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) *
      (algebraMap R (MvPolynomial ℕ R)) (⅟↑p ^ n) =
    X n * C (↑p ^ n) * C (⅟↑p ^ n)

Tactic:
congr 1

Goal state after:
case ind.e_a
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ W_ R n - ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = X n * C (↑p ^ n)
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)
⊢ (fun x ↦ ↑x)
      (coeff c
            ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
              ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
          ↑p ^ n).num =
    coeff c
        ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
          ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
      ↑p ^ n

Tactic:
simp only [← sum_induction_steps, ← map_wittPolynomial p (Int.castRingHom ℚ), ← map_rename, ←
    map_bind₁, ← map_sub, coeff_map]

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)
⊢ ↑((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
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case succ
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m : ℕ
ih : ∀ (n : ℕ), (coeffMonoidHom M p n) ((⇑(powMulEquiv (Perfection M p) p).symm)^[m] f) = (coeffMonoidHom M p (n + m)) f
n : ℕ
⊢ (coeffMonoidHom M p n) ((⇑(powMulEquiv (Perfection M p) p).symm)^[m + 1] f) = (coeffMonoidHom M p (n + (m + 1))) f

Tactic:
Function.iterate_succ_apply',

Goal state after:
case succ
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m : ℕ
ih : ∀ (n : ℕ), (coeffMonoidHom M p n) ((⇑(powMulEquiv (Perfection M p) p).symm)^[m] f) = (coeffMonoidHom M p (n + m)) f
n : ℕ
⊢ (coeffMonoidHom M p n) ((powMulEquiv (Perfection M p) p).symm ((⇑(powMulEquiv (Perfection M p) p).symm)^[m] f)) =
    (coeffMonoidHom M p (n + (m + 1))) f
Module: Mathlib.RingTheory.Perfection

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

Tactic:
Function.iterate_succ_apply',

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

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hh : IsPoly₂ p h
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
⊢ IsPoly₂ p fun x _Rcr x_1 y ↦ h (f x_1) (g y)

Tactic:
obtain ⟨χ, hh⟩ := hh

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
⊢ IsPoly₂ p fun x _Rcr x_1 y ↦ h (f x_1) (g y)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ x.coeff (n + 1 - 1) = x.coeff n

Tactic:
add_tsub_cancel_right

Goal state after:
case succ
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ x.coeff n = x.coeff n
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 →+* S
r : R
n : ℕ
⊢ f ((⇑↑(frobeniusEquiv R p).symm)^[n + 1] r ^ p) = (fun n ↦ f ((⇑↑(frobeniusEquiv R p).symm)^[n] r)) n

Tactic:
Function.iterate_succ_apply',

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 →+* S
r : R
n : ℕ
⊢ f (↑(frobeniusEquiv R p).symm ((⇑↑(frobeniusEquiv R p).symm)^[n] r) ^ p) =
    (fun n ↦ f ((⇑↑(frobeniusEquiv R p).symm)^[n] r)) n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u₁
inst✝² : CommSemiring R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n✝ n : ℕ
ih : (⇑(frobeniusEquiv R p).symm)^[n] (f 0) = f n
⊢ (⇑(frobeniusEquiv R p).symm)^[n.succ] (f 0) ^ p = f n.succ ^ p

Tactic:
Function.iterate_succ_apply',

Goal state after:
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u₁
inst✝² : CommSemiring R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n✝ n : ℕ
ih : (⇑(frobeniusEquiv R p).symm)^[n] (f 0) = f n
⊢ (frobeniusEquiv R p).symm ((⇑(frobeniusEquiv R p).symm)^[n] (f 0)) ^ p = f n.succ ^ p
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n + 1 - 1))

Tactic:
add_tsub_cancel_right

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ n)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) +
        -↑p / ↑p ^ n / ↑p ^ (n - i - v p (j + 1)) * ↑((p ^ (n - i)).choose (j + 1)) *
          ↑p ^ (i + j + (n - i - v p (j + 1))) -
      (↑((p ^ (n - i)).choose (j + 1)) / ↑p ^ (n - i - v p (j + 1)) * ↑p ^ (j - v p (j + 1)) * ↑p +
        -↑p / ↑p ^ n / ↑p ^ (n - i - v p (j + 1)) * ↑((p ^ (n - i)).choose (j + 1)) * ↑p ^ (j - v p (j + 1) + n)) =
    0

Tactic:
skip

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ ↑p ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (↑p ^ i * (↑p ^ n)⁻¹)) +
        -↑p / ↑p ^ n / ↑p ^ (n - i - v p (j + 1)) * ↑((p ^ (n - i)).choose (j + 1)) *
          ↑p ^ (i + j + (n - i - v p (j + 1))) -
      (↑((p ^ (n - i)).choose (j + 1)) / ↑p ^ (n - i - v p (j + 1)) * ↑p ^ (j - v p (j + 1)) * ↑p +
        -↑p / ↑p ^ n / ↑p ^ (n - i - v p (j + 1)) * ↑((p ^ (n - i)).choose (j + 1)) * ↑p ^ (j - v p (j + 1) + n)) =
    0
Module: Mathlib.RingTheory.WittVector.Domain

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

Tactic:
congr 1

Goal state after:
case succ.e_a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
h : ∀ i < k + 1, x.coeff i = 0
n✝ : ℕ
⊢ k.succ + n✝ = k + (n✝ + 1)
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case calc_3
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑frobenius)^[j] x * (⇑frobenius)^[i] y).coeff 0 = ((⇑frobenius)^[j] x).coeff 0 * ((⇑frobenius)^[i] y).coeff 0

pp: case calc_4
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑frobenius)^[j] x).coeff 0 * ((⇑frobenius)^[i] y).coeff 0 = x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i

Tactic:
· apply mul_coeff_zero

Goal state after:
case calc_4
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑frobenius)^[j] x).coeff 0 * ((⇑frobenius)^[i] y).coeff 0 = x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case pos
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : P m
⊢ X m ^ p ^ (n - m) + 0 = X m ^ p ^ (n - m)

Tactic:
add_zero

Goal state after:
case pos
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : P m
⊢ X m ^ p ^ (n - m) = X m ^ p ^ (n - m)
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
hp : Fact (Nat.Prime p)
⊢ ∀ (x : 𝕎 R), select P x + select (fun i ↦ ¬P i) x = x

Tactic:
have : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x :=
    IsPoly₂.diag (hf := IsPoly₂.comp)
  ghost_calc x
  intro n
  simp only [map_add]
  suffices
    (bind₁ (selectPoly P)) (wittPolynomial p ℤ n) +
        (bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) =
      wittPolynomial p ℤ n by
    apply_fun aeval x.coeff at this
    simpa only [map_add, aeval_bind₁, ← coeff_select]
  simp only [wittPolynomial_eq_sum_C_mul_X_pow, selectPoly, map_sum, map_pow, map_mul,
    bind₁_X_right, bind₁_C_right, ← Finset.sum_add_distrib, ← mul_add]
  apply Finset.sum_congr rfl
  refine fun m _ => mul_eq_mul_left_iff.mpr (Or.inl ?_)
  rw [ite_pow, zero_pow (pow_ne_zero _ hp.out.ne_zero)]
  by_cases Pm : P m
  · rw [if_pos Pm, if_neg <| not_not_intro Pm, zero_pow Fin.pos'.ne', add_zero]
  · rwa [if_neg Pm, if_pos, zero_add]

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

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
s : S
⊢ (truncate n) (liftFun f s) = (f n) s

Tactic:
by
  ext i
  simp only [liftFun, TruncatedWittVector.coeff_mk, WittVector.truncate_mk']
  rw [← f_compat (i + 1) n i.is_lt, RingHom.comp_apply, TruncatedWittVector.coeff_truncate]
  congr 1 with _

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

Goal state before:
pp: case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i ↦ ¬P i) z = y
y0 : P n
⊢ x.coeff n = x.coeff n + 0

Tactic:
add_zero

Goal state after:
case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i ↦ ¬P i) z = y
y0 : P n
⊢ x.coeff n = x.coeff n
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, x.coeff m = 0
⊢ x = (⇑verschiebung)^[n] ((⇑frobenius)^[n] ((⇑(frobeniusEquiv p k).symm)^[n] (x.shift n)))

Tactic:
calc
    _ = verschiebung^[n] (x.shift n) := by
      simpa using eq_iterate_verschiebung (x := x) (n := n) h
    _ = _ := 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.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ dickson 2 0 0 = X ^ 0

Tactic:
simp only [dickson_zero, pow_zero]
    norm_num

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

Goal state before:
pp: case succ
n : ℕ
ih : hermite n = (fun p ↦ X * p - derivative p)^[n] 1
⊢ hermite (n + 1) = (fun p ↦ X * p - derivative p)^[n + 1] 1

Tactic:
Function.iterate_succ_apply',

Goal state after:
case succ
n : ℕ
ih : hermite n = (fun p ↦ X * p - derivative p)^[n] 1
⊢ hermite (n + 1) = X * (fun p ↦ X * p - derivative p)^[n] 1 - derivative ((fun p ↦ X * p - derivative p)^[n] 1)
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ map (Int.castRingHom R) (dickson 1 1 (m * n)) = map (Int.castRingHom R) ((dickson 1 1 m).comp (dickson 1 1 n))

Tactic:
congr 1

Goal state after:
case e_a
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = (dickson 1 1 m).comp (dickson 1 1 n)
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n : ℕ
⊢ (hermite n).leadingCoeff = 1

Tactic:
rw [← coeff_natDegree, natDegree_hermite, coeff_hermite_self]

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

Goal state before:
pp: case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + k)

Tactic:
(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)

Goal state after:
case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + k + 2)
⊢ Odd (n + k)
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case succ
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ deriv^[n + 1] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))

Tactic:
Function.iterate_succ_apply',

Goal state after:
case succ
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ deriv (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n - 1)‼ * ((2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1)) =
    (2 * n - 1)‼ * ((2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2))

Tactic:
congr 1

Goal state after:
case e_a.e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n + 1) * (2 * (n + 1) + k).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2)
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case succ.refine_3
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
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ p.support
⊢ p.coeff x * ↑((d + (n - ↑⟨x, hx⟩)).choose d) = p.coeff x * ↑((d + 1 - 1 + (n - x)).choose (d + 1 - 1))

Tactic:
add_tsub_cancel_right

Goal state after:
case succ.refine_3
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
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
x : ℕ
hx : x ∈ p.support
⊢ p.coeff x * ↑((d + (n - ↑⟨x, hx⟩)).choose d) = p.coeff x * ↑((d + (n - x)).choose d)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ C ((-1) ^ x * ↑(n.choose x)) * ↑((n + x)! / x !) = C ((-1) ^ x * ↑(n.choose x)) * (C ↑((n + x).choose n) * ↑n !)

Tactic:
congr 1

Goal state after:
case a.e_a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((n + x)! / x !) = C ↑((n + x).choose n) * ↑n !