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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ mapFun (⇑f) (-x) = -mapFun (⇑f) x

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
n : ℕ
x : 𝕎 R
⊢ mapFun (⇑f) (n • x) = n • mapFun (⇑f) x

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
z : ℤ
x : 𝕎 R
⊢ mapFun (⇑f) (z • x) = z • mapFun (⇑f) x

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n : ℕ
⊢ mapFun (⇑f) (x ^ n) = mapFun (⇑f) x ^ n

Tactic:
by

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

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

Tactic:
cases n <;> simp [*, Int.castDef, neg, natCast]

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: p : ℕ
R : Type u_5
i : Fin 0
j : ℕ
⊢ (![] i).coeff j = ![] i j

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ ghostFun 1 = 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ (x + y).ghostFun = x.ghostFun + y.ghostFun

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ (x - y).ghostFun = x.ghostFun - y.ghostFun

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ (x * y).ghostFun = x.ghostFun * y.ghostFun

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
⊢ (-x).ghostFun = -x.ghostFun

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
⊢ (m • x).ghostFun = m • x.ghostFun

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
⊢ (m • x).ghostFun = m • x.ghostFun

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
m : ℕ
⊢ (x ^ m).ghostFun = x.ghostFun ^ m

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
⊢ LeftInverse (fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) ghostFun

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Invertible ↑p
⊢ RightInverse (fun x ↦ mk p fun n ↦ (aeval x) (xInTermsOfW p R n)) ghostFun

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ map (RingHom.id R) = RingHom.id (𝕎 R)

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (bind₁ (W_ R)) (xInTermsOfW p R n) = X n

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ (map f) x = 0 ↔ ∀ (n : ℕ), f (x.coeff n) = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
i : ℕ
hi : i < n + 1
⊢ (aeval x.coeff) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)) = ↑p ^ i * x.coeff i ^ p ^ (n - i)

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ i ≤ n, ↑p ∣ x.coeff i
⊢ ↑p ^ (n + 1) ∣ (ghostComponent n) x

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Fact (Nat.Prime p)
⊢ coeff 1 0 = 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
α : Type u_3
β : Type u_4
inst✝ : Fact (Nat.Prime p)
⊢ coeff 0 0 = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ k * p ^ (n - k + 1)

Tactic:
by

Goal state after:
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, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
⊢ C ↑(p ^ n) ∣
    (bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℤ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)

Tactic:
by

Goal state after:
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)
⊢ f = g

Tactic:
by

Goal state after:
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, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ (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)

Tactic:
by

Goal state after:
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)
⊢ f = g

Tactic:
by

Goal state after:
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 + 1)) (f ^ p) = (coeffMonoidHom M p n) f

Tactic:
by

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

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
x : Perfection M p
⊢ (pthRootMonoidHom M p) ((fun x ↦ x ^ p) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
x : Perfection M p
⊢ (fun x ↦ x ^ p) ((pthRootMonoidHom M p) x) = x

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
x : Perfection M p
⊢ (powMulEquiv (Perfection M p) p) ((pthRootMonoidHom M p) x) = x

Tactic:
by

Goal state after:
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) ((powMulEquiv (Perfection M p) p).symm f) = (coeffMonoidHom M p (n + 1)) f

Tactic:
by

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

Goal state before:
pp: p n : ℕ
⊢ frobeniusPolyAux p n =
    X (n + 1) -
      ∑ i ∈ range n,
        ∑ j ∈ range (p ^ (n - i)),
          (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n j : ℕ
hj : j < p ^ n
⊢ p ^ (n - v p (j + 1)) ∣ (p ^ n).choose (j + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n : ℕ
⊢ (coeffMonoidHom M p (m + Nat.zero)) (f ^ p ^ Nat.zero) = (coeffMonoidHom M p m) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

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

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
⊢ j - v p (j + 1) + n = i + j + (n - i - v p (j + 1))

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m : ℕ
hmn : m ≤ n
⊢ (coeffMonoidHom M p n) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p (n - m)) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
r : M
n : ℕ
⊢ (fun n ↦ f ((powMulEquiv M (p ^ n)).symm r)) (n + 1) ^ p = (fun n ↦ f ((powMulEquiv M (p ^ n)).symm r)) n

Tactic:
by

Goal state after:
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)
⊢ ↑p ^ n * ⅟↑p ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
x✝ : ℕ
⊢ (coeffMonoidHom N p x✝) ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm 1), ⋯⟩ = (coeffMonoidHom N p x✝) 1

Tactic:
by

