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

Goal state before:
pp: case h.hn
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)
⊢ ↑(p ^ n) ≠ 0

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)
⊢ ↑(p ^ n) ∣
    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))

Tactic:
·

Goal state after:
case h.hn
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)
⊢ ↑(p ^ n) ≠ 0
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₁ fun k ↦ (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
      (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

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:
·

Goal state after:
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₁ fun k ↦ (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
      (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)
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:
·

Goal state after:
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 ℚ)) Φ)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

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

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

Tactic:
·

Goal state after:
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) = fun i ↦
    (map (Int.castRingHom R)) (wittStructureInt p Φ i)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i ↦ (rename (Prod.mk i)) (W_ R n)) = fun i ↦ (map (Int.castRingHom R)) ((rename (Prod.mk i)) (W_ ℤ n))

Tactic:
·

Goal state after:
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i ↦ (rename (Prod.mk i)) (W_ R n)) = fun i ↦ (map (Int.castRingHom R)) ((rename (Prod.mk i)) (W_ ℤ n))
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h✝ : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h : n ≤ m
⊢ R

pp: case refine_2
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ ∀ (n_1 : ℕ),
    (fun m ↦ if h : n ≤ m then ?refine_1 else x ^ p ^ (n - m)) (n_1 + 1) ^ p =
      (fun m ↦ if h : n ≤ m then ?refine_1 else x ^ p ^ (n - m)) n_1

pp: case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ (coeff R p n) ⟨fun m ↦ if h : n ≤ m then ?refine_1 else x ^ p ^ (n - m), ?refine_2⟩ = x

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h✝ : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h : n ≤ m
⊢ R
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ ∀ (n_1 : ℕ),
    (fun m ↦
            if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
            else x ^ p ^ (n - m))
          (n_1 + 1) ^
        p =
      (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        n_1

pp: case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ (coeff R p n)
      ⟨fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m),
        ?refine_2⟩ =
    x

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ ∀ (n_1 : ℕ),
    (fun m ↦
            if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
            else x ^ p ^ (n - m))
          (n_1 + 1) ^
        p =
      (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        n_1
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
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
⊢ n ≤ m ∨ n = m + 1 ∨ ¬n ≤ m + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n ≤ m
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

pp: case refine_2.inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n = m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

pp: case refine_2.inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : ¬n ≤ m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

Tactic:
·

Goal state after:
case refine_2.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n ≤ m
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_2.inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n = m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

pp: case refine_2.inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : ¬n ≤ m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

Tactic:
·

Goal state after:
case refine_2.inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : n = m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_2.inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : ¬n ≤ m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m

Tactic:
·

Goal state after:
case refine_2.inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h1 : ¬n ≤ m + 1
⊢ (fun m ↦
          if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
          else x ^ p ^ (n - m))
        (m + 1) ^
      p =
    (fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m))
      m
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ (aeval x.coeff) (verschiebungPoly 0) = x.verschiebungFun.coeff 0

pp: case succ
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ (aeval x.coeff) (verschiebungPoly (n + 1)) = x.verschiebungFun.coeff (n + 1)

Tactic:
·

Goal state after:
case zero
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ (aeval x.coeff) (verschiebungPoly 0) = x.verschiebungFun.coeff 0
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) (verschiebungPoly (n + 1)) = x.verschiebungFun.coeff (n + 1)

Tactic:
·

Goal state after:
case succ
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ (aeval x.coeff) (verschiebungPoly (n + 1)) = x.verschiebungFun.coeff (n + 1)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ (coeff R p n)
      ⟨fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m),
        ⋯⟩ =
    x

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
⊢ (coeff R p n)
      ⟨fun m ↦
        if h_1 : n ≤ m then Nat.leRec x (fun ⦃k⦄ hle xk ↦ (fun x hx ↦ x) (Classical.choose ⋯) ⋯) h_1
        else x ^ p ^ (n - m),
        ⋯⟩ =
    x
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)
f : R →+* S
x : 𝕎 R
⊢ ((map f) (verschiebung x)).coeff 0 = (verschiebung ((map f) x)).coeff 0

