awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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)
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)
⊢ Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) (i, j)

Tactic:
rw [wittPolynomial_vars, Finset.mem_range] at hj

Premises used: wittPolynomial_vars, Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
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)
⊢ k ∈ Finset.range (n + 1)

Tactic:
replace hk := xInTermsOfW_vars_subset p _ hk
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
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)
hk : k ∈ Finset.range (n + 1)
⊢ (i, j).2 < n + 1

Tactic:
grind
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)

Tactic:
have : Function.Injective (Int.castRingHom ℚ) := Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
rw :
  vars (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n) ⊆
    SProd.sprod (α := Finset idx) Finset.univ (Finset.range (n + 1))
⊢ (wittStructureInt p Φ n).vars ⊆ SProd.sprod (α := Finset idx) Finset.univ (Finset.range (n + 1))

Tactic:
rw [← vars_map_of_injective _ this, map_wittStructureInt]

Premises used: MvPolynomial.vars_map_of_injective, map_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
⊢ vars (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) n) ⊆
    SProd.sprod (α := Finset idx) Finset.univ (Finset.range (n + 1))

Tactic:
apply wittStructureRat_vars

Premises used: wittStructureRat_vars
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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
h₁ : 0 ∉ Finset.range (n + 1) → HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
⊢ (ghostComponent n : (a : 𝕎 R) → R) (teichmullerFun p r) = r ^ p ^ n

Tactic:
rw [ghostComponent_apply, aeval_wittPolynomial, Finset.sum_eq_single 0, pow_zero, one_mul,
    tsub_zero]

Premises used: WittVector.ghostComponent_apply, aeval_wittPolynomial, Finset.sum_eq_single, pow_zero, tsub_zero, OfNat.ofNat, one_mul
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n : ℕ
⊢ (teichmullerFun p r).coeff 0 ^ p ^ n = r ^ p ^ n

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n i : ℕ
h₀ : i ∈ Finset.range (n + 1) → i ≠ 0 → HPow.hPow (α := R) (↑p : R) i * (teichmullerFun p r).coeff i ^ p ^ (n - i) = 0
⊢ i ∈ Finset.range (n + 1) → i ≠ 0 → HPow.hPow (α := R) (↑p : R) i * (teichmullerFun p r).coeff i ^ p ^ (n - i) = 0

Tactic:
_
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n i : ℕ
h : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ HPow.hPow (α := R) (↑p : R) i * (teichmullerFun p r).coeff i ^ p ^ (n - i) = 0

Tactic:
simp [teichmullerFun, h0, hp.1.ne_zero]

Premises used: WittVector.teichmullerFun, Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n : ℕ
h₁ : ¬0 < n + 1 → HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
⊢ 0 ∉ Finset.range (n + 1) → HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
rw [Finset.mem_range]

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n : ℕ
h : ¬0 < n + 1
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
(h (Nat.succ_pos n)).elim

Premises used: False.elim, Nat.succ_pos
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n : ℕ
h : ¬0 < n + 1
⊢ HPow.hPow (α := R) (β := ℕ) (↑p : R) 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
exact (h (Nat.succ_pos n)).elim

Premises used: False.elim, Nat.succ_pos
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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
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)
⊢ 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)

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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)
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)
⊢ 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:
cases n
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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)
    (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:
rfl
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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 + 1) : S)
    (coeff (p := p) (teichmullerFun p ((f : (a : R) → S) r)) (n + 1) : S)

Tactic:
f.map_zero

Premises used: RingHom.map_zero, ite
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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 + 1) : S)
    (coeff (p := p) (teichmullerFun p ((f : (a : R) → S) r)) (n + 1) : S)

Tactic:
exact f.map_zero

Premises used: RingHom.map_zero
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
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 ℚ)
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Tactic:
apply (ghostMap.bijective_of_invertible p (MvPolynomial R ℚ)).1

Premises used: WittVector.ghostMap.bijective_of_invertible, Rat, And.left, MvPolynomial
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
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 ℚ)
⊢ 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:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
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
⊢ (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:
ext1 n
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
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:
simp only [Pi.mul_apply, ghostMap_apply, ghostComponent_teichmullerFun, mul_pow]

Premises used: Pi.mul_apply, _private.0.WittVector.ghostComponent_teichmullerFun, WittVector.ghostMap_apply, mul_pow
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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

Tactic:
map_injective (MvPolynomial.map (Int.castRingHom ℚ))
    (MvPolynomial.map_injective _ Int.cast_injective) ?_

Premises used: WittVector.map_injective, Rat, MvPolynomial.map_injective, Int.castRingHom, MvPolynomial.map, Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℤ
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 ℚ))
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Tactic:
refine map_injective (MvPolynomial.map (Int.castRingHom ℚ))
    (MvPolynomial.map_injective _ Int.cast_injective) ?_

