awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_2 : image (Prod.mk 1) (vars (wittPolynomial p ℤ n)) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
refine Subset.trans (vars_rename _ _) ?_

Premises used: Finset.Subset.trans, MvPolynomial.vars_rename
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ image (Prod.mk 1) (vars (wittPolynomial p ℤ n)) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
simp [wittPolynomial_vars, image_subset_iff]

Premises used: wittPolynomial_vars, Finset.image_subset_iff
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (R := ℤ) (∑ i ∈ range n, HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
Subset.trans (vars_sum_subset _ _) ?_

Premises used: Finset.Subset.trans, MvPolynomial.vars_sum_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine :
  ((range n).biUnion fun (i : ℕ) ↦ (HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i)).vars) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range n)
⊢ vars (R := ℤ) (∑ i ∈ range n, HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
refine Subset.trans (vars_sum_subset _ _) ?_

Premises used: Finset.Subset.trans, MvPolynomial.vars_sum_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  ∀ x ∈ range n,
    (HPow.hPow (α := 𝕄) (↑p : 𝕄) x * wittMul p x ^ p ^ (n - x)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
⊢ ((range n).biUnion fun (i : ℕ) ↦ (HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i)).vars) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
rw [biUnion_subset]

Premises used: Finset.biUnion_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
apply :
  (HPow.hPow (α := 𝕄) (↑p : 𝕄) x).vars ∪ (wittMul p x ^ p ^ (n - x)).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range n)
