awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a ≠ 0
hax : (Φ(p, k) : (a : V) → V) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb :
  HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k)) a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ (Φ(p, k) : (a : V) → V) (HSMul.hSMul (β := V) b ((F₀ : (a : StandardOneDimIsocrystal p k m) → V) c : V)) =
    HSMul.hSMul (β := V) b
      ((F₀ : (a : StandardOneDimIsocrystal p k m) → V)
          (HSMul.hSMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
            ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k))) :
        V)
have h : (Φ(p, k) : (a : V) → V) (HSMul.hSMul (β := V) b ((F₀ : (a : K(p, k)) → V) c : V)) =
  HSMul.hSMul (β := V) b
    ((F₀ : (a : K(p, k)) → V)
        (HSMul.hSMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
          ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k))) :
      V)
Tactic: unfold StandardOneDimIsocrystal
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a ≠ 0
hax : (Φ(p, k) : (a : V) → V) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb :
  HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k)) a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ (Φ(p, k) : (a : V) → V) (HSMul.hSMul (β := V) b ((F₀ : (a : K(p, k)) → V) c : V)) =
    HSMul.hSMul (β := V) b
      ((F₀ : (a : K(p, k)) → V)
          (HSMul.hSMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
            ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k))) :
        V)
have h : (Φ(p, k) : (a : V) → V) (b • c • x) =
  b •
    HSMul.hSMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
        ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) •
      x
Tactic: rw [LinearMap.toSpanSingleton_apply K(p, k) V x c, LinearMap.toSpanSingleton_apply K(p, k) V x]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a ≠ 0
hax : (Φ(p, k) : (a : V) → V) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb :
  HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k)) a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ (Φ(p, k) : (a : V) → V) (b • c • x) =
    b •
      HSMul.hSMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
          ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) •
        x
have h : HSMul.hSMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
    (HSMul.hSMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) (a • x)) =
  b •
    HMul.hMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
        ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) •
      x
Tactic: simp only [hax, map_smulₛₗ, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a ≠ 0
hax : (Φ(p, k) : (a : V) → V) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb :
  HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k)) a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ HSMul.hSMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
      (HSMul.hSMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) (a • x)) =
    b •
      HMul.hMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
          ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) •
        x
have h : HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
      (HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) a) •
    x =
  (b *
      HMul.hMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
        ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k))) •
    x
Tactic: simp only [← mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a ≠ 0
hax : (Φ(p, k) : (a : V) → V) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb :
  HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k)) a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
        (HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) a) •
      x =
    (b *
        HMul.hMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
          ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k))) •
      x
have h : HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
    (HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) a) =
  b *
    HMul.hMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
      ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (HMul.hMul (α := 𝕄) (β := 𝕄) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)
        ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have apply : vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ∪
    vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
  SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: apply Subset.trans (vars_mul _ _)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ∪
      vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have refine_1 : vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
  SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: refine union_subset ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 :
  vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ∪
      vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have refine_2 : vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
  SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: refine union_subset ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have refine_1 : image (Prod.mk 0) (vars (wittPolynomial p ℤ n)) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: refine Subset.trans (vars_rename _ _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have refine_2 : image (Prod.mk 1) (vars (wittPolynomial p ℤ n)) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: refine Subset.trans (vars_rename _ _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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)
have 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)
Tactic: refine Subset.trans (vars_sum_subset _ _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
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)
have rw : ∀ x ∈ range n,
  (HPow.hPow (α := 𝕄) (↑p : 𝕄) x * wittMul p x ^ p ^ (n - x)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
Tactic: rw [biUnion_subset]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (HPow.hPow (α := 𝕄) (↑p : 𝕄) x * wittMul p x ^ p ^ (n - x)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
have apply : (HPow.hPow (α := 𝕄) (↑p : 𝕄) x).vars ∪ (wittMul p x ^ p ^ (n - x)).vars ⊆
  SProd.sprod (α := Finset (Fin 2)) univ (range n)
Tactic: apply Subset.trans (vars_mul _ _)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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)
have refine_1 : (HPow.hPow (α := 𝕄) (↑p : 𝕄) x).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
Tactic: refine union_subset ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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)
⊢ (HPow.hPow (α := 𝕄) (↑p : 𝕄) x).vars ∪ (wittMul p x ^ p ^ (n - x)).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range n)
have refine_2 : (wittMul p x ^ p ^ (n - x)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
Tactic: refine union_subset ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (HPow.hPow (α := 𝕄) (↑p : 𝕄) x).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
have refine_1 : vars (R := ℤ) (↑p : 𝕄) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
Tactic: apply Subset.trans (vars_pow _ _)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ vars (R := ℤ) (↑p : 𝕄) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
have this : Eq (α := 𝕄) (↑p : 𝕄) ((C : (a : ℤ) → 𝕄) (↑p : ℤ))
Tactic: have : (p : 𝕄) = C (p : ℤ) := by simp only [Int.cast_natCast, eq_intCast]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
this : Eq (α := 𝕄) (↑p : 𝕄) ((C : (a : ℤ) → 𝕄) (↑p : ℤ))
⊢ vars (R := ℤ) (↑p : 𝕄) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
have refine_1 : ∅ ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
Tactic: rw [this, vars_C]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (wittMul p x ^ p ^ (n - x)).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
have refine_2 : (wittMul p x).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
Tactic: apply Subset.trans (vars_pow _ _)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (wittMul p x).vars ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
have refine_2 : SProd.sprod (α := Finset (Fin 2)) univ (range (x + 1)) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
Tactic: apply Subset.trans (wittMul_vars _ _)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ SProd.sprod (α := Finset (Fin 2)) univ (range (x + 1)) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range n)
have refine_2 : range (x + 1) ⊆ range n
Tactic: apply product_subset_product (Subset.refl _)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (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))
have 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))
Tactic: apply Subset.trans (vars_mul _ _)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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))
have 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))
Tactic: refine union_subset ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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))
⊢ 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))
have 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))
Tactic: refine union_subset ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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))
have 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))
Tactic: refine Subset.trans (vars_sum_subset _ _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((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))
have 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))
Tactic: rw [biUnion_subset]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : 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))
have refine_1 : Finsupp.support (Finsupp.single (0, x) (p ^ (n + 1 - x))) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: rw [rename_monomial, vars_monomial, Finsupp.mapDomain_single]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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))
⊢ 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))
have refine_1₁ : HPow.hPow (α := ℤ) (↑p : ℤ) x ≠ 0
Tactic: rw [rename_monomial, vars_monomial, Finsupp.mapDomain_single]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ Finsupp.support (Finsupp.single (0, x) (p ^ (n + 1 - x))) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
have refine_1 : {(0, x)} ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: apply Subset.trans Finsupp.support_single_subset
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) x ≠ 0
have refine_1 : Ne (α := ℤ) (↑p : ℤ) 0
Tactic: apply pow_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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))
have 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))
Tactic: refine Subset.trans (vars_sum_subset _ _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((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))
have 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))
Tactic: rw [biUnion_subset]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : 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))
have refine_2 : Finsupp.support (Finsupp.single (1, x) (p ^ (n + 1 - x))) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
Tactic: rw [rename_monomial, vars_monomial, Finsupp.mapDomain_single]