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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ pairs σ k
⊢ weight σ R k t + weight σ R k (pairMap σ t) = 0

Tactic:
rw [weight, weight]
  rw [mem_pairs] at h
  have h2 (n : ℕ) : -(-1 : MvPolynomial σ R) ^ n = (-1) ^ (n + 1) := by
    rw [← neg_one_mul ((-1 : MvPolynomial σ R) ^ n), pow_add, pow_one, mul_comm]
  rcases (em (t.snd ∈ t.fst)) with h1 | h1
  · rw [pairMap_of_snd_mem_fst σ h1]
    simp only [← prod_erase_mul t.fst (fun j ↦ (X j : MvPolynomial σ R)) h1,
      mul_assoc (∏ a ∈ erase t.fst t.snd, X a), card_erase_of_mem h1]
    nth_rewrite 1 [← pow_one (X t.snd)]
    simp only [← pow_add, add_comm]
    have h3 : 1 ≤ #t.1 := lt_iff_add_one_le.mp (card_pos.mpr ⟨t.snd, h1⟩)
    rw [← tsub_tsub_assoc h.left h3, ← neg_neg ((-1 : MvPolynomial σ R) ^ (#t.1 - 1)),
      h2 (#t.1 - 1), Nat.sub_add_cancel h3]
    simp
  · rw [pairMap_of_snd_notMem_fst σ h1]
    simp only [mul_comm, mul_assoc (∏ a ∈ t.fst, X a), card_cons, prod_cons]
    nth_rewrite 2 [← pow_one (X t.snd)]
    simp only [← pow_add, ← Nat.add_sub_assoc (Nat.lt_of_le_of_ne h.left (mt h.right h1)), add_comm,
      Nat.succ_eq_add_one, Nat.add_sub_add_right]
    rw [← neg_neg ((-1 : MvPolynomial σ R) ^ #t.1), h2]
    simp

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case pos
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 ∈ 𝓝 (Valued.v a),
    ⇑Valued.v ⁻¹' s ∈
      Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a)

Tactic:
intro S

Goal state after:
case pos
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 ℤ))
⊢ S ∈ 𝓝 (Valued.v a) →
    ⇑Valued.v ⁻¹' S ∈
      Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a)
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ ∀ {X Y : ModuleCat R} (f : X ⟶ Y),
    (ModuleCat.toMatrixModCat R ι ⋙ toModuleCat R i).map f ≫
        (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑Y) i ≪≫ₗ
              fromModuleCatToModuleCatLinearEquiv R (↑Y) i).toModuleIso.hom =
      (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X) i ≪≫ₗ
              fromModuleCatToModuleCatLinearEquiv R (↑X) i).toModuleIso.hom ≫
        (𝟭 (ModuleCat R)).map f

Tactic:
intros

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
X✝ Y✝ : ModuleCat R
f✝ : X✝ ⟶ Y✝
⊢ (ModuleCat.toMatrixModCat R ι ⋙ toModuleCat R i).map f✝ ≫
      (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑Y✝) i ≪≫ₗ
            fromModuleCatToModuleCatLinearEquiv R (↑Y✝) i).toModuleIso.hom =
    (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X✝) i ≪≫ₗ
            fromModuleCatToModuleCatLinearEquiv R (↑X✝) i).toModuleIso.hom ≫
      (𝟭 (ModuleCat R)).map f✝
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ ∀ {X Y : ModuleCat (Matrix ι ι R)} (f : X ⟶ Y),
    (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι).map f ≫
        (toModuleCatFromModuleCatLinearEquiv R Y i).symm.toModuleIso.hom =
      (toModuleCatFromModuleCatLinearEquiv R X i).symm.toModuleIso.hom ≫ (𝟭 (ModuleCat (Matrix ι ι R))).map f