⊢ (HPow.hPow (α := 𝕄) (↑p : 𝕄) x * wittMul p x ^ p ^ (n - x)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
apply Subset.trans (vars_mul _ _)

Premises used: Finset.Subset.trans, MvPolynomial.vars_mul
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (HPow.hPow (α := 𝕄) (↑p : 𝕄) x).vars ∪ (wittMul p x ^ p ^ (n - x)).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
union_subset ?_ ?_

Premises used: Finset.union_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
refine_1 : (HPow.hPow (α := 𝕄) (↑p : 𝕄) x).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
refine_2 : (wittMul p x ^ p ^ (n - x)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
⊢ (HPow.hPow (α := 𝕄) (↑p : 𝕄) x).vars ∪ (wittMul p x ^ p ^ (n - x)).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
refine union_subset ?_ ?_

Premises used: Finset.union_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
refine_1 : vars (R := ℤ) (↑p : 𝕄) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
⊢ (HPow.hPow (α := 𝕄) (↑p : 𝕄) x).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
apply Subset.trans (vars_pow _ _)

Premises used: Finset.Subset.trans, MvPolynomial.vars_pow
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ Eq (α := 𝕄) (↑p : 𝕄) ((C : (a : ℤ) → 𝕄) (↑p : ℤ))

Tactic:
simp only [Int.cast_natCast, eq_intCast]

Premises used: Int.cast_natCast, eq_intCast
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ Eq (α := 𝕄) (↑p : 𝕄) ((C : (a : ℤ) → 𝕄) (↑p : ℤ))

Tactic:
have : (p : 𝕄) = C (p : ℤ) := by simp only [Int.cast_natCast, eq_intCast]
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
this : Eq (α := 𝕄) (↑p : 𝕄) ((C : (a : ℤ) → 𝕄) (↑p : ℤ))
refine_1 : ∅ ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
⊢ vars (R := ℤ) (↑p : 𝕄) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
rw [this, vars_C]

Premises used: MvPolynomial.vars_C
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
this : Eq (α := 𝕄) (↑p : 𝕄) ((C : (a : ℤ) → 𝕄) (↑p : ℤ))
⊢ ∅ ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
apply empty_subset

Premises used: Finset.empty_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
refine_2 : (wittMul p x).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
⊢ (wittMul p x ^ p ^ (n - x)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
apply Subset.trans (vars_pow _ _)

Premises used: Finset.Subset.trans, MvPolynomial.vars_pow
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
refine_2 : SProd.sprod (α := Finset (Fin 2)) univ (range (x + 1)) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
⊢ (wittMul p x).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
apply Subset.trans (wittMul_vars _ _)

Premises used: Finset.Subset.trans, WittVector.wittMul_vars
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
refine_2 : range (x + 1) ⊆ range n
⊢ SProd.sprod (α := Finset (Fin 2)) univ (range (x + 1)) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)

Tactic:
apply product_subset_product (Subset.refl _)

Premises used: Finset.Subset.refl, Finset.product_subset_product
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ range (x + 1) ⊆ range n

Tactic:
simpa using hx
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
apply :
  vars (R := ℤ)
        (∑ x ∈ range (n + 1),
          (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ∪
      vars (R := ℤ)
        (∑ x ∈ range (n + 1),
          (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ (HMul.hMul (α := 𝕄)
        (∑ x ∈ range (n + 1),
          (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
        (∑ x ∈ range (n + 1),
          (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x)))).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
apply Subset.trans (vars_mul _ _)

Premises used: Finset.Subset.trans, MvPolynomial.vars_mul
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (R := ℤ)
        (∑ x ∈ range (n + 1),
          (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ∪
      vars (R := ℤ)
        (∑ x ∈ range (n + 1),
          (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
union_subset ?_ ?_

Premises used: Finset.union_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 :
  vars (R := ℤ)
      (∑ x ∈ range (n + 1),
        (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
refine_2 :
  vars (R := ℤ)
      (∑ x ∈ range (n + 1),
        (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ vars (R := ℤ)
        (∑ x ∈ range (n + 1),
          (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ∪
      vars (R := ℤ)
        (∑ x ∈ range (n + 1),
          (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
            ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
              (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
refine union_subset ?_ ?_

Premises used: Finset.union_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (R := ℤ)
      (∑ x ∈ range (n + 1),
        (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
Subset.trans (vars_sum_subset _ _) ?_

Premises used: Finset.Subset.trans, MvPolynomial.vars_sum_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 :
  ((range (n + 1)).biUnion fun (i : ℕ) ↦
      vars (R := ℤ)
        ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single i (p ^ (n + 1 - i))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) i)))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ vars (R := ℤ)
      (∑ x ∈ range (n + 1),
        (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
refine Subset.trans (vars_sum_subset _ _) ?_

Premises used: Finset.Subset.trans, MvPolynomial.vars_sum_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 :
  ∀ x ∈ range (n + 1),
    vars (R := ℤ)
        ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
      SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ ((range (n + 1)).biUnion fun (i : ℕ) ↦
      vars (R := ℤ)
        ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single i (p ^ (n + 1 - i))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) i)))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
rw [biUnion_subset]

Premises used: Finset.biUnion_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
refine_1 :
  Finsupp.support (Finsupp.single (0, x) (p ^ (n + 1 - x))) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
refine_1₁ : HPow.hPow (α := ℤ) (↑p : ℤ) x ≠ 0
⊢ vars (R := ℤ)
      ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
          (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
rw [rename_monomial, vars_monomial, Finsupp.mapDomain_single]

Premises used: MvPolynomial.vars_monomial, Finsupp.mapDomain_single, MvPolynomial.rename_monomial
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
refine_1 : {(0, x)} ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ Finsupp.support (Finsupp.single (0, x) (p ^ (n + 1 - x))) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
apply Subset.trans Finsupp.support_single_subset

Premises used: Finset.Subset.trans, Finsupp.support_single_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ {(0, x)} ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
simpa using mem_range.mp hx

Premises used: Finset.mem_range, Iff.mp
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
refine_1 : Ne (α := ℤ) (↑p : ℤ) 0
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) x ≠ 0

Tactic:
apply pow_ne_zero

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ Ne (α := ℤ) (↑p : ℤ) 0

Tactic:
mod_cast hp.out.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.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ Ne (α := ℤ) (↑p : ℤ) 0

Tactic:
exact mod_cast hp.out.ne_zero

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (R := ℤ)
      (∑ x ∈ range (n + 1),
        (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
Subset.trans (vars_sum_subset _ _) ?_

Premises used: Finset.Subset.trans, MvPolynomial.vars_sum_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_2 :
  ((range (n + 1)).biUnion fun (i : ℕ) ↦
      vars (R := ℤ)
        ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single i (p ^ (n + 1 - i))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) i)))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ vars (R := ℤ)
      (∑ x ∈ range (n + 1),
        (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
refine Subset.trans (vars_sum_subset _ _) ?_

Premises used: Finset.Subset.trans, MvPolynomial.vars_sum_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_2 :
  ∀ x ∈ range (n + 1),
    vars (R := ℤ)
        ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
      SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ ((range (n + 1)).biUnion fun (i : ℕ) ↦
      vars (R := ℤ)
        ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single i (p ^ (n + 1 - i))) : (a : ℤ) → MvPolynomial ℕ ℤ)
            (HPow.hPow (α := ℤ) (↑p : ℤ) i)))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
rw [biUnion_subset]

Premises used: Finset.biUnion_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
refine_2 :
  Finsupp.support (Finsupp.single (1, x) (p ^ (n + 1 - x))) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
refine_2₁ : HPow.hPow (α := ℤ) (↑p : ℤ) x ≠ 0
⊢ vars (R := ℤ)
      ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n + 1 - x))) : (a : ℤ) → MvPolynomial ℕ ℤ)
          (HPow.hPow (α := ℤ) (↑p : ℤ) x))) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
rw [rename_monomial, vars_monomial, Finsupp.mapDomain_single]

Premises used: MvPolynomial.vars_monomial, Finsupp.mapDomain_single, MvPolynomial.rename_monomial
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
refine_2 : {(1, x)} ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ Finsupp.support (Finsupp.single (1, x) (p ^ (n + 1 - x))) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
apply Subset.trans Finsupp.support_single_subset

Premises used: Finset.Subset.trans, Finsupp.support_single_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ {(1, x)} ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
simpa using mem_range.mp hx

Premises used: Finset.mem_range, Iff.mp
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
refine_2 : Ne (α := ℤ) (↑p : ℤ) 0
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) x ≠ 0

Tactic:
apply pow_ne_zero

Premises used: pow_ne_zero
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := 𝕄)
    ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        (wittPolynomial p ℤ n) :
      𝕄)
    ((bind₁ fun (i : Fin 2) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) :
          (a : MvPolynomial (Fin 2) ℤ) → 𝕄)
        (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) :
      𝕄)

Tactic:
wittStructureInt_prop p (X (0 : Fin 2) * X 1) n

Premises used: HMul.hMul, MvPolynomial.X, wittStructureInt_prop, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h :
  Eq (α := 𝕄) (∑ i ∈ range (n + 1), HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i) : 𝕄)
    ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        (wittPolynomial p ℤ n) :
      𝕄)
h₁ :
  HMul.hMul (α := 𝕄) (β := 𝕄) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)
      ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄) =
    (bind₁ fun (i : Fin 2) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) :
        (a : MvPolynomial (Fin 2) ℤ) → 𝕄)
      (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))
⊢ ∑ i ∈ range (n + 1), HPow.hPow (α := 𝕄) (↑p : 𝕄) i * wittMul p i ^ p ^ (n - i) =
    HMul.hMul (α := 𝕄) (β := 𝕄) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)
      ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)

Tactic:
convert! wittStructureInt_prop p (X (0 : Fin 2) * X 1) n using 1

Premises used: HMul.hMul, MvPolynomial.X, wittStructureInt_prop, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h :
  Eq (α := 𝕄)
    (∑ x ∈ range (n + 1),
      HPow.hPow (α := 𝕄) (↑p : 𝕄) x *
        wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) x ^ p ^ (n - x))
    (∑ x ∈ range (n + 1),
      (bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)))
⊢ Eq (α := 𝕄)
    (∑ x ∈ range (n + 1),
      HPow.hPow (α := 𝕄) (↑p : 𝕄) x *
        wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) x ^ p ^ (n - x))
    ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      (∑ i ∈ range (n + 1),
        (monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i)))

Tactic:
rw [map_sum]

Premises used: map_sum
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h :
  ∀ (i : ℕ) (m : Fin 2 × ℕ →₀ ℕ),
    MvPolynomial.coeff m
        (HPow.hPow (α := 𝕄) (↑p : 𝕄) i *
          wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) i ^ p ^ (n - i)) =
      MvPolynomial.coeff m
        ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
          ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i)))
⊢ Eq (α := 𝕄)
    (∑ x ∈ range (n + 1),
      HPow.hPow (α := 𝕄) (↑p : 𝕄) x *
        wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) x ^ p ^ (n - x))
    (∑ x ∈ range (n + 1),
      (bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single x (p ^ (n - x))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) x)))

Tactic:
congr 1 with i
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
h :
  HPow.hPow (α := 𝕄) (↑p : 𝕄) i *
      wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
      ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i))
⊢ MvPolynomial.coeff m
      (HPow.hPow (α := 𝕄) (↑p : 𝕄) i *
        wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1)) i ^ p ^ (n - i)) =
    MvPolynomial.coeff m
      ((bind₁ (wittStructureInt p (HMul.hMul (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) : (a : MvPolynomial ℕ ℤ) → 𝕄)
        ((monomial (Finsupp.single i (p ^ (n - i))) : (a : ℤ) → MvPolynomial ℕ ℤ) (HPow.hPow (α := ℤ) (↑p : ℤ) i)))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
rw :
  Ne (α := ℕ) ((Finsupp.single i (p ^ (n - i)) : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ∧
    Eq (α := ℕ →₀ ℕ) (Finsupp.single i (p ^ (n - i)))
      (Finsupp.single i ((Finsupp.single i (p ^ (n - i)) : (a : ℕ) → ℕ) i))
⊢ Finsupp.support (Finsupp.single i (p ^ (n - i))) = {i}

Tactic:
rw [Finsupp.support_eq_singleton]

Premises used: Finsupp.support_eq_singleton
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
simp : ¬p ^ (n - i) = 0
⊢ Ne (α := ℕ) ((Finsupp.single i (p ^ (n - i)) : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ∧
    Eq (α := ℕ →₀ ℕ) (Finsupp.single i (p ^ (n - i)))
      (Finsupp.single i ((Finsupp.single i (p ^ (n - i)) : (a : ℕ) → ℕ) i))

Tactic:
simp only [and_true, Finsupp.single_eq_same, Ne]

Premises used: Finsupp.single_eq_same, and_true, Ne
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
⊢ ¬p ^ (n - i) = 0

Tactic:
pow_ne_zero _ hp.out.ne_zero

Premises used: pow_ne_zero, Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
⊢ ¬p ^ (n - i) = 0

Tactic:
exact pow_ne_zero _ hp.out.ne_zero

Premises used: pow_ne_zero, Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m : Fin 2 × ℕ →₀ ℕ
⊢ Finsupp.support (Finsupp.single i (p ^ (n - i))) = {i}

Tactic:
have hsupp : (Finsupp.single i (p ^ (n - i))).support = {i} := by
      rw [Finsupp.support_eq_singleton]
      simp only [and_true, Finsupp.single_eq_same, Ne]
      exact pow_ne_zero _ hp.out.ne_zero