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

Goal state before:
pp: case zero
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : CharP (R ⧸ I) p
x : Perfection (R ⧸ I) p
⊢ x.teichmullerAux 0 ≡ x.teichmullerAux (0 + 1) [SMOD I ^ 0]

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: 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✝ : ℕ
⊢ (Ideal.Quotient.mk I) 1 = (coeff (R ⧸ I) p x✝) 1 ∧ 1 ^ p ^ x✝ ≡ 1 [SMOD I ^ (x✝ + 1)]

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: 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) * Quotient.out ((coeff (R ⧸ I) p n) y)) =
    (coeff (R ⧸ I) p n) (x * y)

Tactic:
simp

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

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

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: 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 : Perfection R p
n : ℕ
⊢ (Ideal.Quotient.mk I) ((coeffMonoidHom R p n) x) = (coeff (R ⧸ I) p n) ((mapMonoidHom p ↑(Ideal.Quotient.mk I)) x) ∧
    (coeffMonoidHom R p n) x ^ p ^ n ≡ (coeffMonoidHom R p 0) x [SMOD I ^ (n + 1)]

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: 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✝
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_2
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x✝ : Perfection R p
⊢ ((liftMonoidHom p (Perfection R p) R).symm
        (((liftMonoidHom p (Perfection (R ⧸ I) p) R) (teichmuller p I)).comp (mapMonoidHom p ↑(Ideal.Quotient.mk I))))
      x✝ =
    ((liftMonoidHom p (Perfection R p) R).symm (MonoidHom.id (Perfection R p))) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: 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✝
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_2
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x✝ : Perfection (R ⧸ I) p
⊢ ((liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)).symm
        ((mapMonoidHom p ↑(Ideal.Quotient.mk I)).comp ((liftMonoidHom p (Perfection (R ⧸ I) p) R) (teichmuller p I))))
      x✝ =
    ((liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)).symm (MonoidHom.id (Perfection (R ⧸ I) p))) x✝

Tactic:
simp

Goal state after:
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 : ℕ
⊢ i ∈ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars → i ∈ range n

Tactic:
intro H
    replace H := vars_sum_subset _ _ H
    rw [mem_biUnion] at H
    rcases H with ⟨j, hj, H⟩
    rw [vars_C_mul] at H
    swap
    · apply pow_ne_zero
      exact mod_cast hp.1.ne_zero
    rw [mem_range] at hj
    replace H := (ih j hj).2 (vars_pow _ _ H)
    rw [mem_range] at H

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 j : ℕ
hj : j < n
H : i < j + 1
⊢ 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)
⊢ n ∉ (∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)).vars

Tactic:
intro H
    replace H := vars_sum_subset _ _ H
    rw [mem_biUnion] at H
    rcases H with ⟨j, hj, H⟩
    rw [vars_C_mul] at H
    swap
    · apply pow_ne_zero
      exact mod_cast hp.1.ne_zero
    rw [mem_range] at hj
    replace H := (ih j hj).2 (vars_pow _ _ H)
    rw [mem_range] at 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 < j + 1
⊢ False
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case zero
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
IH : ∀ m < 0, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
⊢ C ↑(p ^ 0) ∣
    (bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℤ 0)) Φ -
      ∑ i ∈ Finset.range 0, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (0 - i)

Tactic:
simp

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

Tactic:
simp

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

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

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✝ : ℕ
⊢ ((map (RingHom.id R)) x✝).coeff n✝ = ((RingHom.id (𝕎 R)) x✝).coeff n✝

Tactic:
simp

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

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

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