pp: case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n✝ : ℕ
⊢ ((map f) (verschiebung x)).coeff (n✝ + 1) = (verschiebung ((map f) x)).coeff (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)
f : R →+* S
x : 𝕎 R
⊢ ((map f) (verschiebung x)).coeff 0 = (verschiebung ((map f) x)).coeff 0
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n✝ : ℕ
⊢ ((map f) (verschiebung x)).coeff (n✝ + 1) = (verschiebung ((map f) x)).coeff (n✝ + 1)

Tactic:
·

Goal state after:
case succ
p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n✝ : ℕ
⊢ ((map f) (verschiebung x)).coeff (n✝ + 1) = (verschiebung ((map f) x)).coeff (n✝ + 1)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) = (MvPolynomial.eval x) 0

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

Tactic:
·

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) = (MvPolynomial.eval x) 0
Module: Mathlib.RingTheory.WittVector.Verschiebung

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

Tactic:
·

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℕ → ℤ
hn : ¬n = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n - 1))
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:
·

Goal state after:
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))
Module: Mathlib.RingTheory.WittVector.MulP

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

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

Goal state before:
pp: case inl
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
y : ModP O p
⊢ preVal K v O p (0 + y) ≤ max (preVal K v O p 0) (preVal K v O p y)

pp: case inr
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x ≠ 0
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)

Tactic:
·

Goal state after:
case inl
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
y : ModP O p
⊢ preVal K v O p (0 + y) ≤ max (preVal K v O p 0) (preVal K v O p y)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case inr.inl
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
hx0 : x ≠ 0
⊢ preVal K v O p (x + 0) ≤ max (preVal K v O p x) (preVal K v O p 0)

pp: case inr.inr
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x ≠ 0
hy0 : y ≠ 0
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)

Tactic:
·

Goal state after:
case inr.inl
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : ModP O p
hx0 : x ≠ 0
⊢ preVal K v O p (x + 0) ≤ max (preVal K v O p x) (preVal K v O p 0)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 1

pp: case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → (bind₁ onePoly) (C (↑p ^ b) * X b ^ p ^ (n - b)) = 0

pp: case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0

Tactic:
·

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 1
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x ≠ 0
hy0 : y ≠ 0
hxy0 : x + y = 0
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)

pp: case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x ≠ 0
hy0 : y ≠ 0
hxy0 : ¬x + y = 0
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)

Tactic:
·

Goal state after:
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x y : ModP O p
hx0 : x ≠ 0
hy0 : y ≠ 0
hxy0 : x + y = 0
⊢ preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → (bind₁ onePoly) (C (↑p ^ b) * X b ^ p ^ (n - b)) = 0

pp: case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0

Tactic:
·

Goal state after:
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → (bind₁ onePoly) (C (↑p ^ b) * X b ^ p ^ (n - b)) = 0
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0

Tactic:
·

Goal state after:
case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case zero
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 0 = (aeval x✝.coeff) (onePoly 0)

pp: case succ
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✝ + 1) = (aeval x✝.coeff) (onePoly (n✝ + 1))

Tactic:
·

Goal state after:
case zero
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 0 = (aeval x✝.coeff) (onePoly 0)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case succ
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✝ + 1) = (aeval x✝.coeff) (onePoly (n✝ + 1))

Tactic:
·

Goal state after:
case succ
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✝ + 1) = (aeval x✝.coeff) (onePoly (n✝ + 1))
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
hj : 0 ≠ i + 1
⊢ (verschiebung (↑p ^ i)).coeff 0 ^ p = 0

pp: case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
n✝ : ℕ
hj : n✝ + 1 ≠ i + 1
⊢ (verschiebung (↑p ^ i)).coeff (n✝ + 1) ^ p = 0

Tactic:
·

Goal state after:
case succ.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
hj : 0 ≠ i + 1
⊢ (verschiebung (↑p ^ i)).coeff 0 ^ p = 0