mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
⊢ (bind₁ fun b ↦ (rename fun i ↦ (b, i)) ((expand p) (W_ ℤ n))) Φ =
    (bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n)

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

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
⊢ (map (Int.castRingHom ℚ)) ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) ((expand p) (W_ ℤ n))) Φ) =
    (map (Int.castRingHom ℚ)) ((bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False

Tactic:
replace H := (ih j hj).2 (vars_pow _ _ H)

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ range (j + 1)
⊢ False
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittAdd p 0 = X (0, 0) + X (1, 0)

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

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittAdd p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) + X (1, 0))
Module: Mathlib.RingTheory.WittVector.Defs

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

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

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittSub p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) - X (1, 0))
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittMul p 0 = X (0, 0) * X (1, 0)

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

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittMul p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) * X (1, 0))
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

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittNeg p 0) = (map (Int.castRingHom ℚ)) (-X (0, 0))
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p' : ℕ
R' : Type u_2
x y : WittVector p' R'
i : Fin 2
⊢ (![x, y] i).coeff = ![x.coeff, y.coeff] i

Tactic:
fin_cases i

Goal state after:
case «0»
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
⊢ (![x, y] ((fun i ↦ i) ⟨0, ⋯⟩)).coeff = ![x.coeff, y.coeff] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
⊢ (![x, y] ((fun i ↦ i) ⟨1, ⋯⟩)).coeff = ![x.coeff, y.coeff] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
idx : Type u_1
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ f n = g n

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

Goal state after:
p : ℕ
idx : Type u_1
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ f n = g n

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

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ (coeffMonoidHom M p n) f ^ p ^ n = (coeffMonoidHom M p 0) f

Tactic:
← coeffMonoidHom_pow_p_pow' _ 0 n,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ (coeffMonoidHom M p n) f ^ p ^ n = (coeffMonoidHom M p (0 + n)) f ^ p ^ n
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (bind₁ (wittStructureInt p Φ)) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ

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

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (map (Int.castRingHom ℚ)) ((bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) =
    (map (Int.castRingHom ℚ)) ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ)
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)) Φ
k : ℕ
⊢ φ k = wittStructureInt p Φ k

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

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)) Φ
k : ℕ
⊢ (map (Int.castRingHom ℚ)) (φ k) = (map (Int.castRingHom ℚ)) (wittStructureInt p Φ k)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ wittStructureInt p ((rename f) Φ) n = (rename (Prod.map f id)) (wittStructureInt p Φ n)

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

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ (map (Int.castRingHom ℚ)) (wittStructureInt p ((rename f) Φ) n) =
    (map (Int.castRingHom ℚ)) ((rename (Prod.map f id)) (wittStructureInt p Φ n))
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

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

Tactic:
apply inj

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ 0)) = (Int.castRingHom ℚ) (constantCoeff Φ)
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 : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ constantCoeff (wittStructureInt p Φ n) = 0

Tactic:
apply inj

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ⇑(Int.castRingHom ℚ)
⊢ (Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ n)) = (Int.castRingHom ℚ) 0
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:
funext n

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✝
n : ℕ
⊢ (h (f x✝) (g y✝)).coeff 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.Verschiebung

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

Tactic:
aeval_X,

Goal state after:
case succ
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ x.coeff (n + 1 - 1) = x.coeff 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
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✝
n✝ : ℕ
i : Fin 2
n : ℕ
⊢ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] (i, n).1 (i, n).2 =
    (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
      (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] (i, n).1 (i, n).2)

Tactic:
fin_cases i

Goal state after:
case «0»
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✝
n✝ n : ℕ
⊢ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] ((fun i ↦ i) ⟨0, ⋯⟩, n).1
      ((fun i ↦ i) ⟨0, ⋯⟩, n).2 =
    (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
      (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] ((fun i ↦ i) ⟨0, ⋯⟩, n).1
        ((fun i ↦ i) ⟨0, ⋯⟩, n).2)

