awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
a b : (ValueGroupWithZero R)ˣ
this : Valuation.IsEquiv (Γ₀ := ValueGroupWithZero R) (Γ'₀ := Γ) (valuation R) 1
r s : ↥(posSubmonoid R)
hr :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) =
    (↑a : ValueGroupWithZero R)
t u : ↥(posSubmonoid R)
ht :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑t : R) : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑u : R) : ValueGroupWithZero R) =
    (↑b : ValueGroupWithZero R)
⊢ Eq (α := Γ) ((1 : (a : R) → Γ) ((↑r : R) * (↑u : R)) : Γ) ((1 : (a : R) → Γ) ((↑t : R) * (↑s : R)) : Γ)

Tactic:
simp [one_apply_posSubmonoid]

Premises used: ValuativeRel.one_apply_posSubmonoid
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
a b : (ValueGroupWithZero R)ˣ
this : Valuation.IsEquiv (Γ₀ := ValueGroupWithZero R) (Γ'₀ := Γ) (valuation R) 1
r s : ↥(posSubmonoid R)
hr :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) =
    (↑a : ValueGroupWithZero R)
t u : ↥(posSubmonoid R)
ht :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑t : R) : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑u : R) : ValueGroupWithZero R) =
    (↑b : ValueGroupWithZero R)
⊢ Ne (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)
    (0 : ValueGroupWithZero R)

Tactic:
simp [one_apply_posSubmonoid]

Premises used: ValuativeRel.one_apply_posSubmonoid
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
a b : (ValueGroupWithZero R)ˣ
this : Valuation.IsEquiv (Γ₀ := ValueGroupWithZero R) (Γ'₀ := Γ) (valuation R) 1
r s : ↥(posSubmonoid R)
hr :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) =
    (↑a : ValueGroupWithZero R)
t u : ↥(posSubmonoid R)
ht :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑t : R) : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑u : R) : ValueGroupWithZero R) =
    (↑b : ValueGroupWithZero R)
⊢ Ne (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (↑u : R) : ValueGroupWithZero R)
    (0 : ValueGroupWithZero R)

Tactic:
simp [one_apply_posSubmonoid]

Premises used: ValuativeRel.one_apply_posSubmonoid
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
x : ValueGroupWithZero R
hx : x ≠ 0
hx' : x ≠ 1
⊢ Subsingleton (ValueGroupWithZero R)ˣ

