awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
ind :
  n ∉
    vars (R := ℚ)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i))))
⊢ Disjoint (vars (R := ℚ) (X n))
    (vars (R := ℚ)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))

Tactic:
on_goal 2 => rw [vars_X, disjoint_singleton_left]

Premises used: MvPolynomial.vars_X, Finset.disjoint_singleton_left
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
H :
  Membership.mem (γ := Finset ℕ)
    (vars (R := ℚ)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
    i
⊢ Membership.mem (γ := Finset ℕ)
    ((range n).biUnion fun (i : ℕ) ↦
      (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))).vars)
    i

Tactic:
replace H := vars_sum_subset _ _ H
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
H :
  Membership.mem (γ := Finset ℕ)
    ((range n).biUnion fun (i : ℕ) ↦
      (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))).vars)
    i
⊢ ∃ a ∈ range n,
    i ∈
      (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) a) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ a) (p ^ (n - a)))).vars

Tactic:
rw [mem_biUnion] at H

Premises used: Finset.mem_biUnion
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
H :
  ∃ a ∈ range n,
    i ∈
      (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) a) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ a) (p ^ (n - a)))).vars
ind :
  ∀ (j : ℕ) (hj : j ∈ range n)
    (H :
      i ∈
        (HMul.hMul (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars),
    i ∈ range n
⊢ i ∈ range n

Tactic:
rcases H with ⟨j, hj, H⟩
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H :
  i ∈
    (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars
ind : ∀ (H : i ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars), i ∈ range n
ind₁ : HPow.hPow (α := ℚ) (↑p : ℚ) j ≠ 0
⊢ i ∈ range n

Tactic:
rw [vars_C_mul] at H

Premises used: MvPolynomial.vars_C_mul
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H :
  i ∈
    (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars
ind : Ne (α := ℚ) (↑p : ℚ) 0
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) j ≠ 0

Tactic:
apply pow_ne_zero

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H :
  i ∈
    (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
mod_cast hp.1.ne_zero

Premises used: congrArg, cast, Ne, Nat.cast, Nat.Prime.ne_zero, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Fact.out, Eq.trans
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H :
  i ∈
    (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
exact mod_cast hp.1.ne_zero

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars
⊢ j < n

Tactic:
rw [mem_range] at hj

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars
hj₁ : j < n
⊢ i ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars

Tactic:
rw [mem_range] at hj

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars
⊢ i ∈ range (j + 1)

Tactic:
replace H := (ih j hj).2 (vars_pow _ _ H)
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i ∈ range (j + 1)
⊢ i < j + 1

Tactic:
rw [mem_range] at H

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H :
  Membership.mem (γ := Finset ℕ)
    (vars (R := ℚ)
      (∑ i ∈ range n,
        HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
    n
⊢ Membership.mem (γ := Finset ℕ)
    ((range n).biUnion fun (i : ℕ) ↦
      (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))).vars)
    n

Tactic:
replace H := vars_sum_subset _ _ H
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H :
  Membership.mem (γ := Finset ℕ)
    ((range n).biUnion fun (i : ℕ) ↦
      (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))).vars)
    n
⊢ ∃ a ∈ range n,
    n ∈
      (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) a) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ a) (p ^ (n - a)))).vars

Tactic:
rw [mem_biUnion] at H

Premises used: Finset.mem_biUnion
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H :
  ∃ a ∈ range n,
    n ∈
      (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) a) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ a) (p ^ (n - a)))).vars
ind :
  ∀ (j : ℕ) (hj : j ∈ range n)
    (H :
      n ∈
        (HMul.hMul (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars),
    False
⊢ False

Tactic:
rcases H with ⟨j, hj, H⟩
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H :
  n ∈
    (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars
ind : ∀ (H : n ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars), False
ind₁ : HPow.hPow (α := ℚ) (↑p : ℚ) j ≠ 0
⊢ False

Tactic:
rw [vars_C_mul] at H

Premises used: MvPolynomial.vars_C_mul
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H :
  n ∈
    (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars
ind : Ne (α := ℚ) (↑p : ℚ) 0
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) j ≠ 0

Tactic:
apply pow_ne_zero

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H :
  n ∈
    (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
mod_cast hp.1.ne_zero

Premises used: congrArg, cast, Ne, Nat.cast, Nat.Prime.ne_zero, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Fact.out, Eq.trans
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H :
  n ∈
    (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) j) : MvPolynomial ℕ ℚ)
        (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j)))).vars
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
exact mod_cast hp.1.ne_zero

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars
⊢ j < n

Tactic:
rw [mem_range] at hj

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars
hj₁ : j < n
⊢ n ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars

Tactic:
rw [mem_range] at hj

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars
⊢ n ∈ range (j + 1)

Tactic:
replace H := (ih j hj).2 (vars_pow _ _ H)
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ range (j + 1)
⊢ n < j + 1

Tactic:
rw [mem_range] at H

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
ind : i < n
⊢ i ∈ range n

Tactic:
rw [mem_range]

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i < n

Tactic:
lia
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False

Tactic:
lia
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)

Tactic:
(xInTermsOfW_vars_aux p n).2

Premises used: And.right, xInTermsOfW_vars_aux
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
k : ℕ
rw :
  Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
    (∑ x ∈ range (k + 1),
      (bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        (HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (k - x)))))
    (X k)
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (W_ R k) : MvPolynomial ℕ R)
    (X k : MvPolynomial ℕ R)

Tactic:
rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum]

Premises used: map_sum, wittPolynomial_eq_sum_C_mul_X_pow
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
k : ℕ
simp :
  Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
    (∑ x ∈ range (k + 1),
      HPow.hPow (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (↑p : R)) x *
        HPow.hPow (α := MvPolynomial ℕ R)
          ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (X x) : MvPolynomial ℕ R)
          (p ^ (k - x)))
    (X k)
