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

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, (a, k - a) ∈ {a ∈ antidiagonal k | a.1 < k}

pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ {a ∈ antidiagonal k | a.1 < k}, a.1 ∈ range k

pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, (a, k - a).1 = a

pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ {a ∈ antidiagonal k | a.1 < k}, (a.1, k - a.1) = a

pp: case refine_5
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, ∑ x ∈ powersetCard a univ, ∑ y, f (x, y) = ∑ A ∈ powersetCard (a, k - a).1 univ, ∑ j, f (A, j)

Tactic:
<;>

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, (a, k - a) ∈ {a ∈ antidiagonal k | a.1 < k}

case refine_2
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ {a ∈ antidiagonal k | a.1 < k}, a.1 ∈ range k

case refine_3
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, (a, k - a).1 = a

case refine_4
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ {a ∈ antidiagonal k | a.1 < k}, (a.1, k - a.1) = a

case refine_5
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, ∑ x ∈ powersetCard a univ, ∑ y, f (x, y) = ∑ A ∈ powersetCard (a, k - a).1 univ, ∑ j, f (A, j)
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
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ((algebraMap K⟮X⟯ K⸨X⸩) ((fun x ↦ x.2 - x.1) x✝¹)) < embedding ↑d

Tactic:
map_sub

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
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ((algebraMap K⟮X⟯ K⸨X⸩) x✝¹.2 - (algebraMap K⟮X⟯ K⸨X⸩) x✝¹.1) < embedding ↑d
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: case pos
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
i1 j1 : ι
h : j = i1
⊢ x i j1 = ∑ c, if j = i1 ∧ c = j1 then x i c else 0

pp: case neg
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
i1 j1 : ι
h : ¬j = i1
⊢ 0 = ∑ c, if j = i1 ∧ c = j1 then x i c else 0

Tactic:
<;>

Goal state after:
case pos
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
i1 j1 : ι
h : j = i1
⊢ x i j1 = ∑ c, if j = i1 ∧ c = j1 then x i c else 0

case neg
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
i1 j1 : ι
h : ¬j = i1
⊢ 0 = ∑ c, if j = i1 ∧ c = j1 then x i c else 0
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case zero
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
v : Fin (n + 1) →₀ ℕ
⊢ MvPolynomial.coeff v
      ((MvPolynomial.aeval fun i ↦
          (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i))
        (MvPolynomial.X 0)) =
    MvPolynomial.coeff v ((MvPolynomial.aeval MvPolynomial.X) (MvPolynomial.X 0))

pp: case succ
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
v : Fin (n + 1) →₀ ℕ
i✝ : Fin n
⊢ MvPolynomial.coeff v
      ((MvPolynomial.aeval fun i ↦
          (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i))
        (MvPolynomial.X i✝.succ)) =
    MvPolynomial.coeff v ((MvPolynomial.aeval MvPolynomial.X) (MvPolynomial.X i✝.succ))

Tactic:
<;>

Goal state after:
case zero
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
v : Fin (n + 1) →₀ ℕ
⊢ MvPolynomial.coeff v
      ((MvPolynomial.aeval fun i ↦
          (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i))
        (MvPolynomial.X 0)) =
    MvPolynomial.coeff v ((MvPolynomial.aeval MvPolynomial.X) (MvPolynomial.X 0))

case succ
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
v : Fin (n + 1) →₀ ℕ
i✝ : Fin n
⊢ MvPolynomial.coeff v
      ((MvPolynomial.aeval fun i ↦
          (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i))
        (MvPolynomial.X i✝.succ)) =
    MvPolynomial.coeff v ((MvPolynomial.aeval MvPolynomial.X) (MvPolynomial.X i✝.succ))
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ (T1 f c).comp (T1 f (-c)) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)

Tactic:
by
  rw [comp_aeval, ← MvPolynomial.aeval_X_left]
  ext i v
  cases i using Fin.cases <;> simp

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

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