Tactic:
have := subsingleton_units_valueGroupWithZero_of_trivialRel R Γ
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
x : ValueGroupWithZero R
hx : x ≠ 0
hx' : x ≠ 1
this : Subsingleton (ValueGroupWithZero R)ˣ
inl : ∀ (hx : Ne (α := ValueGroupWithZero R) 0 0) (hx' : Ne (α := ValueGroupWithZero R) 0 1), False
inr :
  ∀ (u : (ValueGroupWithZero R)ˣ) (hx : (↑u : ValueGroupWithZero R) ≠ 0) (hx' : (↑u : ValueGroupWithZero R) ≠ 1), False
⊢ False

Tactic:
rcases GroupWithZero.eq_zero_or_unit x with rfl | ⟨u, rfl⟩

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
this : Subsingleton (ValueGroupWithZero R)ˣ
hx : Ne (α := ValueGroupWithZero R) 0 0
hx' : Ne (α := ValueGroupWithZero R) 0 1
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
this : Subsingleton (ValueGroupWithZero R)ˣ
u : (ValueGroupWithZero R)ˣ
hx : (↑u : ValueGroupWithZero R) ≠ 0
hx' : (↑u : ValueGroupWithZero R) ≠ 1
⊢ False

Tactic:
simp_all [Subsingleton.elim u 1]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
⊢ IsDiscrete R

Tactic:
⟨⟨0, zero_lt_one, fun x ↦ ?_⟩⟩

Premises used: ValuativeRel.IsDiscrete.mk, zero_lt_one, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
refine : ∀ x < 1, x ≤ 0
⊢ IsDiscrete R

Tactic:
refine ⟨⟨0, zero_lt_one, fun x ↦ ?_⟩⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
x : ValueGroupWithZero R
⊢ Subsingleton (ValueGroupWithZero R)ˣ

Tactic:
have := subsingleton_units_valueGroupWithZero_of_trivialRel R Γ
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
x : ValueGroupWithZero R
this : Subsingleton (ValueGroupWithZero R)ˣ
inl : LT.lt (α := ValueGroupWithZero R) 0 1 → LE.le (α := ValueGroupWithZero R) 0 0
inr : ∀ (u : (ValueGroupWithZero R)ˣ), (↑u : ValueGroupWithZero R) < 1 → (↑u : ValueGroupWithZero R) ≤ 0
⊢ x < 1 → x ≤ 0

Tactic:
rcases GroupWithZero.eq_zero_or_unit x with rfl | ⟨u, rfl⟩

Premises used: GroupWithZero.eq_zero_or_unit, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
this : Subsingleton (ValueGroupWithZero R)ˣ
⊢ LT.lt (α := ValueGroupWithZero R) 0 1 → LE.le (α := ValueGroupWithZero R) 0 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
this : Subsingleton (ValueGroupWithZero R)ˣ
u : (ValueGroupWithZero R)ˣ
⊢ u < 1 → (↑u : ValueGroupWithZero R) ≤ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ Injective (α := 𝕎 α) (mapFun f)

Tactic:
fun _ _ h => ext fun n => hf (congr_arg (fun x => coeff x n) h :)

Premises used: congr_arg, Function.Injective, WittVector.ext, WittVector.coeff
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Surjective f
x : 𝕎 β
h :
  ∀ (n : ℕ),
    (mapFun f (mk p fun (n : ℕ) ↦ Classical.choose (p := fun (x_1 : α) ↦ f x_1 = x.coeff n) ⋯)).coeff n = x.coeff n
⊢ mapFun f (mk p fun (n : ℕ) ↦ Classical.choose (p := fun (x_1 : α) ↦ f x_1 = x.coeff n) ⋯) = x

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Surjective f
x : 𝕎 β
n : ℕ
⊢ (mapFun f (mk p fun (n : ℕ) ↦ Classical.choose (p := fun (x_1 : α) ↦ f x_1 = x.coeff n) ⋯)).coeff n = x.coeff n

Tactic:
simp only [mapFun, coeff_mk, comp_apply, Classical.choose_spec (hf (x.coeff n))]

Premises used: Classical.choose_spec, WittVector.coeff_mk, Function.comp_apply, WittVector.coeff, WittVector.mapFun
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
h h₁ :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := S) (coeff (p := p) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) 0) n) (coeff (p := p) 0 n)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) 0) 0

Tactic:
map_fun_tac
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
h h₁ :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := S) (coeff (p := p) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) 1) n) (coeff (p := p) 1 n)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) 1) 1

Tactic:
map_fun_tac
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x y : 𝕎 R
h h₁ :
  ∀ (n : ℕ),
    coeff (mapFun (⇑f : (a : R) → S) (x + y)) n =
      (HAdd.hAdd (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) (mapFun (⇑f : (a : R) → S) y)).coeff n
⊢ mapFun (⇑f : (a : R) → S) (x + y) = HAdd.hAdd (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) (mapFun (⇑f : (a : R) → S) y)

Tactic:
map_fun_tac
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x y : 𝕎 R
h h₁ :
  ∀ (n : ℕ),
    coeff (mapFun (⇑f : (a : R) → S) (x - y)) n =
      (HSub.hSub (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) (mapFun (⇑f : (a : R) → S) y)).coeff n
⊢ mapFun (⇑f : (a : R) → S) (x - y) = HSub.hSub (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) (mapFun (⇑f : (a : R) → S) y)

Tactic:
map_fun_tac
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x y : 𝕎 R
h h₁ :
  ∀ (n : ℕ),
    coeff (mapFun (⇑f : (a : R) → S) (x * y)) n =
      (HMul.hMul (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) (mapFun (⇑f : (a : R) → S) y)).coeff n
⊢ mapFun (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) (mapFun (⇑f : (a : R) → S) y)

Tactic:
map_fun_tac
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h h₁ :
  ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) (coeff (mapFun (⇑f : (a : R) → S) (-x)) n) (coeff (-mapFun (⇑f : (a : R) → S) x) n)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) (-x)) (-mapFun (⇑f : (a : R) → S) x)

Tactic:
map_fun_tac
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
n : ℕ
x : 𝕎 R
h h₁ :
  ∀ (n_1 : ℕ),
    coeff (mapFun (⇑f : (a : R) → S) (n • x)) n_1 = (HSMul.hSMul (β := 𝕎 S) n (mapFun (⇑f : (a : R) → S) x)).coeff n_1
⊢ mapFun (⇑f : (a : R) → S) (n • x) = HSMul.hSMul (β := 𝕎 S) n (mapFun (⇑f : (a : R) → S) x)