case «1»
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✝
n✝ n : ℕ
⊢ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] ((fun i ↦ i) ⟨1, ⋯⟩, n).1
      ((fun i ↦ i) ⟨1, ⋯⟩, n).2 =
    (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
      (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] ((fun i ↦ i) ⟨1, ⋯⟩, n).1
        ((fun i ↦ i) ⟨1, ⋯⟩, n).2)
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:
funext n

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✝
n : ℕ
⊢ (f x✝ x✝).coeff n = (aeval x✝.coeff) ((fun n ↦ (bind₁ (uncurry ![X, X])) (φ 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
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✝
n : ℕ
i : Fin 2
k : ℕ
⊢ ![x✝.coeff, x✝.coeff] (i, k).1 (i, k).2 = (aeval x✝.coeff) (![X, X] (i, k).1 (i, k).2)

Tactic:
fin_cases i

Goal state after:
case «0»
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✝
n k : ℕ
⊢ ![x✝.coeff, x✝.coeff] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2 =
    (aeval x✝.coeff) (![X, X] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2)

case «1»
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✝
n k : ℕ
⊢ ![x✝.coeff, x✝.coeff] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2 =
    (aeval x✝.coeff) (![X, X] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2)
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:
funext n

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✝
n : ℕ
⊢ (-x✝).coeff 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✝
n : ℕ
i : Fin 1
k : ℕ
⊢ uncurry ![x✝.coeff] (i, k) = (x✝.coeff ∘ Prod.snd) (i, k)

Tactic:
fin_cases i

Goal state after:
case «0»
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✝
n k : ℕ
⊢ uncurry ![x✝.coeff] ((fun i ↦ i) ⟨0, ⋯⟩, k) = (x✝.coeff ∘ Prod.snd) ((fun i ↦ i) ⟨0, ⋯⟩, k)
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:
funext n

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✝
n : ℕ
⊢ coeff 0 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:
funext n

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✝
n : ℕ
⊢ coeff 1 n = (aeval x✝.coeff) (onePoly n)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n + 1)

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

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) ((bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n)) =
    (MvPolynomial.map (Int.castRingHom ℚ)) (wittPolynomial p ℤ (n + 1))
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:
funext n

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✝
n : ℕ
⊢ x✝.frobeniusFun.coeff n = (aeval x✝.coeff) (frobeniusPoly p n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → 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]
n : ℕ
i : Fin 2
k : ℕ
⊢ g (![x.coeff, y.coeff] (i, k).1 (i, k).2) =
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] (i, k).1 (i, k).2

Tactic:
fin_cases i

Goal state after:
case «0»
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → 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]
n k : ℕ
⊢ g (![x.coeff, y.coeff] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2) =
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2

case «1»
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → 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]
n k : ℕ
⊢ g (![x.coeff, y.coeff] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2) =
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : (truncate n) x = (truncate n) y
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff ⟨i, hi⟩ ((truncate n) x) = y.coeff i

Tactic:
← coeff_truncate y ⟨i, hi⟩,

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : (truncate n) x = (truncate n) y
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff ⟨i, hi⟩ ((truncate n) x) = TruncatedWittVector.coeff ⟨i, hi⟩ ((truncate n) y)
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e'_3
n : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + 0).choose 0) = -(hermite (2 * n + 1)).coeff 1

Tactic:
coeff_hermite_explicit n 1,

Goal state after:
case e'_3
n : ℕ
⊢ (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + 0).choose 0) =
    -((-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + 1).choose 1))
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))
⊢ (-1) ^ n *
      (deriv (fun x ↦ (aeval x) (hermite n)) x * Real.exp (-(x ^ 2 / 2)) +
        (aeval x) (hermite n) * (-x * Real.exp (-(x ^ 2 / 2)))) =
    (-1) ^ n * -1 *
      (((aeval x) X * (aeval x) (hermite n) - (aeval x) (derivative (hermite n))) * Real.exp (-(x ^ 2 / 2)))

pp: case succ.hc
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))
⊢ DifferentiableAt ℝ (fun x ↦ (aeval x) (hermite n)) x

pp: case succ.hd
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))
⊢ DifferentiableAt ℝ (fun x ↦ Real.exp (-(x ^ 2 / 2))) x

Tactic:
aeval_X,

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))
⊢ (-1) ^ n *
      (deriv (fun x ↦ (aeval x) (hermite n)) x * Real.exp (-(x ^ 2 / 2)) +
        (aeval x) (hermite n) * (-x * Real.exp (-(x ^ 2 / 2)))) =
    (-1) ^ n * -1 * ((x * (aeval x) (hermite n) - (aeval x) (derivative (hermite n))) * Real.exp (-(x ^ 2 / 2)))

case succ.hc
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))
⊢ DifferentiableAt ℝ (fun x ↦ (aeval x) (hermite n)) x

case succ.hd
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))
⊢ DifferentiableAt ℝ (fun x ↦ Real.exp (-(x ^ 2 / 2))) x
Module: Mathlib.RingTheory.Polynomial.Selmer

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

Tactic:
right_eq_add

Goal state after:
n : ℕ
z : ℂ
h1 : z = 0
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ z = 0
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p.degree ≤ 2
⊢ p = C (p.coeff 2) * X ^ 2 + C (p.coeff 1) * X + C (p.coeff 0)

Tactic:
by
  rw [p.as_sum_range_C_mul_X_pow'
    (Nat.lt_of_le_of_lt (natDegree_le_iff_degree_le.mpr hp) (Nat.lt_add_one 2))]
  simp [Finset.sum_range_succ]
  abel

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

Goal state before:
pp: n : ℕ
⊢ (-1) ^ n * ((⇑derivative)^[n] (X ^ n * (1 - X) ^ n)).comp (1 - X) = (⇑derivative)^[n] (X ^ n * (1 - X) ^ n)

Tactic:
← iterate_derivative_comp_one_sub_X

Goal state after:
n : ℕ
⊢ (⇑derivative)^[n] ((X ^ n * (1 - X) ^ n).comp (1 - X)) = (⇑derivative)^[n] (X ^ n * (1 - X) ^ n)