Tactic:
have h (i : Fin n) :
      (Polynomial.C (X (R := k) i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0 :=
    pow_ne_zero (v i.succ) (leadingCoeff_ne_zero.mp <| by simp [add_comm, leadingCoeff_X_pow_add_C])

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
h : ∀ (i : Fin n), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.C a) *
        (Polynomial.X ^ v 0 *
          ∏ x, (Polynomial.C (MvPolynomial.X x) + Polynomial.X ^ up ^ ↑x.succ) ^ v x.succ)).natDegree =
    up ^ ↑0 * v 0 + ∑ i, up ^ ↑i.succ * v i.succ
Module: Mathlib.RingTheory.NoetherNormalization

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

Tactic:
add_comm (Polynomial.C _),

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

Goal state before:
pp: case refine_1
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
i : Fin (n + 1)
⊢ v i < up

pp: case refine_2
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
i : Fin (n + 1)
⊢ w i < up

Tactic:
<;>

Goal state after:
case refine_1
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
i : Fin (n + 1)
⊢ v i < up

case refine_2
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
i : Fin (n + 1)
⊢ w i < up
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case neg
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : ¬j = 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.X j) +
        (MvPolynomial.finSuccEquiv k n) (MvPolynomial.X 0) ^ up ^ ↑j).leadingCoeff =
    1

Tactic:
obtain ⟨i, rfl⟩ := Fin.exists_succ_eq.mpr h

Goal state after:
case neg
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
i : Fin n
h : ¬i.succ = 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.X i.succ) +
        (MvPolynomial.finSuccEquiv k n) (MvPolynomial.X 0) ^ up ^ ↑i.succ).leadingCoeff =
    1
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: case refine_1
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ (Ideal.Quotient.mk I) (Quotient.out ((coeff (R ⧸ I) p n) x)) = (coeff (R ⧸ I) p n) x

pp: case refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ (Ideal.Quotient.mk I) (Quotient.out ((coeff (R ⧸ I) p n) y)) = (coeff (R ⧸ I) p n) y

Tactic:
<;>

Goal state after:
case refine_1
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ (Ideal.Quotient.mk I) (Quotient.out ((coeff (R ⧸ I) p n) x)) = (coeff (R ⧸ I) p n) x

case refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ (Ideal.Quotient.mk I) (Quotient.out ((coeff (R ⧸ I) p n) y)) = (coeff (R ⧸ I) p n) y
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

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

pp: case refine_2
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∀ (y : ℕ → MvPolynomial (idx × ℕ) ℚ),
    (fun φ ↦ ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ) y →
      y = wittStructureRat p Φ

Tactic:
· intro n; apply wittStructureRat_prop

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

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
H : i ∈ (range n).biUnion fun i ↦ (C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars
⊢ i ∈ range n

Tactic:
mem_biUnion

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i : ℕ
H : ∃ a ∈ range n, i ∈ (C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a)).vars
⊢ i ∈ range 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)
H : n ∈ (range n).biUnion fun i ↦ (C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars
⊢ False

Tactic:
mem_biUnion

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)
H : ∃ a ∈ range n, n ∈ (C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a)).vars
⊢ False
Module: Mathlib.RingTheory.WittVector.Defs

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

Tactic:
simp only [wittAdd, wittStructureRat, map_add, rename_X, xInTermsOfW_zero, map_X,
    wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]

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

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

pp: 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, ⋯⟩)

Tactic:
<;>

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.Basic

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
⊢ mapFun (⇑f) (Nat.unaryCast 0) = ↑0

pp: case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
n✝ : ℕ
a✝ : mapFun (⇑f) n✝.unaryCast = ↑n✝
⊢ mapFun (⇑f) (n✝ + 1).unaryCast = ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
⊢ mapFun (⇑f) (Nat.unaryCast 0) = ↑0

case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
n✝ : ℕ
a✝ : mapFun (⇑f) n✝.unaryCast = ↑n✝
⊢ mapFun (⇑f) (n✝ + 1).unaryCast = ↑(n✝ + 1)
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
⊢ 0 = ↑0

pp: case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
n✝ : ℕ
a✝ : mapFun (⇑f) n✝.unaryCast = ↑n✝
⊢ ↑n✝ + 1 = ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
⊢ 0 = ↑0

case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
n✝ : ℕ
a✝ : mapFun (⇑f) n✝.unaryCast = ↑n✝
⊢ ↑n✝ + 1 = ↑(n✝ + 1)
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: case ofNat
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
a✝ : ℕ
⊢ mapFun (⇑f) (Int.ofNat a✝).castDef = ↑(Int.ofNat a✝)