Tactic:
map_fun_tac
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
z : ℤ
x : 𝕎 R
h h₁ :
  ∀ (n : ℕ),
    coeff (mapFun (⇑f : (a : R) → S) (z • x)) n = (HSMul.hSMul (β := 𝕎 S) z (mapFun (⇑f : (a : R) → S) x)).coeff n
⊢ mapFun (⇑f : (a : R) → S) (z • x) = HSMul.hSMul (β := 𝕎 S) z (mapFun (⇑f : (a : R) → S) x)

Tactic:
map_fun_tac
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n : ℕ
h h₁ :
  ∀ (n_1 : ℕ),
    coeff (mapFun (⇑f : (a : R) → S) (x ^ n)) n_1 = (HPow.hPow (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) n).coeff n_1
⊢ mapFun (⇑f : (a : R) → S) (x ^ n) = HPow.hPow (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) n

Tactic:
map_fun_tac
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
n : ℕ
zero : Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (Nat.unaryCast 0)) (↑0 : 𝕎 S)
succ :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) n.unaryCast) (↑n : 𝕎 S) →
      Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (n + 1).unaryCast) (↑(n + 1) : 𝕎 S)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) n.unaryCast) (↑n : 𝕎 S)

Tactic:
induction n
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
zero : Eq.{u_2 + 1} (α := 𝕎 S) 0 (↑0 : 𝕎 S)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (Nat.unaryCast 0)) (↑0 : 𝕎 S)

Tactic:
simp [*, Nat.unaryCast, add, one, zero]

Premises used: WittVector.mapFun.zero, WittVector.mapFun.add, WittVector.mapFun.one, Nat.unaryCast
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
n : ℕ
h : Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) n.unaryCast) (↑n : 𝕎 S)
succ : HAdd.hAdd (α := 𝕎 S) (↑n : 𝕎 S) 1 = (↑(n + 1) : 𝕎 S)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (n + 1).unaryCast) (↑(n + 1) : 𝕎 S)

Tactic:
simp [*, Nat.unaryCast, add, one, zero]

Premises used: WittVector.mapFun.zero, WittVector.mapFun.add, WittVector.mapFun.one, Nat.unaryCast
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
⊢ Eq.{u_2 + 1} (α := 𝕎 S) 0 (↑0 : 𝕎 S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
n : ℕ
h : Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) n.unaryCast) (↑n : 𝕎 S)
⊢ HAdd.hAdd (α := 𝕎 S) (↑n : 𝕎 S) 1 = (↑(n + 1) : 𝕎 S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
n : ℤ
ofNat :
  ∀ (a : ℕ),
    Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (Int.ofNat a).castDef) (↑(Int.ofNat a) : 𝕎 S)
negSucc :
  ∀ (a : ℕ),
    Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (Int.negSucc a).castDef)
      (↑(Int.negSucc a) : 𝕎 S)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) n.castDef) (↑n : 𝕎 S)

Tactic:
cases n
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
a : ℕ
ofNat : Eq.{u_2 + 1} (α := 𝕎 S) (↑a : 𝕎 S) (↑(↑a : ℤ) : 𝕎 S)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (Int.ofNat a).castDef) (↑(Int.ofNat a) : 𝕎 S)

Tactic:
simp [*, Int.castDef, neg, natCast]

Premises used: Int.castDef, WittVector.mapFun.natCast, WittVector.mapFun.neg
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
a : ℕ
negSucc : Eq.{u_2 + 1} (α := 𝕎 S) (-(↑(a + 1) : 𝕎 S)) (↑(Int.negSucc a) : 𝕎 S)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (Int.negSucc a).castDef)
    (↑(Int.negSucc a) : 𝕎 S)

Tactic:
simp [*, Int.castDef, neg, natCast]