Tactic:
intros

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
X✝ Y✝ : ModuleCat (Matrix ι ι R)
f✝ : X✝ ⟶ Y✝
⊢ (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι).map f✝ ≫
      (toModuleCatFromModuleCatLinearEquiv R Y✝ i).symm.toModuleIso.hom =
    (toModuleCatFromModuleCatLinearEquiv R X✝ i).symm.toModuleIso.hom ≫ (𝟭 (ModuleCat (Matrix ι ι R))).map f✝
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case cont_f
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
⊢ Continuous ⇑Valued.v

Tactic:
refine Valued.continuous_valuation_of_surjective (fun x ↦ ?_)

Goal state after:
case cont_f
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
this : UniformSpace ratfuncAdicComplPkg.space := ratfuncAdicComplPkg.uniformStruct
raw_surj : Function.Surjective ⇑Valued.v
x : WithZero (Multiplicative ℤ)
⊢ ∃ a, Valued.v a = x
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = (expand p) (C (↑p ^ k) * X k ^ p ^ (n - k))

Tactic:
map_mul (expand p),

Goal state after:
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = (expand p) (C (↑p ^ k)) * (expand p) (X k ^ p ^ (n - k))
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
n : ℕ
⊢ constantCoeff (wittZSMul p z n) = 0

Tactic:
apply constantCoeff_wittStructureInt p _ _ n
  simp only [smul_zero, map_zsmul, constantCoeff_X]

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

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (id x).coeff = fun n ↦ (aeval x.coeff) (X n)

Tactic:
intros

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ (id x✝).coeff = fun n ↦ (aeval x✝.coeff) (X n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x

Tactic:
intros

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ f x✝ = g x✝
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 (↑p ^ n) * C (⅟↑p ^ n) * X n ^ p +
        C (↑p ^ (n + 1)) * X (n + 1) * C (⅟↑p ^ n) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)

Tactic:
mul_right_comm (C ((p : ℚ) ^ (n + 1))),

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 (↑p ^ n) * C (⅟↑p ^ n) * X n ^ p +
        C (↑p ^ (n + 1)) * C (⅟↑p ^ n) * 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.IsPoly

Goal state before:
pp: case h
p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃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)
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    ((g ∘ f) x).coeff = fun n ↦ (aeval x.coeff) ((fun n ↦ (bind₁ φ) (ψ n)) n)

Tactic:
intros

Goal state after:
case h
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
g f : ⦃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)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ ((g ∘ f) x✝).coeff = fun n ↦ (aeval x✝.coeff) ((fun n ↦ (bind₁ φ) (ψ n)) n)
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:
by
  rw [verschiebungFun_coeff, if_pos rfl]

Goal state after:
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
φ : ℕ → 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]
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R),
    (h (f x) (g y)).coeff = fun n ↦
      peval
        ((fun n ↦ (bind₁ (uncurry ![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)])) (χ n)) n)
        ![x.coeff, y.coeff]

Tactic:
intros

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]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (h (f x✝) (g y✝)).coeff = fun n ↦
    peval
      ((fun n ↦ (bind₁ (uncurry ![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)])) (χ n)) n)
      ![x✝.coeff, y✝.coeff]
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case h
p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R),
    (g (f x y)).coeff = fun n ↦ peval ((fun n ↦ (bind₁ φ) (ψ n)) n) ![x.coeff, y.coeff]

Tactic:
intros

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

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (f x x).coeff = fun n ↦ (aeval x.coeff) ((fun n ↦ (bind₁ (uncurry ![X, X])) (φ n)) n)

Tactic:
intros

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ (f x✝ x✝).coeff = fun n ↦ (aeval x✝.coeff) ((fun n ↦ (bind₁ (uncurry ![X, X])) (φ n)) n)
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: case «0»
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 i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ((fun i ↦ i) ⟨0, ⋯⟩, i) =
    (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ((fun i ↦ i) ⟨0, ⋯⟩, i))

pp: case «1»
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 i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ((fun i ↦ i) ⟨1, ⋯⟩, i) =
    (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ((fun i ↦ i) ⟨1, ⋯⟩, i))

Tactic:
· simp [Function.uncurry, Matrix.cons_val_zero, ih]

