awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih :
  (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
succ :
  (bind₁ (Function.uncurry ![wittMulN p n, X]) : (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
      ((bind₁ fun (i : Fin 2) ↦
            (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k) :
          (a : MvPolynomial (Fin 2) ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ)
        (HAdd.hAdd (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑(n + 1) : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
⊢ (bind₁ (wittMulN p (n + 1)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑(n + 1) : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)

Tactic:
rw [wittMulN, ← bind₁_bind₁, wittAdd, wittStructureInt_prop]

Premises used: WittVector.wittAdd, wittStructureInt_prop, MvPolynomial.bind₁_bind₁, WittVector.wittMulN
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih :
  (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
succ :
  HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
      ((bind₁ (Function.uncurry ![wittMulN p n, X]) :
            (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
          ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k)) :
        MvPolynomial ℕ ℤ)
      ((bind₁ (Function.uncurry ![wittMulN p n, X]) :
            (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
          ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k)) :
        MvPolynomial ℕ ℤ) =
    HAdd.hAdd (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) 1 * wittPolynomial p ℤ k
⊢ (bind₁ (Function.uncurry ![wittMulN p n, X]) : (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
      ((bind₁ fun (i : Fin 2) ↦
            (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k) :
          (a : MvPolynomial (Fin 2) ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ)
        (HAdd.hAdd (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑(n + 1) : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)

Tactic:
simp only [map_add, Nat.cast_succ, bind₁_X_right]

Premises used: Nat.cast_succ, map_add, MvPolynomial.bind₁_X_right
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih :
  (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
succ :
  HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
      ((bind₁ (Function.uncurry ![wittMulN p n, X] ∘ Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
          (wittPolynomial p ℤ k) :
        MvPolynomial ℕ ℤ)
      ((bind₁ (Function.uncurry ![wittMulN p n, X] ∘ Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
          (wittPolynomial p ℤ k) :
        MvPolynomial ℕ ℤ) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) + wittPolynomial p ℤ k
⊢ HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
      ((bind₁ (Function.uncurry ![wittMulN p n, X]) :
            (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
          ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k)) :
        MvPolynomial ℕ ℤ)
      ((bind₁ (Function.uncurry ![wittMulN p n, X]) :
            (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
          ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k)) :
        MvPolynomial ℕ ℤ) =
    HAdd.hAdd (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) 1 * wittPolynomial p ℤ k

Tactic:
rw [add_mul, one_mul, bind₁_rename, bind₁_rename]

Premises used: add_mul, MvPolynomial.bind₁_rename, one_mul
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih :
  (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
⊢ HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
      ((bind₁ (Function.uncurry ![wittMulN p n, X] ∘ Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
          (wittPolynomial p ℤ k) :
        MvPolynomial ℕ ℤ)
      ((bind₁ (Function.uncurry ![wittMulN p n, X] ∘ Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
          (wittPolynomial p ℤ k) :
        MvPolynomial ℕ ℤ) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) + wittPolynomial p ℤ k

Tactic:
simp only [ih, Function.uncurry, Function.comp_def, bind₁_X_left, AlgHom.id_apply,
      Matrix.cons_val_zero, Matrix.cons_val_one]

Premises used: MvPolynomial.bind₁_X_left, Matrix.cons_val_one, Matrix.cons_val_zero, Function.comp_def, Function.uncurry, AlgHom.id_apply
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n k : ℕ
zero :
  (bind₁ (wittMulN p 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑0 : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
succ :
  ∀ (n : ℕ)
    (ih :
      (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
        HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)),
    (bind₁ (wittMulN p (n + 1)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
      HMul.hMul (α := MvPolynomial ℕ ℤ) (↑(n + 1) : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
⊢ (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)

Tactic:
induction n with
  | zero => simp [wittMulN, zero_mul, bind₁_zero_wittPolynomial]
  | succ n ih =>
    rw [wittMulN, ← bind₁_bind₁, wittAdd, wittStructureInt_prop]
    simp only [map_add, Nat.cast_succ, bind₁_X_right]
    rw [add_mul, one_mul, bind₁_rename, bind₁_rename]
    simp only [ih, Function.uncurry, Function.comp_def, bind₁_X_left, AlgHom.id_apply,
      Matrix.cons_val_zero, Matrix.cons_val_one]

Premises used: add_mul, Nat.cast_succ, MvPolynomial.bind₁_X_left, MulZeroClass.zero_mul, Matrix.cons_val_one, Matrix.cons_val_zero, map_add, WittVector.wittAdd, MvPolynomial.bind₁_rename, wittStructureInt_prop, Function.comp_def, MvPolynomial.bind₁_bind₁, WittVector.bind₁_zero_wittPolynomial, Function.uncurry, MvPolynomial.bind₁_X_right, WittVector.wittMulN, one_mul, AlgHom.id_apply
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
rw :
  Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ (wittStructureRat p Φ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : ℕ) ↦
            (bind₁ fun (k : ℕ) ↦
                  (bind₁ fun (i : idx) ↦
                        (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                      (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                    Φ :
                (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
              (xInTermsOfW p ℚ i) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ (wittStructureRat p Φ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ (xInTermsOfW p ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (W_ ℚ n)) :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
rw [bind₁_bind₁]

Premises used: MvPolynomial.bind₁_bind₁
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ (wittStructureRat p Φ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : ℕ) ↦
            (bind₁ fun (k : ℕ) ↦
                  (bind₁ fun (i : idx) ↦
                        (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                      (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                    Φ :
                (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
              (xInTermsOfW p ℚ i) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
eval₂Hom_congr (RingHom.ext_rat _ _) rfl rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_rat, rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ (wittStructureRat p Φ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : ℕ) ↦
            (bind₁ fun (k : ℕ) ↦
                  (bind₁ fun (i : idx) ↦
                        (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                      (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                    Φ :
                (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
              (xInTermsOfW p ℚ i) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
exact eval₂Hom_congr (RingHom.ext_rat _ _) rfl rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_rat, rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
rw :
  Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (X n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ :
      MvPolynomial (idx × ℕ) ℚ)
rw₁ rw₂ :
  Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ n) :
          (a : MvPolynomial idx ℚ) → 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 × ℕ) ℚ)
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ (xInTermsOfW p ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (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 × ℕ) ℚ)

Tactic:
rw [bind₁_xInTermsOfW_wittPolynomial p _ n, bind₁_X_right]

Premises used: bind₁_xInTermsOfW_wittPolynomial, MvPolynomial.bind₁_X_right
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∃! φ : ℕ → MvPolynomial (idx × ℕ) ℚ,
    ∀ (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 × ℕ) ℚ)

Tactic:
⟨wittStructureRat p Φ, ?_, ?_⟩

Premises used: wittStructureRat, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
refine_1 :
  (fun (φ : ℕ → MvPolynomial (idx × ℕ) ℚ) ↦
      ∀ (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 × ℕ) ℚ))
    (wittStructureRat p Φ)
refine_2 :
  ∀ (y : ℕ → MvPolynomial (idx × ℕ) ℚ),
    (fun (φ : ℕ → MvPolynomial (idx × ℕ) ℚ) ↦
          ∀ (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 × ℕ) ℚ))
        y →
      y = wittStructureRat p Φ
⊢ ∃! φ : ℕ → MvPolynomial (idx × ℕ) ℚ,
    ∀ (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 × ℕ) ℚ)

Tactic:
refine ⟨wittStructureRat p Φ, ?_, ?_⟩
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ (wittStructureRat 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 × ℕ) ℚ)

Tactic:
apply wittStructureRat_prop

Premises used: wittStructureRat_prop
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 × ℕ) ℚ)
refine_2 : ∀ (n : ℕ), φ n = wittStructureRat p Φ n
⊢ φ = wittStructureRat p Φ

Tactic:
funext n
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 × ℕ) ℚ)
n : ℕ
rw : φ n = (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (X n)
rw₁ rw₂ : φ n = φ n
⊢ φ n =
    (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ (W_ ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n))

Tactic:
rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]

Premises used: bind₁_wittPolynomial_xInTermsOfW, MvPolynomial.bind₁_X_right
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 × ℕ) ℚ)
n : ℕ
refine_2 :
  (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ (W_ ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)) =
    wittStructureRat p Φ n
⊢ φ n = wittStructureRat p Φ n

Tactic:
rw [show φ n = bind₁ φ (bind₁ (W_ ℚ) (xInTermsOfW p ℚ n)) by
        rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]]
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 × ℕ) ℚ)
n : ℕ
refine_2 :
  (bind₁ fun (i : ℕ) ↦ (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ i) :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (xInTermsOfW p ℚ n) =
    wittStructureRat p Φ n
⊢ (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      ((bind₁ (W_ ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)) =
    wittStructureRat p Φ n

Tactic:
rw [bind₁_bind₁]

Premises used: MvPolynomial.bind₁_bind₁
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 × ℕ) ℚ)
n : ℕ
⊢ (bind₁ fun (i : ℕ) ↦ (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ i) :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (xInTermsOfW p ℚ n) =
    wittStructureRat p Φ n

Tactic:
eval₂Hom_congr (RingHom.ext_rat _ _) (funext H) rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_rat, wittStructureRat, funext, rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 × ℕ) ℚ)
n : ℕ
⊢ (bind₁ fun (i : ℕ) ↦ (bind₁ φ : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ i) :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
      (xInTermsOfW p ℚ n) =
    wittStructureRat p Φ n

Tactic:
exact eval₂Hom_congr (RingHom.ext_rat _ _) (funext H) rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_rat, funext, rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial ℕ ℚ) =
    HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
      (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i))))

Tactic:
have := xInTermsOfW_aux p ℚ n
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial ℕ ℚ) =
    HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
      (∑ i ∈ Finset.range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i))))
⊢ Eq.{u_2 + 1} (α := MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) n) : MvPolynomial ℕ ℚ)) :
      MvPolynomial (idx × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
          (∑ i ∈ Finset.range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i))))) :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
replace := congr_arg (bind₁ fun k : ℕ => bind₁ (fun i => rename (Prod.mk i) (W_ ℚ k)) Φ) this