awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
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₁ 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 × ℕ) ℚ)
have 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 × ℕ) ℤ)
Tactic: specialize h n
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
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.{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 × ℕ) ℚ)
have 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 × ℕ) ℚ)
Tactic: apply_fun map (Int.castRingHom ℚ) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
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)
    ((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)
have 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)
Tactic: convert! congr_arg (map (Int.castRingHom R)) (wittStructureInt_prop p Φ n) using 1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
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)
⊢ 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)
have 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)
Tactic: convert! congr_arg (map (Int.castRingHom R)) (wittStructureInt_prop p Φ n) using 1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
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)
    ((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)
have 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)
Tactic: rw [hom_bind₁]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
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)
    ((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)
have 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)
Tactic: rw [hom_bind₁]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
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)
    ((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)
have 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)
Tactic: apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
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)
    ((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)
have 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))
Tactic: apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ Eq.{u_3 + 1} (α := MvPolynomial (σ × ℕ) ℤ)
    (wittStructureInt p
      (((rename f : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial idx ℤ) (MvPolynomial σ ℤ)) :
          (a : MvPolynomial idx ℤ) → MvPolynomial σ ℤ)
        Φ)
      n)
    (((rename (Prod.map f id) : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial (idx × ℕ) ℤ) (MvPolynomial (σ × ℕ) ℤ)) :
        (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℤ)
      (wittStructureInt p Φ n))
have a : Eq.{u_3 + 1} (α := MvPolynomial (σ × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (σ × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℚ)
      (wittStructureInt p
        (((rename f : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial idx ℤ) (MvPolynomial σ ℤ)) :
            (a : MvPolynomial idx ℤ) → MvPolynomial σ ℤ)
          Φ)
        n) :
    MvPolynomial (σ × ℕ) ℚ)
  ((map (Int.castRingHom ℚ) : (a : MvPolynomial (σ × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℚ)
      (((rename (Prod.map f id) : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial (idx × ℕ) ℤ) (MvPolynomial (σ × ℕ) ℤ)) :
            (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℤ)
          (wittStructureInt p Φ n) :
        MvPolynomial (σ × ℕ) ℤ) :
    MvPolynomial (σ × ℕ) ℚ)
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)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ Eq.{u_3 + 1} (α := MvPolynomial (σ × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (σ × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℚ)
        (wittStructureInt p
          (((rename f : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial idx ℤ) (MvPolynomial σ ℤ)) :
              (a : MvPolynomial idx ℤ) → MvPolynomial σ ℤ)
            Φ)
          n) :
      MvPolynomial (σ × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (σ × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℚ)
        (((rename (Prod.map f id) : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial (idx × ℕ) ℤ) (MvPolynomial (σ × ℕ) ℤ)) :
              (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℤ)
            (wittStructureInt p Φ n) :
          MvPolynomial (σ × ℕ) ℤ) :
      MvPolynomial (σ × ℕ) ℚ)
have a : Eq.{u_3 + 1} (α := MvPolynomial (σ × ℕ) ℚ)
  ((bind₁ fun (k : ℕ) ↦
          ((bind₁
                  ((fun (i : σ) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ) (W_ ℚ k)) ∘
                    f) :
                AlgHom.{0, u_2, u_3} ℚ (MvPolynomial idx ℚ) (MvPolynomial (σ × ℕ) ℚ)) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (σ × ℕ) ℚ)
            ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ)
      (xInTermsOfW p ℚ n) :
    MvPolynomial (σ × ℕ) ℚ)
  ((bind₁ fun (i : ℕ) ↦
          (bind₁ fun (i_1 : idx) ↦
                (rename (Prod.map f id ∘ Prod.mk i_1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ) (W_ ℚ i) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (σ × ℕ) ℚ)
            ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) :
        (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ)
      (xInTermsOfW p ℚ n) :
    MvPolynomial (σ × ℕ) ℚ)
Tactic: simp only [map_rename, map_wittStructureInt, wittStructureRat, rename_bind₁, rename_rename,
    bind₁_rename]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ 0) : ℤ)
    ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ)
have inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
Tactic: have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ 0) : ℤ)
    ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ)
have a : Eq (α := ℚ)
  ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
      ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ 0) : ℤ) :
    ℚ)
  ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
Tactic: apply inj
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
⊢ Eq (α := ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
        ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ 0) : ℤ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
have a : Eq (α := ℚ)
  ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (wittStructureInt p Φ 0) :
        MvPolynomial (idx × ℕ) ℚ) :
    ℚ)
  ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
Tactic: rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero,
    constantCoeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
a :
  Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
            (wittStructureInt p Φ 0) :
          MvPolynomial (idx × ℕ) ℚ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
⊢ Eq (α := ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
        ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ 0) : ℤ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
have a₁ : Eq (α := ℚ)
  ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ)
      (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) 0) :
    ℚ)
  ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
Tactic: rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero,
    constantCoeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
a :
  Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
            (wittStructureInt p Φ 0) :
          MvPolynomial (idx × ℕ) ℚ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
a₁ :
  Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ)
        (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) 0) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
⊢ Eq (α := ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
        ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ 0) : ℤ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
have a₂ : Eq (α := ℚ)
  ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
    ℚ)
  ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
Tactic: rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero,
    constantCoeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
a :
  Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
            (wittStructureInt p Φ 0) :
          MvPolynomial (idx × ℕ) ℚ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
a₁ :
  Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ)
        (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) 0) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
a₂ :
  Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
⊢ Eq (α := ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
        ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ 0) : ℤ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
have a₃ : Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
  ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
Tactic: rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero,
    constantCoeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n : ℕ
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ n) : ℤ) (0 : ℤ)
have inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
Tactic: have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n : ℕ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ n) : ℤ) (0 : ℤ)
have a : Eq (α := ℚ)
  ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
      ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ n) : ℤ) :
    ℚ)
  ((Int.castRingHom ℚ : (a : ℤ) → ℚ) 0 : ℚ)
Tactic: apply inj