pp: case negSucc
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
a✝ : ℕ
⊢ mapFun (⇑f) (Int.negSucc a✝).castDef = ↑(Int.negSucc a✝)

Tactic:
<;>

Goal state after:
case ofNat
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
a✝ : ℕ
⊢ mapFun (⇑f) (Int.ofNat a✝).castDef = ↑(Int.ofNat a✝)

case negSucc
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
a✝ : ℕ
⊢ mapFun (⇑f) (Int.negSucc a✝).castDef = ↑(Int.negSucc a✝)
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: case ofNat
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
a✝ : ℕ
⊢ ↑a✝ = ↑↑a✝

pp: case negSucc
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
a✝ : ℕ
⊢ -↑(a✝ + 1) = ↑(Int.negSucc a✝)

Tactic:
<;>

Goal state after:
case ofNat
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
a✝ : ℕ
⊢ ↑a✝ = ↑↑a✝

case negSucc
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
a✝ : ℕ
⊢ -↑(a✝ + 1) = ↑(Int.negSucc a✝)
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ (Nat.unaryCast 0).ghostFun = ↑0

pp: case succ
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n✝ : ℕ
a✝ : n✝.unaryCast.ghostFun = ↑n✝
⊢ (n✝ + 1).unaryCast.ghostFun = ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ (Nat.unaryCast 0).ghostFun = ↑0

case succ
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n✝ : ℕ
a✝ : n✝.unaryCast.ghostFun = ↑n✝
⊢ (n✝ + 1).unaryCast.ghostFun = ↑(n✝ + 1)
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: case ofNat
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
a✝ : ℕ
⊢ (Int.ofNat a✝).castDef.ghostFun = ↑(Int.ofNat a✝)

pp: case negSucc
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
a✝ : ℕ
⊢ (Int.negSucc a✝).castDef.ghostFun = ↑(Int.negSucc a✝)

Tactic:
<;>

Goal state after:
case ofNat
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
a✝ : ℕ
⊢ (Int.ofNat a✝).castDef.ghostFun = ↑(Int.ofNat a✝)

case negSucc
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
a✝ : ℕ
⊢ (Int.negSucc a✝).castDef.ghostFun = ↑(Int.negSucc a✝)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case py₂
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 : ℕ),
    (bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
      (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Tactic:
· intro n; apply wittStructureRat_prop

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

Goal state before:
pp: case e'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    (map (Int.castRingHom R)) ((bind₁ (wittStructureInt p Φ)) (W_ ℤ n))

pp: case e'_3
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (rename (Prod.mk i)) (W_ R n)) Φ =
    (map (Int.castRingHom R)) ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ)

Tactic:
<;>

Goal state after:
case e'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    (map (Int.castRingHom R)) ((bind₁ (wittStructureInt p Φ)) (W_ ℤ n))

case e'_3
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (rename (Prod.mk i)) (W_ R n)) Φ =
    (map (Int.castRingHom R)) ((bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case e'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    (eval₂Hom ((map (Int.castRingHom R)).comp C) fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n)

pp: case e'_3
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (rename (Prod.mk i)) (W_ R n)) Φ =
    (eval₂Hom ((map (Int.castRingHom R)).comp C) fun i ↦ (map (Int.castRingHom R)) ((rename (Prod.mk i)) (W_ ℤ n))) Φ

Tactic:
<;>

Goal state after:
case e'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    (eval₂Hom ((map (Int.castRingHom R)).comp C) fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n)

case e'_3
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (aeval fun i ↦ (rename (Prod.mk i)) (W_ R n)) Φ =
    (eval₂Hom ((map (Int.castRingHom R)).comp C) fun i ↦ (map (Int.castRingHom R)) ((rename (Prod.mk i)) (W_ ℤ n))) Φ
Module: Mathlib.RingTheory.WittVector.Verschiebung

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

pp: case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n✝ : ℕ
⊢ (verschiebungFun 0).coeff (n✝ + 1) = coeff 0 (n✝ + 1)

Tactic:
<;>

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

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

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

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

Tactic:
<;>

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

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