Goal state before:
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
⊢ (map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n

Tactic:
rw [wittStructureInt, map_mapRange_eq_iff, Int.coe_castRingHom]

Goal state after:
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
⊢ ∀ (d : idx × ℕ →₀ ℕ),
    (fun x ↦ ↑x) (coeff d (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n)).num =
      coeff d (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n)
Module: Mathlib.RingTheory.Perfection

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Perfection

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Perfection

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

Tactic:
simp

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

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✝ : M
⊢ ((coeffMonoidHom N p 0).comp
        ((fun f ↦ { toFun := fun r ↦ ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ })
          f))
      x✝ =
    f x✝

Tactic:
simp

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
x✝ : M
n✝ : ℕ
⊢ (coeffMonoidHom N p n✝)
      ({ toFun := fun r ↦ ⟨fun n ↦ (x✝² * x✝¹) ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
        x✝) =
    (coeffMonoidHom N p n✝)
      (({ 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' := ⋯ })
        x✝)

Tactic:
simp

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
n✝ : ℕ
⊢ (coeffMonoidHom N p n✝) ⟨fun n ↦ φ ((coeffMonoidHom M p n) 1), ⋯⟩ = (coeffMonoidHom N p n✝) 1

Tactic:
simp

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
n✝ : ℕ
⊢ (coeffMonoidHom N p n✝) ⟨fun n ↦ φ ((coeffMonoidHom M p n) (x✝¹ * x✝)), ⋯⟩ =
    (coeffMonoidHom N p n✝) (⟨fun n ↦ φ ((coeffMonoidHom M p n) x✝¹), ⋯⟩ * ⟨fun n ↦ φ ((coeffMonoidHom M p n) x✝), ⋯⟩)

Tactic:
simp

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

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
x✝ : Perfection R p
n✝ : ℕ
⊢ (coeff R p n✝) (((pthRoot R p).comp (frobenius (Perfection R p) p)) x✝) =
    (coeff R p n✝) ((RingHom.id (Perfection R p)) x✝)

Tactic:
simp

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

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u₁
inst✝² : CommSemiring R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n✝ n : ℕ
ih : (⇑(frobeniusEquiv R p).symm)^[n] (f 0) = f n
⊢ f n = f n.succ ^ p

Tactic:
hf

Goal state after:
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u₁
inst✝² : CommSemiring R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n✝ n : ℕ
ih : (⇑(frobeniusEquiv R p).symm)^[n] (f 0) = f n
⊢ f n = f n
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
k : ℕ
⊢ (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)

Tactic:
exact mulN_coeff n x k

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ ∀ x ∈ range (p ^ (n - i)),
    C (↑p ^ i) *
          ((C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (x + 1) *
              (X i ^ p) ^ (p ^ (n - i) - (x + 1)) *
            ↑((p ^ (n - i)).choose (x + 1))) *
        C (⅟↑p ^ n) =
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (x + 1)) * frobeniusPolyAux p i ^ (x + 1) *
            C ↑((p ^ (n - i)).choose (x + 1) / p ^ (n - i - v p (x + 1)) * p ^ (x - v p (x + 1))))

Tactic:
intro j

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
⊢ j ∈ range (p ^ (n - i)) →
    C (↑p ^ i) *
          ((C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (j + 1) *
              (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
            ↑((p ^ (n - i)).choose (j + 1))) *
        C (⅟↑p ^ n) =
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((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))))
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
m : ℕ
⊢ (x * ↑p ^ 0).coeff (m + 0) = x.coeff m ^ p ^ 0

Tactic:
simp

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

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
⊢ ((⇑verschiebung)^[0] x).coeff (k + 0) = x.coeff k

Tactic:
simp

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

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ (⇑verschiebung)^[0] x * y = (⇑verschiebung)^[0] (x * (⇑frobenius)^[0] y)

Tactic:
simp

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

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k : ℕ
⊢ ((⇑frobenius)^[0] x).coeff k = x.coeff k ^ p ^ 0

Tactic:
simp

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ ((⇑frobenius)^[i + 1] x).coeff k = x.coeff k ^ p ^ (i + 1)

Tactic:
rw [iterate_succ_apply', coeff_frobenius_charP, ih]

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ (x.coeff k ^ p ^ i) ^ p = x.coeff k ^ p ^ (i + 1)
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ (⇑verschiebung ∘ ⇑frobenius)^[0] x = x * ↑p ^ 0

Tactic:
simp

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 → 𝕎 R
hf : IsPoly₂ p f
hg : IsPoly₂ p g
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y

Tactic:
by
  obtain ⟨φ, hf⟩ := hf
  obtain ⟨ψ, hg⟩ := hg
  intros
  ext n
  rw [hf, hg, poly_eq_of_wittPolynomial_bind_eq' p φ ψ]
  intro k
  apply MvPolynomial.funext
  intro x
  simp only [hom_bind₁]
  specialize h (ULift ℤ) (mk p fun i => ⟨x (0, i)⟩) (mk p fun i => ⟨x (1, i)⟩) k
  simp only [ghostComponent_apply, aeval_eq_eval₂Hom] at h
  apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective
  simp only [← RingEquiv.coe_toRingHom, map_eval₂Hom]
  convert! h using 1
  all_goals
    simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    ext1
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    ext ⟨b, _⟩
    fin_cases b <;> simp only [coeff_mk, uncurry] <;> rfl

Goal state after:
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
g : PreTilt O p
⊢ valAux K v O p (0 * g) = valAux K v O p 0 * valAux K v O p g

Tactic:
simp

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

Goal state before:
pp: case pos
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ x.coeff n = (aeval x.coeff) (X n)

Tactic:
simp

Goal state after:
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf : f ≠ 0
⊢ valAux K v O p (f * 0) = valAux K v O p f * valAux K v O p 0

Tactic:
simp

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

Goal state before:
pp: case neg
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ 0 = (aeval x.coeff) 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
g : PreTilt O p
⊢ valAux K v O p (0 + g) ≤ max (valAux K v O p 0) (valAux K v O p g)

Tactic:
simp

Goal state after:
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf : f ≠ 0
⊢ valAux K v O p (f + 0) ≤ max (valAux K v O p f) (valAux K v O p 0)

Tactic:
simp

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

Goal state before:
pp: case refine_1
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 1 - 1 ∈ ⊥

Tactic:
← iInf_ker_truncate,

Goal state after:
case refine_1
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 1 - 1 ∈ ⨅ i, RingHom.ker (truncate i)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_2
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ y✝ : S
⊢ liftFun f (x✝ * y✝) - liftFun f x✝ * liftFun f y✝ ∈ ⊥

Tactic:
← iInf_ker_truncate,

Goal state after:
case refine_2
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ y✝ : S
⊢ liftFun f (x✝ * y✝) - liftFun f x✝ * liftFun f y✝ ∈ ⨅ i, RingHom.ker (truncate i)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_3
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 0 - 0 ∈ ⊥

Tactic:
← iInf_ker_truncate,

Goal state after:
case refine_3
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 0 - 0 ∈ ⨅ i, RingHom.ker (truncate i)