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 ℤ
φ : ℕ → 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 : ℕ
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 × ℕ) ℚ)
⊢ φ k = wittStructureInt p Φ k

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Premises used: Rat, MvPolynomial.map_injective, Int.castRingHom, Int.cast_injective
-- 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 × ℕ) ℤ)
k : ℕ
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 × ℕ) ℚ)
⊢ 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:
rw [map_wittStructureInt]

Premises used: map_wittStructureInt
-- 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 × ℕ) ℤ)
k : ℕ
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 × ℕ) ℚ)
⊢ 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
-- 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 × ℕ) ℤ)
⊢ ∀ (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:
congr_fun ?_

Premises used: congr_fun
-- 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 × ℕ) ℤ)
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 ℚ) Φ))
⊢ ∀ (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:
refine congr_fun ?_

Premises used: congr_fun
-- 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 × ℕ) ℤ)
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 × ℕ) ℚ)
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 × ℕ) ℚ)
⊢ 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:
apply ExistsUnique.unique (wittStructureRat_existsUnique p (map (Int.castRingHom ℚ) Φ))

Premises used: Rat, Int.castRingHom, ExistsUnique.unique, MvPolynomial.map, wittStructureRat_existsUnique, DFunLike.coe
-- 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 : ℕ
⊢ 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:
specialize h n
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  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 (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ φ : (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_fun map (Int.castRingHom ℚ) at h

Premises used: Rat, Int.castRingHom, MvPolynomial.map
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
        ((bind₁ φ : (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 × ℕ) ℚ)
⊢ 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:
simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial,
      AlgHom.coe_toRingHom] using h

Premises used: MvPolynomial.map_bind₁, AlgHom.coe_toRingHom, MvPolynomial.map_rename, MvPolynomial.eval₂Hom_map_hom, map_wittPolynomial, MvPolynomial.eval₂Hom_C_left
-- 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 : ℕ
⊢ 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 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 × ℕ) ℤ,
    ∀ (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:
⟨wittStructureInt p Φ, wittStructureInt_prop _ _, eq_wittStructureInt _ _⟩

Premises used: eq_wittStructureInt, wittStructureInt_prop, wittStructureInt, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
R : Type u_1
idx : Type u_2
inst : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ Eq (α := MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
        ((bind₁ (wittStructureInt p Φ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n)) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
        ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)

Tactic:
congr_arg (map (Int.castRingHom R)) (wittStructureInt_prop p Φ n)

Premises used: wittStructureInt_prop, congr_arg, Int.castRingHom, MvPolynomial.map, DFunLike.coe
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
R : Type u_1
idx : Type u_2
inst : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
h :
  Eq (α := MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((aeval fun (i : ℕ) ↦
            (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
              (wittStructureInt p Φ i) :
          (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) R)
        (W_ ℤ n) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
        ((bind₁ (wittStructureInt p Φ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n)) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
h₁ :
  Eq (α := MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((aeval fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ R) → MvPolynomial (idx × ℕ) R) (W_ R n) :
          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) R)
        Φ :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
        ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
⊢ Eq (α := MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((aeval fun (i : ℕ) ↦
            (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
              (wittStructureInt p Φ i) :
          (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) R)
        (W_ ℤ n) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((aeval fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ R) → MvPolynomial (idx × ℕ) R) (W_ R n) :
          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) R)
        Φ :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)

Tactic:
convert! congr_arg (map (Int.castRingHom R)) (wittStructureInt_prop p Φ n) using 1

Premises used: wittStructureInt_prop, congr_arg, Int.castRingHom, MvPolynomial.map, DFunLike.coe
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
R : Type u_1
idx : Type u_2
inst : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
h :
  Eq (α := MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((aeval fun (i : ℕ) ↦
            (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
              (wittStructureInt p Φ i) :
          (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) R)
        (W_ ℤ n) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((eval₂Hom (RingHom.comp (map (Int.castRingHom R)) C) fun (i : ℕ) ↦
            (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
              (wittStructureInt p Φ i) :
          (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) R)
        (W_ ℤ n) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
⊢ Eq (α := MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((aeval fun (i : ℕ) ↦
            (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
              (wittStructureInt p Φ i) :
          (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) R)
        (W_ ℤ n) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
        ((bind₁ (wittStructureInt p Φ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n)) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)

Tactic:
rw [hom_bind₁]

Premises used: MvPolynomial.hom_bind₁
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
R : Type u_1
idx : Type u_2
inst : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
h :
  Eq (α := MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((aeval fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ R) → MvPolynomial (idx × ℕ) R) (W_ R n) :
          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) R)
        Φ :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((eval₂Hom (RingHom.comp (map (Int.castRingHom R)) C) fun (i : idx) ↦
            (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
              ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n)) :
          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) R)
        Φ :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
⊢ Eq (α := MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((aeval fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ R) → MvPolynomial (idx × ℕ) R) (W_ R n) :
          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) R)
        Φ :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
        ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n) :
            (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) ℤ)
          Φ) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)

Tactic:
rw [hom_bind₁]

Premises used: MvPolynomial.hom_bind₁
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
R : Type u_1
idx : Type u_2
inst : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
apply :
  Eq (α := ℕ → MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    (fun (i : ℕ) ↦
      (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R) (wittStructureInt p Φ i))
    fun (i : ℕ) ↦
    (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R) (wittStructureInt p Φ i)
⊢ Eq (α := MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((aeval fun (i : ℕ) ↦
            (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
              (wittStructureInt p Φ i) :
          (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) R)
        (W_ ℤ n) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((eval₂Hom (RingHom.comp (map (Int.castRingHom R)) C) fun (i : ℕ) ↦
            (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
              (wittStructureInt p Φ i) :
          (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) R)
        (W_ ℤ n) :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)

Tactic:
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_int, rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
R : Type u_1
idx : Type u_2
inst : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
apply :
  Eq (α := idx → MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    (fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ R) → MvPolynomial (idx × ℕ) R) (W_ R n)) fun (i : idx) ↦
    (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
      ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n))
⊢ Eq (α := MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((aeval fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ R) → MvPolynomial (idx × ℕ) R) (W_ R n) :
          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) R)
        Φ :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    ((eval₂Hom (RingHom.comp (map (Int.castRingHom R)) C) fun (i : idx) ↦
            (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
              ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n)) :
          (a : MvPolynomial idx ℤ) → MvPolynomial (idx × ℕ) R)
        Φ :
      MvPolynomial.{u_2, u_1} (idx × ℕ) R)

Tactic:
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_int, rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
R : Type u_1
idx : Type u_2
inst : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ Eq (α := ℕ → MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    (fun (i : ℕ) ↦
      (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R) (wittStructureInt p Φ i))
    fun (i : ℕ) ↦
    (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R) (wittStructureInt p Φ i)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
R : Type u_1
idx : Type u_2
inst : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ Eq (α := idx → MvPolynomial.{u_2, u_1} (idx × ℕ) R)
    (fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ R) → MvPolynomial (idx × ℕ) R) (W_ R n)) fun (i : idx) ↦
    (map (Int.castRingHom R) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) R)
      ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (W_ ℤ n))

Tactic:
simp only [map_rename, map_wittPolynomial]

Premises used: MvPolynomial.map_rename, map_wittPolynomial