awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x y : 𝕎 R
⊢ (x * y).coeff 0 = x.coeff 0 * y.coeff 0

Tactic:
simp [mul_coeff, peval, Function.uncurry]

Premises used: WittVector.peval, WittVector.mul_coeff, Function.uncurry
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittAdd p n).vars ⊆ SProd.sprod (α := Finset (Fin 2)) Finset.univ (Finset.range (n + 1))

Tactic:
wittStructureInt_vars _ _ _

Premises used: Set.Mem, setOf, WittVector.wittAdd, wittStructureInt_vars
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittSub p n).vars ⊆ SProd.sprod (α := Finset (Fin 2)) Finset.univ (Finset.range (n + 1))

Tactic:
wittStructureInt_vars _ _ _

Premises used: Set.Mem, setOf, wittStructureInt_vars, WittVector.wittSub
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittMul p n).vars ⊆ SProd.sprod (α := Finset (Fin 2)) Finset.univ (Finset.range (n + 1))

Tactic:
wittStructureInt_vars _ _ _

Premises used: Set.Mem, setOf, WittVector.wittMul, wittStructureInt_vars
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittNeg p n).vars ⊆ SProd.sprod (α := Finset (Fin 1)) Finset.univ (Finset.range (n + 1))

Tactic:
wittStructureInt_vars _ _ _

Premises used: Set.Mem, setOf, WittVector.wittNeg, wittStructureInt_vars
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
⊢ (wittNSMul p m n).vars ⊆ SProd.sprod (α := Finset (Fin 1)) Finset.univ (Finset.range (n + 1))

Tactic:
wittStructureInt_vars _ _ _

Premises used: Set.Mem, setOf, wittStructureInt_vars, WittVector.wittNSMul
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
n : ℕ
⊢ (wittZSMul p m n).vars ⊆ SProd.sprod (α := Finset (Fin 1)) Finset.univ (Finset.range (n + 1))

Tactic:
wittStructureInt_vars _ _ _

Premises used: Set.Mem, setOf, wittStructureInt_vars, WittVector.wittZSMul
-- Module: Mathlib.RingTheory.WittVector.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
⊢ (wittPow p m n).vars ⊆ SProd.sprod (α := Finset (Fin 1)) Finset.univ (Finset.range (n + 1))

Tactic:
wittStructureInt_vars _ _ _

Premises used: Set.Mem, setOf, wittStructureInt_vars, WittVector.wittPow
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
h : ∀ (n : ℕ), (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
⊢ A * { coeff := inverseCoeff a A : 𝕎 k } = 1

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff 0 = coeff (p := p) 1 0

Tactic:
simp [WittVector.mul_coeff_zero, inverseCoeff, hA]

Premises used: WittVector.mul_coeff_zero, WittVector.inverseCoeff
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) = coeff (p := p) 1 (n + 1)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h :
  ∀ (n : ℕ),
    (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n →
      (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) = coeff (p := p) 1 (n + 1)
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n

Tactic:
induction n with
    | zero => simp [WittVector.mul_coeff_zero, inverseCoeff, hA]
    | succ n => ?_

Premises used: WittVector.mul_coeff_zero, WittVector.inverseCoeff
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
⊢ (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1

Tactic:
have H := Units.mul_inv (a ^ p ^ (n + 1))
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
a₁ :
  (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) + -H_coeff * 1 -
      (coeff (p := p) 1 (n + 1) + -H_coeff * ((↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k))) =
    0
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) = coeff (p := p) 1 (n + 1)

Tactic:
linear_combination (norm := skip) -H_coeff * H
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : a ^ p ^ (n + 1) = a ^ p ^ (n + 1)
⊢ (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
⊢ (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)

Tactic:
have ha : (a : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1)) := by norm_cast
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
ha : (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : a⁻¹ ^ p ^ (n + 1) = (a ^ p ^ (n + 1))⁻¹
⊢ (↑a⁻¹ : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1))⁻¹ : k)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
ha : (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)
⊢ (↑a⁻¹ : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1))⁻¹ : k)

Tactic:
have ha_inv : (↑a⁻¹ : k) ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹ := by norm_cast
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
ha : (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)
ha_inv : (↑a⁻¹ : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1))⁻¹ : k)
a₁ :
  A.coeff (n + 1) * (↑(a ^ p ^ (n + 1))⁻¹ : k) +
            -(↑(a ^ p ^ (n + 1))⁻¹ : k) *
                (A.coeff (n + 1) * (↑(a ^ p ^ (n + 1))⁻¹ : k) +
                  nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)) *
              (↑(a ^ p ^ (n + 1)) : k) +
          nthRemainder p n (truncateFun (n + 1) A) (truncateFun (n + 1) { coeff := inverseCoeff a A : 𝕎 k }) +
        -H_coeff * 1 -
      (0 + -H_coeff * ((↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k))) =
    0
⊢ (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff (n + 1) + -H_coeff * 1 -
      (coeff (p := p) 1 (n + 1) + -H_coeff * ((↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k))) =
    0

Tactic:
simp only [nthRemainder_spec, inverseCoeff, succNthValUnits, hA,
      one_coeff_eq_of_pos, Nat.succ_pos', ha_inv, ha, inv_pow]

Premises used: Nat.succ_pos', WittVector.succNthValUnits, inv_pow, WittVector.one_coeff_eq_of_pos, WittVector.inverseCoeff, WittVector.nthRemainder_spec
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
n : ℕ
h : (A * { coeff := inverseCoeff a A : 𝕎 k }).coeff n = coeff (p := p) 1 n
H_coeff : k :=
  A.coeff (n + 1) * (↑(a⁻¹ ^ p ^ (n + 1)) : k) +
    nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)
H : (↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k) = 1
ha : (↑a : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1)) : k)
ha_inv : (↑a⁻¹ : k) ^ p ^ (n + 1) = (↑(a ^ p ^ (n + 1))⁻¹ : k)
⊢ A.coeff (n + 1) * (↑(a ^ p ^ (n + 1))⁻¹ : k) +
            -(↑(a ^ p ^ (n + 1))⁻¹ : k) *
                (A.coeff (n + 1) * (↑(a ^ p ^ (n + 1))⁻¹ : k) +
                  nthRemainder p n (truncateFun (n + 1) A) fun (i : Fin (n + 1)) ↦ inverseCoeff a A (↑i : ℕ)) *
              (↑(a ^ p ^ (n + 1)) : k) +
          nthRemainder p n (truncateFun (n + 1) A) (truncateFun (n + 1) { coeff := inverseCoeff a A : 𝕎 k }) +
        -H_coeff * 1 -
      (0 + -H_coeff * ((↑(a ^ p ^ (n + 1)) : k) * (↑(a ^ p ^ (n + 1))⁻¹ : k))) =
    0

Tactic:
ring!
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : kˣ
A : 𝕎 k
hA : A.coeff 0 = (↑a : k)
⊢ (↑(mkUnit hA) : 𝕎 k) = A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
x : 𝕎 k
hx : x.coeff 0 ≠ 0
y : kˣ := Units.mk0 (x.coeff 0) hx
⊢ x.coeff 0 = (↑y : k)

Tactic:
have hy : x.coeff 0 = y := rfl
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
x : 𝕎 k
hx : x.coeff 0 ≠ 0
y : kˣ := Units.mk0 (x.coeff 0) hx
hy : x.coeff 0 = (↑y : k)
⊢ IsUnit x

Tactic:
(mkUnit hy).isUnit

Premises used: Units.isUnit, WittVector.mkUnit
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
x : 𝕎 k
hx : x.coeff 0 ≠ 0
y : kˣ := Units.mk0 (x.coeff 0) hx
hy : x.coeff 0 = (↑y : k)
⊢ IsUnit x

Tactic:
exact (mkUnit hy).isUnit

Premises used: Units.isUnit, WittVector.mkUnit
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
⊢ False

Tactic:
simpa only [constantCoeff_apply, coeff_p_zero, not_isUnit_zero] using
      (constantCoeff : WittVector p k →+* _).isUnit_map hp

Premises used: not_isUnit_zero, WittVector.constantCoeff, WittVector.coeff_p_zero, RingHom.isUnit_map, WittVector.constantCoeff_apply
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
⊢ ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)

Tactic:
have hp : ¬IsUnit (p : 𝕎 k) := by
    intro hp
    simpa only [constantCoeff_apply, coeff_p_zero, not_isUnit_zero] using
      (constantCoeff : WittVector p k →+* _).isUnit_map hp
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
⊢ Irreducible.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)

Tactic:
⟨hp, fun a b hab => ?_⟩

Premises used: Irreducible.mk
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
refine : ∀ (a b : 𝕎 k) (hab : (↑p : 𝕎 k) = a * b), IsUnit a ∨ IsUnit b
⊢ Irreducible.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)

Tactic:
refine ⟨hp, fun a b hab => ?_⟩
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
rw : a * b ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
rw [← mul_ne_zero_iff]

Premises used: mul_ne_zero_iff
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
h : a * b = 0
⊢ Eq.{u_1 + 1} (α := 𝕎 k) (↑p : 𝕎 k) 0

Tactic:
rw [h] at hab
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
h : a * b = 0
hab₁ : Eq.{u_1 + 1} (α := 𝕎 k) (↑p : 𝕎 k) 0
⊢ a * b = 0

Tactic:
rw [h] at hab
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a b : 𝕎 k
hab : Eq.{u_1 + 1} (α := 𝕎 k) (↑p : 𝕎 k) 0
h : a * b = 0
⊢ False

Tactic:
p_nonzero p k hab

Premises used: WittVector.p_nonzero
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a b : 𝕎 k
hab : Eq.{u_1 + 1} (α := 𝕎 k) (↑p : 𝕎 k) 0
h : a * b = 0
⊢ False

Tactic:
exact p_nonzero p k hab

Premises used: WittVector.p_nonzero
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
⊢ a ≠ 0

Tactic:
obtain ⟨ha0, hb0⟩ : a ≠ 0 ∧ b ≠ 0 := by
    rw [← mul_ne_zero_iff]; intro h; rw [h] at hab; exact p_nonzero p k hab
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
ha0 : a ≠ 0
⊢ b ≠ 0

Tactic:
obtain ⟨ha0, hb0⟩ : a ≠ 0 ∧ b ≠ 0 := by
    rw [← mul_ne_zero_iff]; intro h; rw [h] at hab; exact p_nonzero p k hab
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a b : 𝕎 k
hab : (↑p : 𝕎 k) = a * b
ha0 : a ≠ 0
hb0 : b ≠ 0
obtain :
  ∀ (m : ℕ) (a : 𝕎 k) (ha : a.coeff 0 ≠ 0) (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a * b)
    (ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a ≠ 0), IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a) ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain ⟨m, a, ha, rfl⟩ := verschiebung_nonzero ha0

Premises used: WittVector.verschiebung_nonzero, rfl
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
b : 𝕎 k
hb0 : b ≠ 0
m : ℕ
a : 𝕎 k
ha : a.coeff 0 ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a * b
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a ≠ 0
obtain :
  ∀ (n : ℕ) (b : 𝕎 k) (hb : b.coeff 0 ≠ 0) (hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b ≠ 0)
    (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b),
    IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a) ∨ IsUnit b

Tactic:
obtain ⟨n, b, hb, rfl⟩ := verschiebung_nonzero hb0

Premises used: WittVector.verschiebung_nonzero, rfl
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
m : ℕ
a : 𝕎 k
ha : a.coeff 0 ≠ 0
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b
zero :
  ∀ (ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a ≠ 0)
    (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b),
    IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
succ :
  ∀ (n_1 : ℕ) (ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a ≠ 0)
    (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b),
    IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[m] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)

Tactic:
cases m
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b ≠ 0
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)

Tactic:
Or.inl (isUnit_of_coeff_zero_ne_zero a ha)

Premises used: WittVector.isUnit_of_coeff_zero_ne_zero, Or.inl
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b ≠ 0
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)

Tactic:
exact Or.inl (isUnit_of_coeff_zero_ne_zero a ha)

Premises used: WittVector.isUnit_of_coeff_zero_ne_zero, Or.inl
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b ≠ 0
n_1 : ℕ
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b
succ :
  ∀ (hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b ≠ 0)
    (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b),
    IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b)
succ₁ :
  ∀ (n : ℕ) (hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b ≠ 0)
    (hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b),
    IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b)
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n] b)

Tactic:
rcases n with - | n
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n : ℕ
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] a ≠ 0
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b)

Tactic:
Or.inr (isUnit_of_coeff_zero_ne_zero b hb)

Premises used: WittVector.isUnit_of_coeff_zero_ne_zero, Or.inr
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n : ℕ
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] a ≠ 0
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b
⊢ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] a) ∨ IsUnit ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[0] b)

Tactic:
exact Or.inr (isUnit_of_coeff_zero_ne_zero b hb)

Premises used: WittVector.isUnit_of_coeff_zero_ne_zero, Or.inr
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n_1 : ℕ
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b ≠ 0
hab : (↑p : 𝕎 k) = (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a * (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b
⊢ (↑p : 𝕎 k) =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1 + (n + 1)]
      ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n + 1] a * (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] b)

Tactic:
rw [iterate_verschiebung_mul] at hab

Premises used: WittVector.iterate_verschiebung_mul
-- Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
k : Type u_1
inst : Field k
inst_1 : CharP k p
hp : ¬IsUnit.{u_1} (M := 𝕎 k) (↑p : 𝕎 k)
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n_1 : ℕ
ha0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n + 1] b ≠ 0
hab :
  (↑p : 𝕎 k) =
    (⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1 + (n + 1)]
      ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n + 1] a * (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] b)
⊢ coeff (p := p) (↑p : 𝕎 k) 1 =
    ((⇑verschiebung : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1 + (n + 1)]
          ((⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n + 1] a * (⇑frobenius : (a : 𝕎 k) → 𝕎 k)^[n_1 + 1] b)).coeff
      1

Tactic:
apply_fun fun x => coeff x 1 at hab

Premises used: WittVector.coeff, OfNat.ofNat