⊢ Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
    (∑ x ∈ range (k + 1),
      (bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
        (HMul.hMul (α := MvPolynomial ℕ R)
          ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
          (HPow.hPow (α := MvPolynomial ℕ R) (X x) (p ^ (k - x)))))
    (X k)

Tactic:
simp only [map_pow, map_mul, algHom_C, algebraMap_eq]

Premises used: map_pow, MvPolynomial.algHom_C, map_mul, MvPolynomial.algebraMap_eq
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
k : ℕ
rw :
  HSub.hSub (α := MvPolynomial ℕ R) (X k)
        (∑ i ∈ range k,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (k - i)))) +
      ∑ x ∈ range k,
        HPow.hPow (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (↑p : R)) x *
          HPow.hPow (α := MvPolynomial ℕ R)
            ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (X x) : MvPolynomial ℕ R)
            (p ^ (k - x)) =
    X k
⊢ Eq.{u_1 + 1} (α := MvPolynomial ℕ R)
    (∑ x ∈ range (k + 1),
      HPow.hPow (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (↑p : R)) x *
        HPow.hPow (α := MvPolynomial ℕ R)
          ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (X x) : MvPolynomial ℕ R)
          (p ^ (k - x)))
    (X k)

Tactic:
rw [sum_range_succ_comm, tsub_self, pow_zero, pow_one, bind₁_X_right, mul_comm, ← C_pow,
    xInTermsOfW_aux]

Premises used: tsub_self, Finset.sum_range_succ_comm, xInTermsOfW_aux, pow_zero, pow_one, mul_comm, MvPolynomial.bind₁_X_right, MvPolynomial.C_pow
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
k : ℕ
⊢ HSub.hSub (α := MvPolynomial ℕ R) (X k)
        (∑ i ∈ range k,
          HMul.hMul (α := MvPolynomial ℕ R)
            ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) i) : MvPolynomial ℕ R)
            (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R i) (p ^ (k - i)))) +
      ∑ x ∈ range k,
        HPow.hPow (α := MvPolynomial ℕ R) ((C : (a : R) → MvPolynomial ℕ R) (↑p : R)) x *
          HPow.hPow (α := MvPolynomial ℕ R)
            ((bind₁ (xInTermsOfW p R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (X x) : MvPolynomial ℕ R)
            (p ^ (k - x)) =
    X k

Tactic:
simp only [C_pow, bind₁_X_right, sub_add_cancel]

Premises used: MvPolynomial.bind₁_X_right, MvPolynomial.C_pow, sub_add_cancel
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
ind :
  ∀ (n : ℕ)
    (H :
      ∀ m < n,
        Eq (α := MvPolynomial ℕ R)
          ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
          (X m : MvPolynomial ℕ R)),
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R)
      (X n : MvPolynomial ℕ R)
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)

Tactic:
induction n using Nat.strongRecOn with | ind n H => ?_
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
rw :
  X n =
    X n *
      HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R)
        ((C : (a : R) → MvPolynomial ℕ R)
            (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
          MvPolynomial ℕ R)
rw₁ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (↑p : R) n *
            HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
rw₂ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HMul.hMul (α := R) (↑p : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) ^ n) :
        MvPolynomial ℕ R)
rw₃ :
  X n =
    HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
      ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) 1 n) : MvPolynomial ℕ R)
rw₄ : X n = HMul.hMul (α := MvPolynomial ℕ R) (X n) ((C : (a : R) → MvPolynomial ℕ R) 1)
rw₅ : X n = HMul.hMul (α := MvPolynomial ℕ R) (X n) 1
rw₆ rw₇ : Eq.{u_1 + 1} (α := MvPolynomial ℕ R) (X n) (X n)
⊢ X n =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)

Tactic:
rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]

Premises used: one_pow, mul_assoc, mul_invOf_self, map_one, MvPolynomial.C_mul, mul_one, mul_pow
-- Module: Mathlib.RingTheory.WittVector.WittPolynomial
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
n : ℕ
H :
  ∀ m < n,
    Eq (α := MvPolynomial ℕ R)
      ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R m) : MvPolynomial ℕ R)
      (X m : MvPolynomial ℕ R)
ind :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (W_ R n)
        (∑ x ∈ range n,
          (bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R)
            (HMul.hMul (α := MvPolynomial ℕ R)
              ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) x) : MvPolynomial ℕ R)
              (HPow.hPow (α := MvPolynomial ℕ R) (xInTermsOfW p R x) (p ^ (n - x))))))
      ((algebraMap R (MvPolynomial ℕ R) : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R) =
    HMul.hMul (β := MvPolynomial ℕ R)
      (HMul.hMul (α := MvPolynomial ℕ R) (β := MvPolynomial ℕ R) (X n)
        ((C : (a : R) → MvPolynomial ℕ R) (HPow.hPow (α := R) (↑p : R) n) : MvPolynomial ℕ R))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) n) :
        MvPolynomial ℕ R)
⊢ Eq (α := MvPolynomial ℕ R)
    ((bind₁ (W_ R) : (a : MvPolynomial ℕ R) → MvPolynomial ℕ R) (xInTermsOfW p R n) : MvPolynomial ℕ R)
    (X n : MvPolynomial ℕ R)

Tactic:
rw [xInTermsOfW_eq, map_mul, map_sub, bind₁_X_right, algHom_C, map_sum,
    show X n = (X n * C ((p : R) ^ n)) * C ((⅟p : R) ^ n) by
      rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]]

Premises used: map_sub, xInTermsOfW_eq, map_sum, MvPolynomial.algHom_C, map_mul, MvPolynomial.bind₁_X_right