awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
key :
  Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦
            (expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
              ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
                MvPolynomial (idx × ℕ) ℚ) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : ℕ) ↦
            (expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
              (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦
            (expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
              ((rename fun (i_1 : ℕ) ↦ (i, i_1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
                MvPolynomial (idx × ℕ) ℚ) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : ℕ) ↦
            (expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
              ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
                  (wittStructureInt p Φ i) :
                MvPolynomial (idx × ℕ) ℚ) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
have a : Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
  ((bind₁ fun (i : ℕ) ↦
          (expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
            (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i) :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (W_ ℚ n) :
    MvPolynomial (idx × ℕ) ℚ)
  ((bind₁ fun (i : ℕ) ↦
          (expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
            ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
                (wittStructureInt p Φ i) :
              MvPolynomial (idx × ℕ) ℚ) :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (W_ ℚ n) :
    MvPolynomial (idx × ℕ) ℚ)
Tactic: rw [key]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : ℕ) ↦
            (expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
              (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : ℕ) ↦
            (expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
              ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
                  (wittStructureInt p Φ i) :
                MvPolynomial (idx × ℕ) ℚ) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
have apply : ∀ i ∈ vars (W_ ℚ n),
  i ∈ vars (W_ ℚ n) →
    Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
      ((expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
          (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i) :
        MvPolynomial (idx × ℕ) ℚ)
      ((expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
          ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
              (wittStructureInt p Φ i) :
            MvPolynomial (idx × ℕ) ℚ) :
        MvPolynomial (idx × ℕ) ℚ)
Tactic: apply eval₂Hom_congr' rfl _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
i : ℕ
hi : i ∈ vars (W_ ℚ n)
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i) :
      MvPolynomial (idx × ℕ) ℚ)
    ((expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
            (wittStructureInt p Φ i) :
          MvPolynomial (idx × ℕ) ℚ) :
      MvPolynomial (idx × ℕ) ℚ)
have hi₁ : i < n + 1
Tactic: rw [wittPolynomial_vars, Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
⊢ (C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (↑(p ^ n) : ℤ) ∣
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (b : idx) ↦
              (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
      (∑ i ∈ Finset.range n,
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ i ^ p ^ (n - i)) :
        MvPolynomial (idx × ℕ) ℤ)
have zero : ∀
  (IH :
    ∀ m < 0,
      Eq (α := MvPolynomial (idx × ℕ) ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
            (wittStructureInt p Φ m) :
          MvPolynomial (idx × ℕ) ℚ)
        (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
          MvPolynomial (idx × ℕ) ℚ)),
  (C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (↑(HPow.hPow (β := ℕ) p 0) : ℤ) ∣
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (b : idx) ↦
              (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ 0) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
      (∑ i ∈ Finset.range 0,
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ i ^ p ^ (0 - i)) :
        MvPolynomial (idx × ℕ) ℤ)
Tactic: rcases n with - | n
Cleared hypotheses: n, IH
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
⊢ (C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (↑(p ^ (n + 1)) : ℤ) ∣
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (b : idx) ↦
              (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ (n + 1)) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
      (∑ i ∈ Finset.range (n + 1),
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ i ^ p ^ (n + 1 - i)) :
        MvPolynomial (idx × ℕ) ℤ)
have key : Eq (α := MvPolynomial (idx × ℕ) ℤ)
  ((bind₁ fun (b : idx) ↦
          (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
            ((expand p : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (W_ ℤ n)) :
        (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
      Φ :
    MvPolynomial (idx × ℕ) ℤ)
  ((bind₁ fun (i : ℕ) ↦
          (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
        (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
      (W_ ℤ n) :
    MvPolynomial (idx × ℕ) ℤ)
Tactic: have key := bind₁_rename_expand_wittPolynomial Φ n IH
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
key :
  Eq (α := MvPolynomial (idx × ℕ) ℤ)
    ((bind₁ fun (b : idx) ↦
            (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
              ((expand p : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (W_ ℤ n)) :
          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
        Φ :
      MvPolynomial (idx × ℕ) ℤ)
    ((bind₁ fun (i : ℕ) ↦
            (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
          (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
        (W_ ℤ n) :
      MvPolynomial (idx × ℕ) ℤ)
⊢ (C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (↑(p ^ (n + 1)) : ℤ) ∣
    HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (b : idx) ↦
              (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ (n + 1)) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
      (∑ i ∈ Finset.range (n + 1),
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ i ^ p ^ (n + 1 - i)) :
        MvPolynomial (idx × ℕ) ℤ)
have key₁ : Eq (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
  ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
        (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
      ((bind₁ fun (b : idx) ↦
              (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
                ((expand p : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (W_ ℤ n)) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ) :
    MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
  ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
        (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
      ((bind₁ fun (i : ℕ) ↦
              (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
            (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
          (W_ ℤ n) :
        MvPolynomial (idx × ℕ) ℤ) :
    MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
Tactic: apply_fun map (Int.castRingHom (ZMod (p ^ (n + 1)))) at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1,
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ m) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) m :
        MvPolynomial (idx × ℕ) ℚ)
key :
  Eq (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        ((bind₁ fun (b : idx) ↦
                (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
                  ((expand p : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (W_ ℤ n)) :
              (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
            Φ :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        ((bind₁ fun (i : ℕ) ↦
                (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
            (W_ ℤ n) :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
| ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
        (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
      ((bind₁ fun (b : idx) ↦
              (rename fun (i : ℕ) ↦ (b, i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
                ((expand p : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (W_ ℤ n)) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ) :
    MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
have simp : ((bind₁ fun (i : idx) ↦
        (rename fun (i_1 : ℕ) ↦ (i, i_1) :
            (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
          ((expand p : (a : MvPolynomial ℕ (ZMod (p ^ (n + 1)))) → MvPolynomial ℕ (ZMod (p ^ (n + 1))))
            (W_ (ZMod (p ^ (n + 1))) n)) :
      (a : MvPolynomial idx (ZMod (p ^ (n + 1)))) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) : (a : MvPolynomial idx ℤ) → MvPolynomial idx (ZMod (p ^ (n + 1)))) Φ :
      MvPolynomial idx (ZMod (p ^ (n + 1)))) :
  MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
Tactic: simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        ((bind₁ fun (i : ℕ) ↦
                (expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ i) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ)
            (W_ ℤ n) :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (∑ i ∈ Finset.range (n + 1),
          HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
            ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
            (wittStructureInt p Φ i ^ p ^ (n + 1 - i))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
have succ : ∀ x ∈ Finset.range (n + 1),
  Eq (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) x *
          HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
            ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ x) :
              MvPolynomial (idx × ℕ) ℤ)
            (p ^ (n - x))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x) : MvPolynomial (idx × ℕ) ℤ)
          (wittStructureInt p Φ x ^ p ^ (n + 1 - x))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
Tactic: rw [bind₁, aeval_wittPolynomial, map_sum, map_sum, Finset.sum_congr rfl]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ Eq (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
          HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
            ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
              MvPolynomial (idx × ℕ) ℤ)
            (p ^ (n - k))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) k) : MvPolynomial (idx × ℕ) ℤ)
          (wittStructureInt p Φ k ^ p ^ (n + 1 - k))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
have hk₁ : k ≤ n
Tactic: rw [Finset.mem_range, Nat.lt_succ_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ Eq (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ) (↑p : MvPolynomial (idx × ℕ) ℤ) k *
          HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
            ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
              MvPolynomial (idx × ℕ) ℤ)
            (p ^ (n - k))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((map (Int.castRingHom (ZMod (p ^ (n + 1)))) :
          (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
        (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) k) : MvPolynomial (idx × ℕ) ℤ)
          (wittStructureInt p Φ k ^ p ^ (n + 1 - k))) :
      MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
have succ : (↑(p ^ (n + 1)) : MvPolynomial (idx × ℕ) ℤ) ∣
  (↑(p ^ k) : MvPolynomial (idx × ℕ) ℤ) *
    (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      wittStructureInt p Φ k ^ p ^ (n + 1 - k))
Tactic: rw [← sub_eq_zero, ← map_sub, ← C_dvd_iff_zmod, C_eq_coe_nat, ← Nat.cast_pow,
    ← Nat.cast_pow, C_eq_coe_nat, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
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)
have rw : p ^ (n + 1) = p ^ (k + (n - k) + 1)
Tactic: rw [← pow_add, ← add_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ (k + (n - k) + 1)
have e_a : n = k + (n - k)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ n = k + (n - k)
have e_a : n = n - k + k
Tactic: rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
e_a : n = n - k + k
⊢ n = k + (n - k)
have e_a₁ : n - k = n - k
Tactic: rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ (↑(p ^ (n + 1)) : MvPolynomial (idx × ℕ) ℤ) ∣
    (↑(p ^ k) : MvPolynomial (idx × ℕ) ℤ) *
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (p ^ (n - k)) -
        wittStructureInt p Φ k ^ p ^ (n + 1 - k))
have this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
Tactic: have : p ^ (n + 1) = p ^ k * p ^ (n - k + 1) := by
    rw [← pow_add, ← add_assoc]; congr 2; rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
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 + 1)) : MvPolynomial (idx × ℕ) ℤ) ∣
    (↑(p ^ k) : MvPolynomial (idx × ℕ) ℤ) *
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
          ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
            MvPolynomial (idx × ℕ) ℤ)
          (p ^ (n - k)) -
        wittStructureInt p Φ k ^ p ^ (n + 1 - k))
have succ : (↑(p ^ k * p ^ (n - k + 1)) : MvPolynomial (idx × ℕ) ℤ) ∣
  (↑(p ^ k) : MvPolynomial (idx × ℕ) ℤ) *
    (HPow.hPow (α := MvPolynomial (idx × ℕ) ℤ)
        ((expand p : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittStructureInt p Φ k) :
          MvPolynomial (idx × ℕ) ℤ)
        (p ^ (n - k)) -
      wittStructureInt p Φ k ^ p ^ (n + 1 - k))
Tactic: rw [this]