Premises used: WittVector.map_injective, Rat, MvPolynomial.map_injective, Int.castRingHom, MvPolynomial.map, Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℤ
⊢ 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:
simp only [teichmuller_mul_aux₁, map_teichmullerFun, map_mul]

Premises used: _private.0.WittVector.teichmuller_mul_aux₁, _private.0.WittVector.map_teichmullerFun, map_mul
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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)
h₁ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) (n + 1)) (coeff (p := p) 1 (n + 1))
⊢ Eq.{u_1 + 1} (α := 𝕎 R) (teichmullerFun p 1) 1

Tactic:
ext ⟨⟩
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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) 1
⊢ Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) 0) (coeff (p := p) 1 0)

Tactic:
rw [one_coeff_zero]

Premises used: WittVector.one_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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) 1

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
n : ℕ
h : Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) (n + 1)) 0
⊢ Eq.{u_1 + 1} (α := R) (coeff (teichmullerFun p 1) (n + 1)) (coeff (p := p) 1 (n + 1))

Tactic:
rw [one_coeff_eq_of_pos _ _ _ (Nat.succ_pos _)]

Premises used: WittVector.one_coeff_eq_of_pos, Nat.succ_pos
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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)) 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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
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)
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Tactic:
rcases counit_surjective R x with ⟨x, rfl⟩

Premises used: MvPolynomial.counit_surjective, rfl
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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 ℤ
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)
⊢ 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 y with ⟨y, rfl⟩

Premises used: MvPolynomial.counit_surjective, rfl
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CommRing S
x 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:
simp only [← map_teichmullerFun, ← map_mul, teichmuller_mul_aux₂]

Premises used: _private.0.WittVector.teichmuller_mul_aux₂, _private.0.WittVector.map_teichmullerFun, map_mul
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
⊢ coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) r) 0 = r

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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)
h₁ :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) (n + 1)) (coeff (p := p) 0 (n + 1))
⊢ Eq.{u_1 + 1} (α := 𝕎 R) ((teichmuller p : (a : R) → 𝕎 R) 0 : 𝕎 R) (0 : 𝕎 R)

Tactic:
ext ⟨⟩
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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) 0
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) 0) (coeff (p := p) 0 0)

Tactic:
rw [zero_coeff]

Premises used: WittVector.zero_coeff
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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) 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
n : ℕ
h : Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) (n + 1)) 0
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) ((teichmuller p : (a : R) → 𝕎 R) 0) (n + 1)) (coeff (p := p) 0 (n + 1))

Tactic:
rw [zero_coeff]

Premises used: WittVector.zero_coeff
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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)) 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
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 (α := 𝕎 S) (((map f : RingHom.{u_1, u_2} (𝕎 R) (𝕎 S)) : (a : 𝕎 R) → 𝕎 S) ((teichmuller p : (a : R) → 𝕎 R) r) : 𝕎 S)
    ((teichmuller p : (a : S) → 𝕎 S) ((f : (a : R) → S) r : S) : 𝕎 S)

Tactic:
map_teichmullerFun _ _ _

Premises used: _private.0.WittVector.map_teichmullerFun, WittVector.teichmullerFun
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
r : R
n : ℕ
⊢ (ghostComponent n : (a : 𝕎 R) → R) ((teichmuller p : (a : R) → 𝕎 R) r : 𝕎 R) = r ^ p ^ n

Tactic:
ghostComponent_teichmullerFun _ _ _

Premises used: _private.0.WittVector.ghostComponent_teichmullerFun, WittVector.teichmullerFun
-- Module: Mathlib.RingTheory.WittVector.Teichmuller
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := 𝕎 R) (β := R) (⇑constantCoeff : (a : 𝕎 R) → R)

Tactic:
fun r ↦ ⟨teichmuller p r, rfl⟩

Premises used: Exists.intro, DFunLike.coe, Function.Surjective, WittVector.teichmuller, rfl
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
α : Type u_2
x : α → 𝕎 R
h : ∀ (n : ℕ), Subsingleton.{u_2 + 1} (↑{r : α | Membership.mem (γ := Finset α) ∅ r ∧ (x r).coeff n ≠ 0} : Type u_2)
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (∑ s ∈ ∅, x s) n) (∑ s ∈ ∅, (x s).coeff n)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
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)

Tactic:
fun n ↦ ⟨fun b c ↦ ?_⟩

Premises used: Subsingleton.intro