Goal state after:
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)) Φ
⊢ φ = wittStructureInt p Φ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
x y : M
x✝ : ℕ
⊢ (coeffMonoidHom N p x✝) ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm (x * y)), ⋯⟩ =
    (coeffMonoidHom N p x✝)
      (⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm x), ⋯⟩ * ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm y), ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
⊢ (coeffMonoidHom N p 0).comp
      ((fun f ↦ { toFun := fun r ↦ ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* Perfection N p
⊢ (fun f ↦ { toFun := fun r ↦ ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ })
      ((coeffMonoidHom N p 0).comp f) =
    f

Tactic:
by

Goal state after:
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 : ℕ
⊢ (aeval fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    (aeval fun i ↦ (rename (Prod.mk i)) (W_ R n)) Φ

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ constantCoeff (wittStructureRat p Φ 0) = constantCoeff Φ

Tactic:
by

Goal state after:
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 : ℕ
⊢ constantCoeff (wittStructureRat p Φ n) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
x✝¹ x✝ : M →* N
⊢ { toFun := fun r ↦ ⟨fun n ↦ (x✝¹ * x✝) ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ } =
    { toFun := fun r ↦ ⟨fun n ↦ x✝¹ ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ } *
      { toFun := fun r ↦ ⟨fun n ↦ x✝ ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: p : ℕ
M : Type u_2
N : Type u_3
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
inst✝ : CommMonoid N
e : M →* N
x : M
⊢ (coeffMonoidHom N p 0) (((liftMonoidHom p M N) e) x) = e x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝² : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
N : Type u_3
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
φ : M →* N
f : Perfection M p
n : ℕ
⊢ (fun n ↦ φ ((coeffMonoidHom M p n) f)) (n + 1) ^ p = (fun n ↦ φ ((coeffMonoidHom M p n) f)) n

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ constantCoeff (wittStructureInt p Φ 0) = constantCoeff Φ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝² : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
N : Type u_3
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
φ : M →* N
⊢ ⟨fun n ↦ φ ((coeffMonoidHom M p n) 1), ⋯⟩ = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝² : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
N : Type u_3
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
φ : M →* N
x✝¹ x✝ : Perfection M p
⊢ ⟨fun n ↦ φ ((coeffMonoidHom M p n) (x✝¹ * x✝)), ⋯⟩ =
    ⟨fun n ↦ φ ((coeffMonoidHom M p n) x✝¹), ⋯⟩ * ⟨fun n ↦ φ ((coeffMonoidHom M p n) x✝), ⋯⟩

Tactic:
by

Goal state after:
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 : ℕ
⊢ Function.Injective ⇑(Int.castRingHom ℚ)

Tactic:
by

Goal state after:
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
⊢ pthRoot R p = ↑(frobeniusEquiv (Perfection R p) p).symm

Tactic:
by

Goal state after:
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
⊢ ⇑(pthRootMonoidHom R p) = ⇑↑(frobeniusEquiv (Perfection R p) p).symm

Tactic:
by

Goal state after:
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
⊢ (pthRoot R p).comp (frobenius (Perfection R p) p) = RingHom.id (Perfection R p)

Tactic:
by

Goal state after:
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 : ℕ
⊢ constantCoeff (wittStructureInt p Φ n) = 0

Tactic:
by

Goal state after:
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
f : Perfection R p
n : ℕ
hfn : (coeff R p n) f ≠ 0
k✝ k : ℕ
ih : (coeff R p (n + k)) f ≠ 0
h : (coeff R p (n + k.succ)) f = 0
⊢ (coeff R p (n + k)) f = 0

Tactic:
by

Goal state after:
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

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (wittStructureRat p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
by

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
by

Goal state after:
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 : ℕ
h1 : n ≤ m
⊢ n ≤ m + 1

Tactic:
by

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
g f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
hf : IsPoly p f
⊢ IsPoly p fun R _Rcr ↦ g ∘ f

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ x.verschiebungFun.coeff n = if n = 0 then 0 else x.coeff (n - 1)

Tactic:
by

Goal state after:
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

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
⊢ (ghostComponent 0) x.verschiebungFun = 0

Tactic:
by

Goal state after:
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 : ℕ
h1 : ¬n ≤ m + 1
⊢ ¬n ≤ m

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ (ghostComponent (n + 1)) x.verschiebungFun = ↑p * (ghostComponent n) x

Tactic:
by

Goal state after:
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 : ℕ
h1 : ¬n ≤ m + 1
h1' : ¬n ≤ m
⊢ n - m = n - (m + 1) + 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ IsPoly p fun R _Rcr ↦ verschiebungFun

Tactic:
by

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

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

Tactic:
by

Goal state after: