awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
inst_2 : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hr0 : HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : q'.coeff 0 ≠ 0
hq :
  Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k))
    (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q')
hq0 : HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q' ≠ 0
hrq :
  Ne (α := FractionRing (𝕎 k))
    (Localization.mk
      (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
            (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq).1
      (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
          Subtype.mk (p := fun (x : 𝕎 k) ↦
            Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
            (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq).2)
    0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ HMul.hMul (α := FractionRing (𝕎 k)) (β := FractionRing (𝕎 k))
      ((IsFractionRing.ringEquivOfRingEquiv (A := 𝕎 k) (B := 𝕎 k) (frobeniusEquiv p k) :
            (a : FractionRing (𝕎 k)) → FractionRing (𝕎 k))
          ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b) :
        FractionRing (𝕎 k))
      (Localization.mk
        (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
            Subtype.mk (p := fun (x : 𝕎 k) ↦
              Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
              (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq).1
        (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) m * r',
            Subtype.mk (p := fun (x : 𝕎 k) ↦
              Membership.mem (γ := Submonoid (𝕎 k)) (nonZeroDivisors (𝕎 k) : Submonoid (𝕎 k)) x)
              (HPow.hPow (α := 𝕎 k) (↑p : 𝕎 k) n * q') hq).2) =
    HMul.hMul (β := FractionRing (𝕎 k))
      (HPow.hPow (α := FractionRing (𝕎 k)) (↑p : FractionRing (𝕎 k)) (HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ)))
      ((algebraMap (𝕎 k) (FractionRing (𝕎 k)) : (a : 𝕎 k) → FractionRing (𝕎 k)) b : FractionRing (𝕎 k))

Tactic:
exact exists_frobenius_solution_fractionRing_aux p m n r' q' hr' hq' hq

Premises used: WittVector.exists_frobenius_solution_fractionRing_aux
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
⊢ IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦
    (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)

Tactic:
have : IsPoly p fun {R} [CommRing R] x ↦ frobenius (verschiebung x) :=
    IsPoly.comp (hg := frobenius_isPoly p) (hf := verschiebung_isPoly)
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
this :
  IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦
    (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)
⊢ IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ x * (↑p : 𝕎 R)

Tactic:
have : IsPoly p fun {R} [CommRing R] x ↦ x * p := mulN_isPoly p p
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
this_1 :
  IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦
    (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ x * (↑p : 𝕎 R)
refine_3 :
  ∀ (R : Type u_1) [R._inst : CommRing R] (x : 𝕎 R) (n : ℕ),
    Eq (α := R)
      ((ghostComponent n : (a : 𝕎 R) → R)
          ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) : 𝕎 R) :
        R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x * (↑p : 𝕎 R)) : R)
⊢ (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) = x * (↑p : 𝕎 R)

Tactic:
ghost_calc x
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
this_1 :
  IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦
    (frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ x * (↑p : 𝕎 R)
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
⊢ ∀ (n : ℕ),
    Eq (α := R)
      ((ghostComponent n : (a : 𝕎 R) → R)
          ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) : 𝕎 R) :
        R)
      ((ghostComponent n : (a : 𝕎 R) → R) (x * (↑p : 𝕎 R)) : R)

Tactic:
ghost_simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
rw :
  Eq (α := 𝕎 (ZMod p)) ((verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
    ((frobenius : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) ((verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p)) :
      𝕎 (ZMod p))
rw₁ rw₂ :
  Eq (α := 𝕎 (ZMod p)) ((verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
    ((verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x : 𝕎 (ZMod p))
⊢ (verschiebung : (a : 𝕎 (ZMod p)) → 𝕎 (ZMod p)) x = x * (↑p : 𝕎 (ZMod p))

Tactic:
rw [← frobenius_verschiebung, frobenius_zmodp]

Premises used: WittVector.frobenius_verschiebung, WittVector.frobenius_zmodp
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
⊢ (HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff 0 = 1

Tactic:
simp only [one_coeff_zero, pow_zero]

Premises used: pow_zero, WittVector.one_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
h : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1
succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i * (↑p : 𝕎 R)).coeff (i + 1) = 1
succ₁ :
  Eq.{u_1 + 1} (α := R)
    (coeff (p := p)
      ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) : 𝕎 R))
      (i + 1))
    1
succ₂ :
  HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (i + 1)) p =
    1
succ₃ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i ^ p = 1
succ₄ : HPow.hPow (α := R) 1 p = 1
succ₅ succ₆ : Eq.{u_1 + 1} (α := R) 1 1
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff (i + 1) = 1

Tactic:
rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]

Premises used: one_pow, WittVector.verschiebung_coeff_succ, pow_succ, WittVector.coeff_frobenius_charP, WittVector.frobenius_verschiebung
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
zero : (HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff 0 = 1
succ :
  ∀ (i : ℕ) (h : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1),
    (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff (i + 1) = 1
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff i = 1

Tactic:
induction i with
  | zero => simp only [one_coeff_zero, pow_zero]
  | succ i h =>
    rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP,
      verschiebung_coeff_succ, h, one_pow]

Premises used: one_pow, WittVector.verschiebung_coeff_succ, pow_succ, pow_zero, WittVector.coeff_frobenius_charP, WittVector.one_coeff_zero, WittVector.frobenius_verschiebung
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
j : ℕ
hj : j ≠ 0
zero : 0 < j
⊢ (HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff j = 0

Tactic:
rw [pow_zero, one_coeff_eq_of_pos]

Premises used: pow_zero, WittVector.one_coeff_eq_of_pos
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
j : ℕ
hj : j ≠ 0
⊢ 0 < j

Tactic:
Nat.pos_of_ne_zero hj

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
j : ℕ
hj : j ≠ 0
⊢ 0 < j

Tactic:
exact Nat.pos_of_ne_zero hj

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
j : ℕ
hj : j ≠ i + 1
succ :
  HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) j) p = 0
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff j = 0

Tactic:
rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP]

Premises used: pow_succ, WittVector.coeff_frobenius_charP, WittVector.frobenius_verschiebung
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
j : ℕ
hj : j ≠ i + 1
succ :
  ∀ (hj : 0 ≠ i + 1),
    HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) 0) p = 0