Goal state after:
case «1»
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 i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ((fun i ↦ i) ⟨1, ⋯⟩, i) =
    (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ((fun i ↦ i) ⟨1, ⋯⟩, i))
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (-x).coeff = fun n ↦ (aeval x.coeff) ((fun n ↦ (rename Prod.snd) (wittNeg p n)) n)

Tactic:
intros

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ (-x✝).coeff = fun n ↦ (aeval x✝.coeff) ((fun n ↦ (rename Prod.snd) (wittNeg p n)) n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), coeff 0 = fun n ↦ (aeval x.coeff) (0 n)

Tactic:
intros

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ coeff 0 = fun n ↦ (aeval x✝.coeff) (0 n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), coeff 1 = fun n ↦ (aeval x.coeff) (onePoly n)

Tactic:
intros

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ coeff 1 = fun n ↦ (aeval x✝.coeff) (onePoly n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (x + y).coeff = fun n ↦ peval (wittAdd p n) ![x.coeff, y.coeff]

Tactic:
intros

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (x✝ + y✝).coeff = fun n ↦ peval (wittAdd p n) ![x✝.coeff, y✝.coeff]
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (x * y).coeff = fun n ↦ peval (wittMul p n) ![x.coeff, y.coeff]

Tactic:
intros

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (x✝ * y✝).coeff = fun n ↦ peval (wittMul p n) ![x✝.coeff, y✝.coeff]
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y

Tactic:
intros

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ f x✝ y✝ = g x✝ y✝
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), x.frobeniusFun.coeff = fun n ↦ (aeval x.coeff) (frobeniusPoly p n)

Tactic:
intros

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ x✝.frobeniusFun.coeff = fun n ↦ (aeval x✝.coeff) (frobeniusPoly p n)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_1
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₁
⊢ liftFun f 1 = 1

Tactic:
intros

Goal state after:
case refine_1
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₁
⊢ liftFun f 1 = 1
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_2
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₁
⊢ ∀ (x y : S), liftFun f (x * y) = liftFun f x * liftFun f y

Tactic:
intros

Goal state after:
case refine_2
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₁
x✝ y✝ : S
⊢ liftFun f (x✝ * y✝) = liftFun f x✝ * liftFun f y✝
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_3
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₁
⊢ liftFun f 0 = 0

Tactic:
intros

Goal state after:
case refine_3
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₁
⊢ liftFun f 0 = 0
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_4
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₁
⊢ ∀ (x y : S), liftFun f (x + y) = liftFun f x + liftFun f y

Tactic:
intros

Goal state after:
case refine_4
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₁
x✝ y✝ : S
⊢ liftFun f (x✝ + y✝) = liftFun f x✝ + liftFun f y✝
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: 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)

Tactic:
apply map_injective (Int.castRingHom ℚ) Int.cast_injective

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

Goal state before:
pp: case pn
n : ℕ
⊢ (hermite n).degree ≤ ↑n

pp: case p1
n : ℕ
⊢ (hermite n).coeff n ≠ 0

Tactic:
· simp_rw [degree_le_iff_coeff_zero, Nat.cast_lt]
    rintro m hnm
    exact coeff_hermite_of_lt hnm

Goal state after:
case p1
n : ℕ
⊢ (hermite n).coeff n ≠ 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
hnk : Odd (n + k)
⊢ (hermite n).coeff k = 0

Tactic:
induction n generalizing k with
  | zero =>
    rw [zero_add k] at hnk
    exact coeff_hermite_of_lt hnk.pos
  | succ n ih =>
    cases k with
    | zero =>
      rw [Nat.succ_add_eq_add_succ] at hnk
      rw [coeff_hermite_succ_zero, ih hnk, neg_zero]
    | succ k =>
      rw [coeff_hermite_succ_succ, ih, ih, mul_zero, sub_zero]
      · rwa [Nat.succ_add_eq_add_succ] at hnk
      · rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk
        exact (Nat.odd_add.mp hnk).mpr even_two

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

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

Tactic:
intro n k

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

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

Tactic:
induction n generalizing x with

Goal state after: