awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
e_a :
  x.shift n =
    (Function.comp (β := 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k)
          (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k))^[n]
      (x.shift n)
e_a₁ :
  Function.Commute (α := 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k) (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)
⊢ x.shift n =
    (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n))

Tactic:
rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]

Premises used: Function.Commute.comp_iterate, Function.comp_apply
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
e_a :
  x.shift n =
    (⇑(RingEquiv.trans (RingEquiv.symm (frobeniusEquiv p k)) (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)
⊢ x.shift n =
    (Function.comp (β := 𝕎 k) (⇑frobenius : (a : 𝕎 k) → 𝕎 k)
          (⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k))^[n]
      (x.shift n)

Tactic:
rw [← WittVector.frobeniusEquiv_apply, ← RingEquiv.coe_trans]

Premises used: WittVector.frobeniusEquiv_apply, RingEquiv.coe_trans
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x.shift n =
    (⇑(RingEquiv.trans (RingEquiv.symm (frobeniusEquiv p k)) (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ ∀ (x : 𝕎 k),
    Eq (α := 𝕎 k)
      ((frobeniusEquiv p k : (a : 𝕎 k) → 𝕎 k) ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k) : 𝕎 k)
      ((RingEquiv.symm (frobeniusEquiv p k) : (a : 𝕎 k) → 𝕎 k) ((frobeniusEquiv p k : (a : 𝕎 k) → 𝕎 k) x : 𝕎 k) : 𝕎 k)

Tactic:
simp only [RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply, implies_true]

Premises used: RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply, implies_true
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
_ : x = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)
_₁ :
  (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n) =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n]
      ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)))
⊢ x =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n]
      ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv p k)) : (a : 𝕎 k) → 𝕎 k)^[n] (x.shift n)))

Tactic:
calc
    _ = verschiebung^[n] (x.shift n) := by
      simpa using eq_iterate_verschiebung (x := x) (n := n) h
    _ = _ := by
      congr
      rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]
      · rw [← WittVector.frobeniusEquiv_apply, ← RingEquiv.coe_trans]
        simp
      · rw [Function.Commute, Function.Semiconj, ← WittVector.frobeniusEquiv_apply]
        simp only [RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply, implies_true]

Premises used: Nat.iterate, WittVector.shift, DFunLike.coe, WittVector.verschiebung
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
h :
  ∀ (x : 𝕎 k),
    Membership.mem (γ := Ideal (𝕎 k)) (RingHom.ker (F := 𝕎 k →+* k) constantCoeff) x ↔
      Membership.mem (γ := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) x
⊢ Eq (α := Ideal (𝕎 k)) (RingHom.ker (F := 𝕎 k →+* k) constantCoeff) (Ideal.span {(↑p : 𝕎 k)})

Tactic:
ext
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
⊢ Membership.mem (γ := Ideal (𝕎 k)) (RingHom.ker (F := 𝕎 k →+* k) constantCoeff) x ↔
    Membership.mem (γ := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) x

Tactic:
simp [mem_span_p_iff_coeff_zero_eq_zero]

Premises used: WittVector.mem_span_p_iff_coeff_zero_eq_zero
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
⊢ Eq (α := k)
    ((quotientPEquiv : (a : 𝕎 k ⧸ Ideal.span {(↑p : 𝕎 k)}) → k)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {(↑p : 𝕎 k)})) : 𝕎 k → 𝕎 k → Prop) x) :
      k)
    ((constantCoeff : (a : 𝕎 k) → k) x : k)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
h :
  ∀ (n : ℕ),
    SModEq (R := 𝕎 k)
      (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) ⊤) x 0
h₁ : ∀ (n : ℕ), x.coeff n = coeff (p := p) 0 n
⊢ x = 0

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
h :
  ∀ (n : ℕ),
    SModEq (R := 𝕎 k)
      (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) ⊤) x 0
n : ℕ
⊢ ∀ (n : ℕ), SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) x 0

Tactic:
simp only [smul_eq_mul, Ideal.mul_top] at h

Premises used: smul_eq_mul, Ideal.mul_top
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ (n : ℕ), SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) x 0
⊢ SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) (n + 1)) x 0

Tactic:
have := h (n + 1)
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ (n : ℕ), SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) x 0
this : SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) (n + 1)) x 0
⊢ ∀ m < n + 1, x.coeff m = 0

Tactic:
simp only [Ideal.span_singleton_pow, SModEq.zero,
        mem_span_p_pow_iff_le_coeff_eq_zero] at this

Premises used: SModEq.zero, WittVector.mem_span_p_pow_iff_le_coeff_eq_zero, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ (n : ℕ), SModEq (R := 𝕎 k) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) x 0
this : ∀ m < n + 1, x.coeff m = 0
⊢ x.coeff n = coeff (p := p) 0 n

Tactic:
simpa using this n
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : ℕ → 𝕎 k
h :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := 𝕎 k)
        (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) m) ⊤) (x m)
        (x n)
h₁ :
  ∀ (n : ℕ),
    SModEq (R := 𝕎 k)
      (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) ⊤) (x n)
      (mk p fun (n : ℕ) ↦ (x (n + 1)).coeff n)
⊢ ∃ (L : 𝕎 k),
    ∀ (n : ℕ),
      SModEq (R := 𝕎 k)
        (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) ⊤) (x n) L

Tactic:
use .mk p (fun n ↦ (x (n + 1)).coeff n)
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : ℕ → 𝕎 k
h :
  ∀ {m n : ℕ},
    m ≤ n →
      SModEq (R := 𝕎 k)
        (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) m) ⊤) (x m)
        (x n)
n : ℕ
h₁ :
  ∀ (h : ∀ {m n : ℕ}, m ≤ n → ∀ i < m, (x m).coeff i = (x n).coeff i),
    ∀ i < n, (x n).coeff i = coeff (mk p fun (n : ℕ) ↦ (x (n + 1)).coeff n) i
⊢ SModEq (R := 𝕎 k)
    (HSMul.hSMul (β := Submodule (𝕎 k) (𝕎 k)) (HPow.hPow (α := Ideal (𝕎 k)) (Ideal.span {(↑p : 𝕎 k)}) n) ⊤) (x n)
    (mk p fun (n : ℕ) ↦ (x (n + 1)).coeff n)

Tactic:
simp only [Ideal.span_singleton_pow, smul_eq_mul, Ideal.mul_top, SModEq.sub_mem,
      mem_span_p_pow_iff_le_coeff_eq_zero, ← le_coeff_eq_iff_le_sub_coeff_eq_zero] at h ⊢

Premises used: WittVector.mem_span_p_pow_iff_le_coeff_eq_zero, SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, WittVector.le_coeff_eq_iff_le_sub_coeff_eq_zero, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : ℕ → 𝕎 k
n : ℕ
h : ∀ {m n : ℕ}, m ≤ n → ∀ i < m, (x m).coeff i = (x n).coeff i
i : ℕ
hi : i < n
⊢ (x n).coeff i = coeff (mk p fun (n : ℕ) ↦ (x (n + 1)).coeff n) i

Tactic:
(h hi i (Nat.lt_succ_self i)).symm

Premises used: Nat.lt_succ_self, Eq.symm
-- Module: Mathlib.RingTheory.WittVector.Complete
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
inst_2 : PerfectRing k p
x : ℕ → 𝕎 k
n : ℕ
h : ∀ {m n : ℕ}, m ≤ n → ∀ i < m, (x m).coeff i = (x n).coeff i
i : ℕ
hi : i < n
⊢ (x n).coeff i = coeff (mk p fun (n : ℕ) ↦ (x (n + 1)).coeff n) i

Tactic:
exact (h hi i (Nat.lt_succ_self i)).symm

Premises used: Nat.lt_succ_self, Eq.symm
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = y.coeff n
mk' :
  ∀ (coeff : ℕ → R) (h : ∀ (n : ℕ), WittVector.coeff (p := p) { coeff := coeff : 𝕎 R } n = y.coeff n),
    { coeff := coeff } = y
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
y : 𝕎 R
coeff : ℕ → R
h : ∀ (n : ℕ), WittVector.coeff (p := p) { coeff := coeff : 𝕎 R } n = y.coeff n
mk' :
  ∀ (coeff_1 : ℕ → R)
    (h :
      ∀ (n : ℕ),
        WittVector.coeff (p := p) { coeff := coeff : 𝕎 R } n = WittVector.coeff (p := p) { coeff := coeff_1 } n),
    Eq (α := 𝕎 R) { coeff := coeff } { coeff := coeff_1 }
⊢ { coeff := coeff } = y

Tactic:
cases y
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
coeff coeff_1 : ℕ → R
h : ∀ (n : ℕ), coeff n = coeff_1 n
⊢ Eq (α := 𝕎 R) { coeff := coeff } { coeff := coeff_1 }

Tactic:
simp [funext_iff, h]

Premises used: funext_iff
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
n : ℕ
⊢ Function.Surjective (β := R) fun (x : 𝕎 R) ↦ x.coeff n

Tactic:
fun x ↦ ⟨(mk p fun _ ↦ x), rfl⟩

Premises used: WittVector.mk, Exists.intro, Function.Surjective, rfl
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
x : ℕ → R
⊢ (mk p x).coeff = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a :
  Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) (wittZero p n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) 0 :
      MvPolynomial (Fin 0 × ℕ) ℚ)
⊢ wittZero p n = 0

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.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) (wittZero p n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) 0 :
      MvPolynomial (Fin 0 × ℕ) ℚ)

Tactic:
simp only [wittZero, wittStructureRat, bind₁, aeval_zero', constantCoeff_xInTermsOfW, map_zero,
    map_wittStructureInt]

Premises used: map_zero, wittStructureRat, MvPolynomial.bind₁, WittVector.wittZero, MvPolynomial.aeval_zero', constantCoeff_xInTermsOfW, map_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a :
  Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) (wittOne p 0) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) 1 :
      MvPolynomial (Fin 0 × ℕ) ℚ)
⊢ wittOne p 0 = 1

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.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) (wittOne p 0) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) 1 :
      MvPolynomial (Fin 0 × ℕ) ℚ)

Tactic:
simp only [wittOne, wittStructureRat, xInTermsOfW_zero, map_one, bind₁_X_right,
    map_wittStructureInt]

Premises used: WittVector.wittOne, wittStructureRat, xInTermsOfW_zero, map_one, MvPolynomial.bind₁_X_right, map_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
a :
  Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) (wittOne p n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) 0 :
      MvPolynomial (Fin 0 × ℕ) ℚ)
⊢ wittOne p n = 0

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.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
a :
  Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) (wittOne p n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (Fin 0 × ℕ) ℤ) → MvPolynomial (Fin 0 × ℕ) ℚ) 0 :
      MvPolynomial (Fin 0 × ℕ) ℚ)

Tactic:
simp only [wittOne, wittStructureRat, map_zero, map_one, map_wittStructureInt]

Premises used: map_zero, WittVector.wittOne, wittStructureRat, map_one, map_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    (0 : MvPolynomial (Fin 0 × ℕ) ℚ)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : 0 < n
a :
  ∀ (n : ℕ)
    (IH :
      ∀ m < n,
        ∀ (hn : 0 < m),
          Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
            ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
              MvPolynomial (Fin 0 × ℕ) ℚ)
            (0 : MvPolynomial (Fin 0 × ℕ) ℚ))
    (hn : 0 < n),
    Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
      ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ n) :
        MvPolynomial (Fin 0 × ℕ) ℚ)
      (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    (0 : MvPolynomial (Fin 0 × ℕ) ℚ)

Tactic:
induction n using Nat.strong_induction_on with | h n IH => ?_
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
a :
  Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
        (HMul.hMul (β := 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)))))
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
              (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
            MvPolynomial ℕ ℚ)) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ n) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    (0 : MvPolynomial (Fin 0 × ℕ) ℚ)

Tactic:
rw [xInTermsOfW_eq]

Premises used: xInTermsOfW_eq
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
a :
  HSub.hSub (α := MvPolynomial (Fin 0 × ℕ) ℚ) 1
        (∑ x ∈ Finset.range n,
          HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) x *
            HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
              ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ x) :
                MvPolynomial (Fin 0 × ℕ) ℚ)
              (p ^ (n - x))) *
      HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
        n =
    0
⊢ Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
        (HMul.hMul (β := 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)))))
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
              (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
            MvPolynomial ℕ ℚ)) :
      MvPolynomial (Fin 0 × ℕ) ℚ)
    (0 : MvPolynomial (Fin 0 × ℕ) ℚ)

Tactic:
simp only [map_mul, map_sub, map_sum, map_pow, bind₁_X_right,
    bind₁_C_right]

Premises used: map_sub, MvPolynomial.bind₁_C_right, map_pow, map_sum, map_mul, MvPolynomial.bind₁_X_right
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    ∀ (hn : 0 < m),
      Eq (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ m) :
          MvPolynomial (Fin 0 × ℕ) ℚ)
        (0 : MvPolynomial (Fin 0 × ℕ) ℚ)
hn : 0 < n
a :
  HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
        n -
      (∑ x ∈ Finset.range n,
          HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) x *
            HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
              ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ x) :
                MvPolynomial (Fin 0 × ℕ) ℚ)
              (p ^ (n - x))) *
        HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
          ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
          n =
    0
⊢ HSub.hSub (α := MvPolynomial (Fin 0 × ℕ) ℚ) 1
        (∑ x ∈ Finset.range n,
          HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ) ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (↑p : ℚ)) x *
            HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
              ((bind₁ fun (k : ℕ) ↦ 1 : (a : MvPolynomial ℕ ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ) (xInTermsOfW p ℚ x) :
                MvPolynomial (Fin 0 × ℕ) ℚ)
              (p ^ (n - x))) *
      HPow.hPow (α := MvPolynomial (Fin 0 × ℕ) ℚ)
        ((C : (a : ℚ) → MvPolynomial (Fin 0 × ℕ) ℚ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _))
        n =
    0

Tactic:
rw [sub_mul, one_mul]

Premises used: sub_mul, one_mul