succ₁ :
  ∀ (n : ℕ) (hj : n + 1 ≠ i + 1),
    HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (n + 1))
        p =
      0
⊢ HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) j) p = 0

Tactic:
cases j
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
hj : 0 ≠ i + 1
succ : HPow.hPow (α := R) 0 p = 0
succ₁ succ₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) 0) p = 0

Tactic:
rw [verschiebung_coeff_zero, zero_pow hp.out.ne_zero]

Premises used: WittVector.verschiebung_coeff_zero, Nat.Prime.ne_zero, zero_pow, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0
n : ℕ
hj : n + 1 ≠ i + 1
succ : (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff n ^ p = 0
succ₁ : HPow.hPow (α := R) 0 p = 0
succ₂ succ₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) (n + 1)) p =
    0

Tactic:
rw [verschiebung_coeff_succ, hi (ne_of_apply_ne _ hj), zero_pow hp.out.ne_zero]

Premises used: WittVector.verschiebung_coeff_succ, ne_of_apply_ne, Nat.Prime.ne_zero, zero_pow, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i j : ℕ
hj : j ≠ i
zero : ∀ {j : ℕ} (hj : j ≠ 0), (HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff j = 0
succ :
  ∀ (i : ℕ) (hi : ∀ {j : ℕ} (hj : j ≠ i), (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0) {j : ℕ} (hj : j ≠ i + 1),
    (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (i + 1)).coeff j = 0
⊢ (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i).coeff j = 0

Tactic:
induction i generalizing j with
  | zero =>
    rw [pow_zero, one_coeff_eq_of_pos]
    exact Nat.pos_of_ne_zero hj
  | succ i hi =>
    rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP]
    cases j
    · rw [verschiebung_coeff_zero, zero_pow hp.out.ne_zero]
    · rw [verschiebung_coeff_succ, hi (ne_of_apply_ne _ hj), zero_pow hp.out.ne_zero]

Premises used: WittVector.verschiebung_coeff_succ, pow_succ, WittVector.verschiebung_coeff_zero, pow_zero, WittVector.coeff_frobenius_charP, Nat.pos_of_ne_zero, WittVector.one_coeff_eq_of_pos, Nat.Prime.ne_zero, WittVector.frobenius_verschiebung, zero_pow, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
pos : ∀ (hi : i = 1), Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) i) 1
neg : ∀ (hi : ¬i = 1), Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) i) 0
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) i) (if i = 1 then 1 else 0)

Tactic:
split_ifs with hi
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hi : i = 1
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) i) 1

Tactic:
simpa only [hi, pow_one] using coeff_p_pow p R 1

Premises used: WittVector.coeff_p_pow, pow_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
i : ℕ
hi : ¬i = 1
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) i) 0

Tactic:
simpa only [pow_one] using coeff_p_pow_eq_zero p R hi

Premises used: pow_one, WittVector.coeff_p_pow_eq_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
hnc : ¬Eq (α := ℕ) 0 1
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) 0) 0

Tactic:
rw [coeff_p, if_neg]

Premises used: WittVector.coeff_p, if_neg
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
⊢ ¬Eq (α := ℕ) 0 1

Tactic:
zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
⊢ ¬Eq (α := ℕ) 0 1

Tactic:
exact zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
rw : Eq.{u_1 + 1} (α := R) (if Eq (α := ℕ) 1 1 then 1 else 0) 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) (↑p : 𝕎 R) 1) 1

Tactic:
rw [coeff_p, if_pos rfl]

Premises used: WittVector.coeff_p, if_pos, rfl
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CharP R p
h : Eq.{u_1 + 1} (α := 𝕎 R) (↑p : 𝕎 R) 0
⊢ False

Tactic:
simpa only [h, zero_coeff, zero_ne_one] using coeff_p_one p R

Premises used: zero_ne_one, WittVector.zero_coeff, WittVector.coeff_p_one
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CharP R p
⊢ Ne.{u_1 + 1} (α := FractionRing (𝕎 R)) (↑p : FractionRing (𝕎 R)) 0

Tactic:
simpa using (IsFractionRing.injective (𝕎 R) (FractionRing (𝕎 R))).ne (WittVector.p_nonzero _ _)
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
⊢ IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R))

Tactic:
have : IsPoly₂ p fun {R} [Rcr : CommRing R] x y ↦ verschiebung (x * frobenius y) :=
    IsPoly.comp₂ (hg := verschiebung_isPoly)
      (hf := IsPoly₂.comp (hh := mulIsPoly₂) (hf := idIsPolyI' p) (hg := frobenius_isPoly p))
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
this :
  IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R))
⊢ IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y

Tactic:
have : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y :=
    IsPoly₂.comp (hh := mulIsPoly₂) (hf := verschiebung_isPoly) (hg := idIsPolyI' p)
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
this_1 :
  IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R))
this :
  IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y
refine_3 :
  ∀ (R : Type u_1) [R._inst : CommRing R] (x y : 𝕎 R) (n : ℕ),
    Eq (α := R)
      ((ghostComponent n : (a : 𝕎 R) → R)
          ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) : 𝕎 R) :
        R)
      ((ghostComponent n : (a : 𝕎 R) → R) (HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y) : R)
⊢ (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) =
    HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y

Tactic:
ghost_calc x y
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
this_1 :
  IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R))
this :
  IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ Eq (α := R)
    ((ghostComponent 0 : (a : 𝕎 R) → R)
        ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) : 𝕎 R) :
      R)
    ((ghostComponent 0 : (a : 𝕎 R) → R) (HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y) : R)

Tactic:
ghost_simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
this_1 :
  IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    (verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R))
this :
  IsPoly₂.{u_1} p fun {R : Type u_1} [CommRing R] (x y : 𝕎 R) ↦
    HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
n : ℕ
⊢ Eq (α := R)
    ((ghostComponent (n + 1) : (a : 𝕎 R) → R)
        ((verschiebung : (a : 𝕎 R) → 𝕎 R) (HMul.hMul (β := 𝕎 R) x ((frobenius : (a : 𝕎 R) → 𝕎 R) y : 𝕎 R)) : 𝕎 R) :
      R)
    ((ghostComponent (n + 1) : (a : 𝕎 R) → R) (HMul.hMul (α := 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R) y) : R)

Tactic:
ghost_simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
rw :
  Eq.{u_1 + 1} (α := R) (coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) 0) 0
rw₁ : HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) 0) p = 0
rw₂ : HPow.hPow (α := R) 0 p = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (x * (↑p : 𝕎 R)).coeff 0 = 0

Tactic:
rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_zero,
    zero_pow hp.out.ne_zero]

Premises used: WittVector.verschiebung_coeff_zero, WittVector.coeff_frobenius_charP, Nat.Prime.ne_zero, WittVector.frobenius_verschiebung, zero_pow, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
i : ℕ
rw : coeff (p := p) ((frobenius : (a : 𝕎 R) → 𝕎 R) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x : 𝕎 R)) (i + 1) = x.coeff i ^ p
rw₁ : HPow.hPow (α := R) (coeff (p := p) ((verschiebung : (a : 𝕎 R) → 𝕎 R) x) (i + 1)) p = x.coeff i ^ p
rw₂ rw₃ : x.coeff i ^ p = x.coeff i ^ p
⊢ (x * (↑p : 𝕎 R)).coeff (i + 1) = x.coeff i ^ p

Tactic:
rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ]

Premises used: WittVector.verschiebung_coeff_succ, WittVector.coeff_frobenius_charP, WittVector.frobenius_verschiebung
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
m : ℕ
h : m < 0
⊢ (x * HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff m = 0

Tactic:
contradiction
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
m : ℕ
h : m < n + 1
succ : (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff m = 0
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)).coeff m = 0

Tactic:
rw [pow_succ, ← mul_assoc]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
h : 0 < n + 1
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff 0 = 0

Tactic:
mul_charP_coeff_zero _

Premises used: WittVector.mul_charP_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
h : 0 < n + 1
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff 0 = 0

Tactic:
exact mul_charP_coeff_zero _

Premises used: WittVector.mul_charP_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
succ : m' < n
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff (m' + 1) = 0

Tactic:
rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_zero]

Premises used: Nat.Prime.ne_zero, zero_pow, Fact.out, WittVector.mul_charP_coeff_succ
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ m' < n

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0
m : ℕ
h : m < n + 1
succ : ∀ (h : 0 < n + 1), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff 0 = 0
succ₁ : ∀ (m' : ℕ) (h : m' + 1 < n + 1), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff (m' + 1) = 0
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)).coeff m = 0

Tactic:
cases m with
    | zero => exact mul_charP_coeff_zero _
    | succ m' =>
      rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_zero]
      simpa using h

Premises used: Nat.Prime.ne_zero, WittVector.mul_charP_coeff_zero, zero_pow, Fact.out, WittVector.mul_charP_coeff_succ
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
m n : ℕ
h : m < n
zero : ∀ {m : ℕ} (h : m < 0), (x * HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff m = 0
succ :
  ∀ (n : ℕ) (ih : ∀ {m : ℕ} (h : m < n), (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0) {m : ℕ} (h : m < n + 1),
    (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)).coeff m = 0
⊢ (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n).coeff m = 0

Tactic:
induction n generalizing m with
  | zero => contradiction
  | succ n ih =>
    rw [pow_succ, ← mul_assoc]
    cases m with
    | zero => exact mul_charP_coeff_zero _
    | succ m' =>
      rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_zero]
      simpa using h

Premises used: pow_succ, mul_assoc, Nat.Prime.ne_zero, WittVector.mul_charP_coeff_zero, zero_pow, Fact.out, WittVector.mul_charP_coeff_succ
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
m : ℕ
⊢ (x * HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0).coeff (m + 0) = x.coeff m ^ HPow.hPow (β := ℕ) p 0

Tactic:
simp