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

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

Tactic:
]

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑p ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ (p * p ^ (n - k))
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

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

Tactic:
]

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑p ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - (wittStructureInt p Φ k ^ p) ^ p ^ (n - k)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ (map (Int.castRingHom (ZMod p))) (wittStructureInt p Φ k) ^ p =
    (map (Int.castRingHom (ZMod p))) (wittStructureInt p Φ k) ^ p

Tactic:
]

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:
| h n IH =>

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

Tactic:
]

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.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
c : idx × ℕ →₀ ℕ
⊢ (fun x ↦ ↑x)
      (coeff c
            ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
              ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
          ↑p ^ n).num =
    coeff c
        ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
          ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
      ↑p ^ n

Tactic:
]

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
c : idx × ℕ →₀ ℕ
⊢ (fun x ↦ ↑x)
      (coeff c
            ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
              ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
          ↑p ^ n).num =
    coeff c
        ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) -
          ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
      ↑p ^ n
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 × ℕ →₀ ℕ
⊢ ∑ x ∈ Finset.range n, (map (Int.castRingHom ℚ)) (C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)

Tactic:
]

Goal state after:
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 × ℕ →₀ ℕ
⊢ ∑ x ∈ Finset.range n, (map (Int.castRingHom ℚ)) (C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x)) =
    ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
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 × ℕ →₀ ℕ
i : ℕ
hi : i < n
⊢ (map (Int.castRingHom ℚ)) (C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)

Tactic:
]

Goal state after:
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 × ℕ →₀ ℕ
i : ℕ
hi : i < n
⊢ (map (Int.castRingHom ℚ)) (C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
idx : Type u_1
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h : (fun n ↦ (bind₁ f) (wittPolynomial p ℤ n)) = fun n ↦ (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)

Tactic:
]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : (fun n ↦ (bind₁ f) (wittPolynomial p ℤ n)) = fun n ↦ (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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
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)
⊢ ↑((Int.castRingHom ℚ)
            (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))) /
          ↑↑(p ^ n)).num =
    (Int.castRingHom ℚ)
        (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))) /
      ↑↑(p ^ n)

Tactic:
]

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
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)
⊢ ↑((Int.castRingHom ℚ)
            (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))) /
          ↑↑(p ^ n)).num =
    (Int.castRingHom ℚ)
        (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))) /
      ↑↑(p ^ n)
Module: Mathlib.RingTheory.Perfection

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

Tactic:
]

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

Goal state before:
pp: p n : ℕ
⊢ (X (n + 1) -
      ∑ i,
        have x := ⋯;
        ∑ 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)))) =
    X (n + 1) -
      ∑ i,
        ∑ 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:
]

Goal state after:
Module: Mathlib.RingTheory.Perfection

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

Tactic:
]

Goal state after:
case succ
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m : ℕ
ih : ∀ (n : ℕ), (coeffMonoidHom M p n) ((⇑(powMulEquiv (Perfection M p) p).symm)^[m] f) = (coeffMonoidHom M p (n + m)) f
n : ℕ
⊢ (coeffMonoidHom M p (n + 1 + m)) f = (coeffMonoidHom M p (n + (m + 1))) f
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
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))

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

Tactic:
]

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
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))

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

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

Tactic:
]

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
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ (fun n ↦ (aeval x✝.coeff) (ψ n)) n = (fun n ↦ (aeval x✝.coeff) (ψ n)) n

pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ ∀ (n : ℕ), (bind₁ φ) (wittPolynomial p ℤ n) = (bind₁ ψ) (wittPolynomial p ℤ n)

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ ∀ (n : ℕ), (bind₁ φ) (wittPolynomial p ℤ n) = (bind₁ ψ) (wittPolynomial p ℤ n)
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) f = (coeffMonoidHom M p m) f

Tactic:
]

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
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)
⊢ C ↑(p ^ n) ∣
    (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
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
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)
⊢ C ↑(p ^ n) ∣
    (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)
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) f = (coeffMonoidHom M p m) f

Tactic:
]

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)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j + (n - m) = j + (n - m)

Tactic:
]

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 n) f ^ p ^ n

Tactic:
]

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) f = (coeffMonoidHom M p n) f

Tactic:
]

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)) Φ
k : ℕ
⊢ (map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) k

Tactic:
]

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ (map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) k
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ n)

Tactic:
]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ n)
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) ((⇑(powMonoidHom p))^[m] f)

Tactic:
]

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)
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1))
      ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n))

Tactic:
]

Goal state after:
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)
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1))
      ((X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n))
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 : ℕ
⊢ f ((powMulEquiv M (p ^ n)).symm r) = (fun n ↦ f ((powMulEquiv M (p ^ n)).symm r)) n

Tactic:
]

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)
⊢ 1 = 1

Tactic:
]

Goal state after:
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:
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) =
    (eval₂Hom ((map (Int.castRingHom R)).comp C) fun i ↦ (map (Int.castRingHom R)) (wittStructureInt p Φ 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)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
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'_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.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
m : M
n : ℕ
⊢ (coeffMonoidHom N p n) (f m) = (coeffMonoidHom N p n) (f m)

Tactic:
]

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 : ℕ
⊢ φ ((coeffMonoidHom M p n) f) = (fun n ↦ φ ((coeffMonoidHom M p n) f)) n

Tactic:
]

Goal state after: