awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n : ℕ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
⊢ Eq (α := ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
        ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ n) : ℤ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) 0 : ℚ)
have a : Eq (α := ℚ)
  ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ)
      ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
    ℚ)
  (0 : ℚ)
Tactic: rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n : ℕ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
⊢ Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      ℚ)
    (0 : ℚ)
have a : Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ) (0 : ℚ)
Tactic: rw [constantCoeff_map, h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n : ℕ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
a : Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ) (0 : ℚ)
⊢ Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      ℚ)
    (0 : ℚ)
have a₁ : Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) 0 : ℚ) (0 : ℚ)
Tactic: rw [constantCoeff_map, h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n : ℕ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
a : Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ) (0 : ℚ)
a₁ : Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) 0 : ℚ) (0 : ℚ)
⊢ Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      ℚ)
    (0 : ℚ)
have a₂ : Eq (α := ℚ) 0 0
Tactic: rw [constantCoeff_map, h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    x
⊢ x ∈ SProd.sprod (α := Finset idx) Finset.univ (Finset.range (n + 1))
have simp : x.2 < n + 1
Tactic: simp only [Finset.mem_product, true_and, Finset.mem_univ, Finset.mem_range]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    x
⊢ x.2 < n + 1
have obtain : ∀ (k : ℕ) (hk : k ∈ vars (xInTermsOfW p ℚ n))
  (hx' :
    Membership.mem (γ := Finset (idx × ℕ))
      (vars (R := ℚ)
        ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ))
      x),
  x.2 < n + 1
Tactic: obtain ⟨k, hk, hx'⟩ := mem_vars_bind₁ _ _ hx
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    x
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ))
    x
⊢ x.2 < n + 1
have obtain : ∀ (i : idx)
  (hx'' :
    Membership.mem (γ := Finset (idx × ℕ))
      (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) x),
  x.2 < n + 1
Tactic: obtain ⟨i, -, hx''⟩ := mem_vars_bind₁ _ _ hx'
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    x
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ))
    x
i : idx
hx'' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) x
⊢ x.2 < n + 1
have obtain : ∀ (j : ℕ) (hj : j ∈ vars (W_ ℚ k))
  (hx :
    Membership.mem (γ := Finset (idx × ℕ))
      (vars (R := ℚ)
        ((bind₁ fun (k : ℕ) ↦
              (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                  (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                Φ :
            (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
          (xInTermsOfW p ℚ n)))
      (i, j))
  (hx' :
    Membership.mem (γ := Finset (idx × ℕ))
      (vars (R := ℚ)
        ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
            (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
          Φ))
      (i, j))
  (hx'' :
    Membership.mem (γ := Finset (idx × ℕ))
      (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) (i, j)),
  (i, j).2 < n + 1
Tactic: obtain ⟨j, hj, rfl⟩ := mem_vars_rename _ _ hx''
Cleared hypotheses: x, hx, hx', hx''
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j ∈ vars (W_ ℚ k)
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    (i, j)
hx' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ))
    (i, j)
hx'' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) (i, j)
⊢ (i, j).2 < n + 1
have hj₁ : j < k + 1
Tactic: rw [wittPolynomial_vars, Finset.mem_range] at hj
Cleared hypotheses: hj, hx, hx', hx''
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j < k + 1
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    (i, j)
hx' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ))
    (i, j)
hx'' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) (i, j)
⊢ (i, j).2 < n + 1
have hk₁ : k ∈ Finset.range (n + 1)
Tactic: replace hk := xInTermsOfW_vars_subset p _ hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (hypothesis)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (wittStructureInt p Φ n).vars ⊆ SProd.sprod (α := Finset idx) Finset.univ (Finset.range (n + 1))
have this : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
Tactic: have : Function.Injective (Int.castRingHom ℚ) := Int.cast_injective
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.StructurePolynomial (goal)
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
⊢ (wittStructureInt p Φ n).vars ⊆ SProd.sprod (α := Finset idx) Finset.univ (Finset.range (n + 1))
have rw : vars (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n) ⊆
  SProd.sprod (α := Finset idx) Finset.univ (Finset.range (n + 1))
Tactic: rw [← vars_map_of_injective _ this, map_wittStructureInt]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n : ℕ
⊢ (ghostComponent n : (a : 𝕎 R) → R) (teichmullerFun p r) = r ^ p ^ n
have rw : (teichmullerFun p r).coeff 0 ^ p ^ n = r ^ p ^ n
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.sum_eq_single 0, pow_zero, one_mul,
    tsub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n : ℕ
rw : (teichmullerFun p r).coeff 0 ^ p ^ n = r ^ p ^ n
⊢ (ghostComponent n : (a : 𝕎 R) → R) (teichmullerFun p r) = r ^ p ^ n
have h₀ : ∀ b ∈ Finset.range (n + 1), b ≠ 0 → HPow.hPow (α := R) (↑p : R) b * (teichmullerFun p r).coeff b ^ p ^ (n - b) = 0
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.sum_eq_single 0, pow_zero, one_mul,
    tsub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n : ℕ
rw : (teichmullerFun p r).coeff 0 ^ p ^ n = r ^ p ^ n
h₀ : ∀ b ∈ Finset.range (n + 1), b ≠ 0 → HPow.hPow (α := R) (↑p : R) b * (teichmullerFun p r).coeff b ^ p ^ (n - b) = 0
⊢ (ghostComponent n : (a : 𝕎 R) → R) (teichmullerFun p r) = r ^ p ^ n
have h₁ : 0 ∉ Finset.range (n + 1) → HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
Tactic: rw [ghostComponent_apply, aeval_wittPolynomial, Finset.sum_eq_single 0, pow_zero, one_mul,
    tsub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
have h₁ : ¬0 < n + 1 → HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
Tactic: rw [Finset.mem_range]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) (teichmullerFun p r) : 𝕎 S)
    (teichmullerFun p ((f : (a : R) → S) r) : 𝕎 S)
have h : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := S)
    (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) (teichmullerFun p r)) n : S)
    (coeff (p := p) (teichmullerFun p ((f : (a : R) → S) r)) n : S)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
n : ℕ
⊢ Eq.{u_2 + 1} (α := S)
    (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) (teichmullerFun p r)) n : S)
    (coeff (p := p) (teichmullerFun p ((f : (a : R) → S) r)) n : S)
have h : Eq.{u_2 + 1} (α := S)
  (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) (teichmullerFun p r)) 0 : S)
  (coeff (p := p) (teichmullerFun p ((f : (a : R) → S) r)) 0 : S)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
n : ℕ
h :
  Eq.{u_2 + 1} (α := S)
    (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) (teichmullerFun p r)) 0 : S)
    (coeff (p := p) (teichmullerFun p ((f : (a : R) → S) r)) 0 : S)
⊢ Eq.{u_2 + 1} (α := S)
    (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) (teichmullerFun p r)) n : S)
    (coeff (p := p) (teichmullerFun p ((f : (a : R) → S) r)) n : S)
have h₁ : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := S)
    (coeff (p := p) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) (teichmullerFun p r)) (n + 1) : S)
    (coeff (p := p) (teichmullerFun p ((f : (a : R) → S) r)) (n + 1) : S)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
have a : Eq (α := ℕ → MvPolynomial R ℚ)
  ((ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p (x * y)) : ℕ → MvPolynomial R ℚ)
  ((ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p x * teichmullerFun p y) :
    ℕ → MvPolynomial R ℚ)
Tactic: apply (ghostMap.bijective_of_invertible p (MvPolynomial R ℚ)).1
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ Eq (α := ℕ → MvPolynomial R ℚ)
    ((ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p (x * y)) : ℕ → MvPolynomial R ℚ)
    ((ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p x * teichmullerFun p y) :
      ℕ → MvPolynomial R ℚ)
have a : (ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p (x * y)) =
  HMul.hMul (α := ℕ → MvPolynomial R ℚ) (β := ℕ → MvPolynomial R ℚ)
    ((ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p x) : ℕ → MvPolynomial R ℚ)
    ((ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p y) : ℕ → MvPolynomial R ℚ)
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ (ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p (x * y)) =
    HMul.hMul (α := ℕ → MvPolynomial R ℚ) (β := ℕ → MvPolynomial R ℚ)
      ((ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p x) : ℕ → MvPolynomial R ℚ)
      ((ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p y) : ℕ → MvPolynomial R ℚ)
have a : ∀ (n : ℕ),
  (ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p (x * y)) n =
    HMul.hMul (α := ℕ → MvPolynomial R ℚ) (β := ℕ → MvPolynomial R ℚ)
      ((ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p x) : ℕ → MvPolynomial R ℚ)
      ((ghostMap : (a : 𝕎 (MvPolynomial R ℚ)) → ℕ → MvPolynomial R ℚ) (teichmullerFun p y) : ℕ → MvPolynomial R ℚ) n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℤ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
have refine : Eq (α := 𝕎 (MvPolynomial R ℚ))
  ((map (MvPolynomial.map (Int.castRingHom ℚ)) : (a : 𝕎 (MvPolynomial R ℤ)) → 𝕎 (MvPolynomial R ℚ))
      (teichmullerFun p (x * y)) :
    𝕎 (MvPolynomial R ℚ))
  ((map (MvPolynomial.map (Int.castRingHom ℚ)) : (a : 𝕎 (MvPolynomial R ℤ)) → 𝕎 (MvPolynomial R ℚ))
      (teichmullerFun p x * teichmullerFun p y) :
    𝕎 (MvPolynomial R ℚ))
Tactic: refine map_injective (MvPolynomial.map (Int.castRingHom ℚ))
    (MvPolynomial.map_injective _ Int.cast_injective) ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (teichmullerFun p 1) 1
have h : Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) 0) (coeff (p := p) 1 0)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
h : Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) 0) (coeff (p := p) 1 0)
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (teichmullerFun p 1) 1
have h₁ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) (n + 1)) (coeff (p := p) 1 (n + 1))
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
⊢ Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) 0) (coeff (p := p) 1 0)
have h : Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) 0) 1
Tactic: rw [one_coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) (n + 1)) (coeff (p := p) 1 (n + 1))
have h : Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) (n + 1)) 0
Tactic: rw [one_coeff_eq_of_pos _ _ _ (Nat.succ_pos _)]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
x y : R
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
have rcases : ∀ (x : MvPolynomial R ℤ),
  teichmullerFun p (HMul.hMul (α := R) ((counit R : (a : MvPolynomial R ℤ) → R) x : R) y) =
    HMul.hMul (α := 𝕎 R) (teichmullerFun p ((counit R : (a : MvPolynomial R ℤ) → R) x) : 𝕎 R) (teichmullerFun p y)
Tactic: rcases counit_surjective R x with ⟨x, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
y : R
x : MvPolynomial R ℤ
⊢ teichmullerFun p (HMul.hMul (α := R) ((counit R : (a : MvPolynomial R ℤ) → R) x : R) y) =
    HMul.hMul (α := 𝕎 R) (teichmullerFun p ((counit R : (a : MvPolynomial R ℤ) → R) x) : 𝕎 R) (teichmullerFun p y)
have rcases : ∀ (y : MvPolynomial R ℤ),
  teichmullerFun p
      (HMul.hMul (α := R) (β := R) ((counit R : (a : MvPolynomial R ℤ) → R) x : R)
        ((counit R : (a : MvPolynomial R ℤ) → R) y : R)) =
    HMul.hMul (α := 𝕎 R) (β := 𝕎 R) (teichmullerFun p ((counit R : (a : MvPolynomial R ℤ) → R) x) : 𝕎 R)
      (teichmullerFun p ((counit R : (a : MvPolynomial R ℤ) → R) y) : 𝕎 R)
Tactic: rcases counit_surjective R y with ⟨y, rfl⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := 𝕎 R) ((teichmuller p : (a : R) → 𝕎 R) 0 : 𝕎 R) (0 : 𝕎 R)
have h : Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) 0) (coeff (p := p) 0 0)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
h : Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) 0) (coeff (p := p) 0 0)
⊢ Eq.{u_1 + 1} (α := 𝕎 R) ((teichmuller p : (a : R) → 𝕎 R) 0 : 𝕎 R) (0 : 𝕎 R)
have h₁ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) (n + 1)) (coeff (p := p) 0 (n + 1))
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) 0) (coeff (p := p) 0 0)
have h : Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) 0) 0
Tactic: rw [zero_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Teichmuller (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) (n + 1)) (coeff (p := p) 0 (n + 1))
have h : Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) (n + 1)) 0
Tactic: rw [zero_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.TeichmullerSeries (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
hind :
  ∀ (h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)) (n : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ S', x s) n) (∑ s ∈ S', (x s).coeff n)
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ insert a S' ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
⊢ ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)
have refine : ∀ (n : ℕ) (b c : (↑{r : α | r ∈ S' ∧ (x r).coeff n ≠ 0} : Type u_2)), b = c
Tactic: refine fun n ↦ ⟨fun b c ↦ ?_⟩