awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
rw :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X 0)
        (∑ i ∈ range 0,
          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 ^ (0 - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₁ :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X 0)
        (∑ i ∈ ∅,
          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 ^ (0 - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₂ :
  HMul.hMul (β := MvPolynomial ℕ R) (HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₃ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 * (C : (a : R) → MvPolynomial ℕ R) 1 = X 0
⊢ Eq (α := MvPolynomial ℕ R) (xInTermsOfW p R 0) (X 0)
have rw₄ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 * 1 = X 0
Tactic: rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
rw :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X 0)
        (∑ i ∈ range 0,
          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 ^ (0 - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₁ :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X 0)
        (∑ i ∈ ∅,
          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 ^ (0 - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₂ :
  HMul.hMul (β := MvPolynomial ℕ R) (HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₃ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 * (C : (a : R) → MvPolynomial ℕ R) 1 = X 0
rw₄ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 * 1 = X 0
⊢ Eq (α := MvPolynomial ℕ R) (xInTermsOfW p R 0) (X 0)
have rw₅ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 = X 0
Tactic: rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) (↑p : R)
rw :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X 0)
        (∑ i ∈ range 0,
          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 ^ (0 - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₁ :
  HMul.hMul (β := MvPolynomial ℕ R)
      (HSub.hSub (α := MvPolynomial ℕ R) (X 0)
        (∑ i ∈ ∅,
          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 ^ (0 - i)))))
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₂ :
  HMul.hMul (β := MvPolynomial ℕ R) (HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0)
      ((C : (a : R) → MvPolynomial ℕ R)
          (HPow.hPow (α := R) (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : R) _) 0) :
        MvPolynomial ℕ R) =
    X 0
rw₃ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 * (C : (a : R) → MvPolynomial ℕ R) 1 = X 0
rw₄ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 * 1 = X 0
rw₅ : HSub.hSub (α := MvPolynomial ℕ R) (X 0) 0 = X 0
⊢ Eq (α := MvPolynomial ℕ R) (xInTermsOfW p R 0) (X 0)
have rw₆ : Eq.{u_1 + 1} (α := MvPolynomial ℕ R) (X 0) (X 0)
Tactic: rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
have ind : ∀ (n : ℕ) (ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)),
  n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
Tactic: induction n using Nat.strongRecOn with | ind n ih => ?_
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
have ind : Membership.mem (γ := Finset ℕ)
    ({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)))))
    n ∧
  {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)))) ⊆
    {n} ∪ range n
Tactic: rw [xInTermsOfW_eq, mul_comm, vars_C_mul _ (Invertible.ne_zero _),
    vars_sub_of_disjoint, vars_X, range_add_one, insert_eq]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
ind :
  Membership.mem (γ := Finset ℕ)
      ({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)))))
      n ∧
    {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)))) ⊆
      {n} ∪ range n
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
have ind₁ : 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: rw [xInTermsOfW_eq, mul_comm, vars_C_mul _ (Invertible.ne_zero _),
    vars_sub_of_disjoint, vars_X, range_add_one, insert_eq]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Membership.mem (γ := Finset ℕ)
      ({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)))))
      n ∧
    {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)))) ⊆
      {n} ∪ range n
have 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)))) ⊆
  {n} ∪ range n
Tactic: simp only [true_and, true_or, mem_union, mem_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ Membership.mem (γ := Finset ℕ)
      ({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)))))
      i →
    i ∈ {n} ∪ range n
have ind : Membership.mem (γ := Finset ℕ) {n} i ∨
    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 ℕ) {n} i ∨ i ∈ range n
Tactic: rw [mem_union, mem_union]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ Membership.mem (γ := Finset ℕ) {n} i ∨
      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 ℕ) {n} i ∨ i ∈ range n
have ind : 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 →
  i ∈ range n
Tactic: apply Or.imp id
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Membership.mem (γ := Finset ℕ)
      ({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)))))
      n ∧
    {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)))) ⊆
      {n} ∪ range n
have ind : ∀ ⦃i : ℕ⦄,
  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 →
    i ∈ range n
Tactic: on_goal 1 =>
    simp only [true_and, true_or, mem_union, mem_singleton]
    intro i
    rw [mem_union, mem_union]
    apply Or.imp id
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ 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)))))
have 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))))
Tactic: rw [vars_X, disjoint_singleton_left]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ 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)))))
have 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))))
Tactic: on_goal 2 => rw [vars_X, disjoint_singleton_left]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
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
⊢ i ∈ range n
have 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
Tactic: replace H := vars_sum_subset _ _ H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
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
⊢ i ∈ range n
have 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
Tactic: rw [mem_biUnion] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ i ∈ range n
have 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
Tactic: rcases H with ⟨j, hj, H⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ i ∈ range n
have ind : ∀ (H : i ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars), i ∈ range n
Tactic: rw [vars_C_mul] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ i ∈ range n
have ind₁ : HPow.hPow (α := ℚ) (↑p : ℚ) j ≠ 0
Tactic: rw [vars_C_mul] at H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) j ≠ 0
have ind : Ne (α := ℚ) (↑p : ℚ) 0
Tactic: apply pow_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
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
⊢ i ∈ range n
have hj₁ : j < n
Tactic: rw [mem_range] at hj
Cleared hypotheses: hj, H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
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 n
have H₁ : i ∈ range (j + 1)
Tactic: replace H := (ih j hj).2 (vars_pow _ _ H)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
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 ∈ range n
have H₁ : i < j + 1
Tactic: rw [mem_range] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
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
⊢ False
have 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
Tactic: replace H := vars_sum_subset _ _ H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (hypothesis)
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
⊢ False
have 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
Tactic: rw [mem_biUnion] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ False
have 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
Tactic: rcases H with ⟨j, hj, H⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ False
have ind : ∀ (H : n ∈ (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ j) (p ^ (n - j))).vars), False
Tactic: rw [vars_C_mul] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.WittPolynomial (goal)
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
⊢ False
have ind₁ : HPow.hPow (α := ℚ) (↑p : ℚ) j ≠ 0
Tactic: rw [vars_C_mul] at H