Premises used: Int.castDef, WittVector.mapFun.natCast, WittVector.mapFun.neg
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
a : ℕ
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (↑a : 𝕎 S) (↑(↑a : ℤ) : 𝕎 S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : R →+* S
a : ℕ
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (-(↑(a + 1) : 𝕎 S)) (↑(Int.negSucc a) : 𝕎 S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_5
i : Fin 0
j : ℕ
⊢ Eq.{u_5 + 1} (α := R) (coeff (p := p) (![] i) j) (![] i j)

Tactic:
rcases i with ⟨_ | _ | _ | _ | i_val, ⟨⟩⟩
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
h h₁ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (ghostFun (p := p) 0 n) (0 n)
h₂ h₃ :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R)
        (peval ((bind₁ (wittStructureInt p 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ) (W_ ℤ n)) ![])
        (peval
          ((bind₁ fun (i : Fin 0) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin 0) ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ)
            0)
          ![]) →
      Eq.{u_1 + 1} (α := R) (ghostFun (p := p) 0 n) (0 n)
h₄ h₅ :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R)
        (peval ((bind₁ (wittStructureInt p 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ) (W_ ℤ n)) ![])
        (peval
          ((bind₁ fun (i : Fin 0) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin 0) ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ)
            0)
          ![]) →
      Eq.{u_1 + 1} (α := R)
        (ghostFun (p := p)
          (eval
            (wittStructureInt p { support := ∅, toFun := fun (x : Fin 0 →₀ ℕ) ↦ Int.ofNat 0, mem_support_toFun := ⋯ })
            ![])
          n)
        Zero.zero
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) 0) 0

Tactic:
ghost_fun_tac 0, ![]
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
h h₁ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (ghostFun (p := p) 1 n) (1 n)
h₂ h₃ :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R)
        (peval ((bind₁ (wittStructureInt p 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ) (W_ ℤ n)) ![])
        (peval
          ((bind₁ fun (i : Fin 0) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin 0) ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ)
            1)
          ![]) →
      Eq.{u_1 + 1} (α := R) (ghostFun (p := p) 1 n) (1 n)
h₄ h₅ :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R)
        (peval ((bind₁ (wittStructureInt p 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ) (W_ ℤ n)) ![])
        (peval
          ((bind₁ fun (i : Fin 0) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin 0) ℤ) → MvPolynomial (Fin 0 × ℕ) ℤ)
            1)
          ![]) →
      Eq.{u_1 + 1} (α := R)
        (ghostFun (p := p)
          (eval
            (wittStructureInt p
              (AddMonoidAlgebra.single { support := ∅, toFun := fun (x : Fin 0) ↦ Nat.zero, mem_support_toFun := ⋯ }
                (Int.ofNat 1)))
            ![])
          n)
        One.one
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) 1) 1

Tactic:
ghost_fun_tac 1, ![]
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
h h₁ : ∀ (n : ℕ), (x + y).ghostFun n = (x.ghostFun + y.ghostFun) n
h₂ h₃ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HAdd.hAdd (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1))) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff, y.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0).succ) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0).succ) ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (HAdd.hAdd (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1)))
          ![x.coeff, y.coeff] →
      (x + y).ghostFun n = (x.ghostFun + y.ghostFun) n
h₄ h₅ :
  ∀ (n : ℕ),
    peval
          ((bind₁ (wittStructureInt p (HAdd.hAdd (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1))) :
              (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (W_ ℤ n))
          ![x.coeff, y.coeff] =
        peval
          ((bind₁ fun (i : Fin (Nat.succ 0).succ) ↦
                (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) (W_ ℤ n) :
              (a : MvPolynomial (Fin (Nat.succ 0).succ) ℤ) → MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ)
            (HAdd.hAdd (α := MvPolynomial (Fin (Nat.succ 0).succ) ℤ) (X 0) (X 1)))
          ![x.coeff, y.coeff] →
      (eval (wittAdd p) ![x, y]).ghostFun n = Add.add (x.ghostFun n) (y.ghostFun n)
⊢ (x + y).ghostFun = x.ghostFun + y.ghostFun

Tactic:
ghost_fun_tac X 0 + X 1, ![x.coeff, y.coeff]

Premises used: MvPolynomial.X, WittVector.coeff, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
i : ℕ
zero : Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (Nat.unaryCast 0)) (↑0 : ℕ → R)
succ :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) n.unaryCast) (↑n : ℕ → R) →
      Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (n + 1).unaryCast) (↑(n + 1) : ℕ → R)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) i.unaryCast) (↑i : ℕ → R)

Tactic:
induction i
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (Nat.unaryCast 0)) (↑0 : ℕ → R)

Tactic:
simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add]

Premises used: _private.0.WittVector.ghostFun_zero, _private.0.WittVector.ghostFun_one, _private.0.WittVector.ghostFun_add, Nat.unaryCast
-- Module: Mathlib.RingTheory.WittVector.Basic
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
n : ℕ
h : Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) n.unaryCast) (↑n : ℕ → R)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) (n + 1).unaryCast) (↑(n + 1) : ℕ → R)

Tactic:
simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add]

Premises used: _private.0.WittVector.ghostFun_zero, _private.0.WittVector.ghostFun_one, _private.0.WittVector.ghostFun_add, Nat.unaryCast