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,
    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 : idx × ℕ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    (∑ x ∈ Finset.range n,
      (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
          ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x) : MvPolynomial (idx × ℕ) ℤ)
          (wittStructureInt p Φ x ^ p ^ (n - x))))
    (∑ i ∈ Finset.range n,
      HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
        (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
          (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
          (p ^ (n - i))))
have apply : ∀ x ∈ Finset.range n,
  (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
      (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
        ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x) : MvPolynomial (idx × ℕ) ℤ)
        (wittStructureInt p Φ x ^ p ^ (n - x))) =
    HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) x) : MvPolynomial (idx × ℕ) ℚ)
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
        (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) x)
        (p ^ (n - x)))
Tactic: apply 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 : ℕ
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 : idx × ℕ →₀ ℕ
i : ℕ
hi : i ∈ Finset.range n
⊢ (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
      (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
        ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
        (wittStructureInt p Φ i ^ p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
        (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
        (p ^ (n - i)))
have hi₁ : i < n
Tactic: rw [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 : idx × ℕ →₀ ℕ
i : ℕ
hi : i < n
⊢ (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
      (HMul.hMul (α := MvPolynomial (idx × ℕ) ℤ)
        ((C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i) : MvPolynomial (idx × ℕ) ℤ)
        (wittStructureInt p Φ i ^ p ^ (n - i))) =
    HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
      (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
        (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
        (p ^ (n - i)))
have simp : HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
      ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) (↑p : ℤ)) : MvPolynomial (idx × ℕ) ℚ)
      i *
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
      (p ^ (n - i)) =
  HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (↑p : ℚ)) i *
    HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i) (p ^ (n - i))
Tactic: simp only [IH i hi, map_mul, map_pow, map_C]
-- 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 : idx × ℕ →₀ ℕ
sum_induction_steps :
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : 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 × ℕ) ℚ)
    (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
          (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
            (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
            (p ^ (n - i))) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) n = (↑(↑(p ^ n) : ℤ) : ℚ)
have norm_cast : p ^ n = p ^ n
Tactic: norm_cast
-- 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 : idx × ℕ →₀ ℕ
sum_induction_steps :
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : 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 × ℕ) ℚ)
    (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
          (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
            (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
            (p ^ (n - i))) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ (↑(p ^ n) : ℤ) ∣
    coeff c
      (HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
        ((bind₁ fun (i : idx) ↦
                (rename fun (i_1 : ℕ) ↦ (i, i_1) : (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 h : ∀ (c : idx × ℕ →₀ ℕ),
  (↑(p ^ n) : ℤ) ∣
    coeff c
      (HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
        ((bind₁ fun (i : idx) ↦
                (rename fun (i_1 : ℕ) ↦ (i, i_1) : (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 × ℕ) ℤ))
Tactic: revert c
Cleared hypotheses: c
-- 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 × ℕ) ℚ)
sum_induction_steps :
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : 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 × ℕ) ℚ)
    (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial (idx × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (idx × ℕ) ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial (idx × ℕ) ℚ)
          (HPow.hPow (α := MvPolynomial (idx × ℕ) ℚ)
            (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) i)
            (p ^ (n - i))) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ ∀ (c : idx × ℕ →₀ ℕ),
    (↑(p ^ n) : ℤ) ∣
      coeff c
        (HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
          ((bind₁ fun (i : idx) ↦
                  (rename fun (i_1 : ℕ) ↦ (i, i_1) : (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 h : (C : (a : ℤ) → MvPolynomial (idx × ℕ) ℤ) (↑(p ^ n) : ℤ) ∣
  HSub.hSub (α := MvPolynomial (idx × ℕ) ℤ) (β := MvPolynomial (idx × ℕ) ℤ)
    ((bind₁ fun (i : idx) ↦
            (rename fun (i_1 : ℕ) ↦ (i, i_1) : (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 × ℕ) ℤ)
Tactic: rw [← C_dvd_iff_dvd_coeff]
-- 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 (α := MvPolynomial (idx × ℕ) ℤ)
    ((bind₁ (wittStructureInt p Φ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
      MvPolynomial (idx × ℕ) ℤ)
    ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
        Φ :
      MvPolynomial (idx × ℕ) ℤ)
have a : Eq (α := MvPolynomial (idx × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ (wittStructureInt p Φ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
        MvPolynomial (idx × ℕ) ℤ) :
    MvPolynomial (idx × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ) :
    MvPolynomial (idx × ℕ) ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ (wittStructureInt p Φ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
            Φ :
          MvPolynomial (idx × ℕ) ℤ) :
      MvPolynomial (idx × ℕ) ℚ)
have this : Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
  ((bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ)) :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (W_ ℚ n) :
    MvPolynomial (idx × ℕ) ℚ)
  ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
        (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
    MvPolynomial (idx × ℕ) ℚ)
Tactic: have := wittStructureRat_prop p (map (Int.castRingHom ℚ) Φ) n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) : MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
⊢ φ = wittStructureInt p Φ
have h₁ : ∀ (k : ℕ), φ k = wittStructureInt p Φ k
Tactic: funext k
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) : MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
k : ℕ
⊢ φ k = wittStructureInt p Φ k
have h₁ : Eq (α := MvPolynomial (idx × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k) :
    MvPolynomial (idx × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ k) :
    MvPolynomial (idx × ℕ) ℚ)
Tactic: apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) : MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
k : ℕ
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k) :
      MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ k) :
      MvPolynomial (idx × ℕ) ℚ)
have h₁ : Eq (α := MvPolynomial (idx × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k) :
    MvPolynomial (idx × ℕ) ℚ)
  (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) k :
    MvPolynomial (idx × ℕ) ℚ)
Tactic: rw [map_wittStructureInt]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) : MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
k : ℕ
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k) :
      MvPolynomial (idx × ℕ) ℚ)
    (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) k :
      MvPolynomial (idx × ℕ) ℚ)
have h₁ : ∀ (k : ℕ),
  Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k) :
      MvPolynomial (idx × ℕ) ℚ)
    (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) k :
      MvPolynomial (idx × ℕ) ℚ)
Tactic: revert k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) : MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
⊢ ∀ (k : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k) :
        MvPolynomial (idx × ℕ) ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) k :
        MvPolynomial (idx × ℕ) ℚ)
have h₁ : Eq.{max 1 (u_2 + 1)} (α := (x : ℕ) → MvPolynomial (idx × ℕ) ℚ)
  (fun (k : ℕ) ↦ (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k))
  (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ))
Tactic: refine congr_fun ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) : MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
⊢ Eq.{max 1 (u_2 + 1)} (α := (x : ℕ) → MvPolynomial (idx × ℕ) ℚ)
    (fun (k : ℕ) ↦ (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k))
    (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ))
have h₁ : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      MvPolynomial (idx × ℕ) ℚ)
Tactic: apply ExistsUnique.unique (wittStructureRat_existsUnique p (map (Int.castRingHom ℚ) Φ))
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ φ : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) : MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ :
        MvPolynomial (idx × ℕ) ℤ)
h₁ :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (k : ℕ) ↦
              (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k) :
            (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
          (W_ ℚ n) :
        MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
        MvPolynomial (idx × ℕ) ℚ)
⊢ Eq.{max 1 (u_2 + 1)} (α := (x : ℕ) → MvPolynomial (idx × ℕ) ℚ)
    (fun (k : ℕ) ↦ (map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (φ k))
    (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ))
have h₂ : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ)) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      MvPolynomial (idx × ℕ) ℚ)
Tactic: apply ExistsUnique.unique (wittStructureRat_existsUnique p (map (Int.castRingHom ℚ) Φ))