awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 (α := 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 × ℕ) ℚ)
    ((bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ)) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
have key := (wittStructureRat_prop p (map (Int.castRingHom ℚ) Φ) n).symm
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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) ↦ (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 × ℕ) ℚ)
    ((bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ)) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (W_ ℚ n) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((expand p : (a : MvPolynomial (idx × ℕ) ℚ) → 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 × ℕ) ℚ) :
      MvPolynomial (idx × ℕ) ℚ)
    ((expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ)) :
              (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
            (W_ ℚ n) :
          MvPolynomial (idx × ℕ) ℚ) :
      MvPolynomial (idx × ℕ) ℚ)

Tactic:
apply_fun expand p at key

Premises used: MvPolynomial.expand
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 × ℕ) ℚ)
    ((expand p : (a : MvPolynomial (idx × ℕ) ℚ) → 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 × ℕ) ℚ) :
      MvPolynomial (idx × ℕ) ℚ)
    ((expand p : (a : MvPolynomial (idx × ℕ) ℚ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ)) :
              (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
            (W_ ℚ n) :
          MvPolynomial (idx × ℕ) ℚ) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ 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 × ℕ) ℚ)

Tactic:
simp only [expand_bind₁] at key

Premises used: MvPolynomial.expand_bind₁
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 × ℕ) ℚ)
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 × ℕ) ℚ)
⊢ 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 × ℕ) ℚ)

Tactic:
rw [key]
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 × ℕ) ℚ)
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 × ℕ) ℚ)
⊢ 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:
apply eval₂Hom_congr' rfl _ rfl

Premises used: MvPolynomial.eval₂Hom_congr', rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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)
⊢ i < n + 1

Tactic:
rw [wittPolynomial_vars, Finset.mem_range] at hi

Premises used: wittPolynomial_vars, Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 < n + 1
⊢ 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:
simp only [IH i hi]
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
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:
simp
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 (α := 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
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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 × ℕ) ℤ)
⊢ 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

Premises used: ZMod, HPow.hPow, HAdd.hAdd, Int.castRingHom, MvPolynomial.map, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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))))
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))))
| ((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))))

Tactic:
simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]

Premises used: MvPolynomial.map_bind₁, MvPolynomial.map_expand, MvPolynomial.map_rename, map_wittPolynomial
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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))))
⊢ Eq (α := MvPolynomial (idx × ℕ) (ZMod (p ^ (n + 1))))
    ((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))))
    ((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:
conv_lhs at key => simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]

Premises used: MvPolynomial.map_bind₁, MvPolynomial.map_expand, MvPolynomial.map_rename, map_wittPolynomial