awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
⊢ Eq (α := ValuativeRel R) trivialRel (ofValuation (Γ := Γ) 1)
have convert_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
Tactic: convert! (eq_trivialRel_of_compatible_one (Γ := Γ)).symm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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
⊢ Subsingleton (ValueGroupWithZero R)ˣ
have allEq : ∀ (a b : (ValueGroupWithZero R)ˣ), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (hypothesis)
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)ˣ
⊢ a = b
have this : Valuation.IsEquiv (Γ₀ := ValueGroupWithZero R) (Γ'₀ := Γ) (valuation R) 1
Tactic: have : (valuation R).IsEquiv (1 : Valuation R Γ) := isEquiv _ _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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
⊢ a = b
have allEq : ∀ (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)),
  a = b
Tactic: obtain ⟨r, s, hr⟩ := exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq a
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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)
⊢ a = b
have allEq : ∀ (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)),
  a = b
Tactic: obtain ⟨t, u, ht⟩ := exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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)
⊢ a = b
have allEq : Eq (α := Γ) ((1 : (a : R) → Γ) ((↑r : R) * (↑u : R)) : Γ) ((1 : (a : R) → Γ) ((↑t : R) * (↑s : R)) : Γ)
Tactic: rw [Units.ext_iff, ← hr, ← ht, div_eq_div_iff, ← map_mul, ← map_mul, this.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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)
allEq : Eq (α := Γ) ((1 : (a : R) → Γ) ((↑r : R) * (↑u : R)) : Γ) ((1 : (a : R) → Γ) ((↑t : R) * (↑s : R)) : Γ)
⊢ a = b
have allEq₁ : Ne (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)
  (0 : ValueGroupWithZero R)
Tactic: rw [Units.ext_iff, ← hr, ← ht, div_eq_div_iff, ← map_mul, ← map_mul, this.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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)
allEq : Eq (α := Γ) ((1 : (a : R) → Γ) ((↑r : R) * (↑u : R)) : Γ) ((1 : (a : R) → Γ) ((↑t : R) * (↑s : R)) : Γ)
allEq₁ :
  Ne (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)
    (0 : ValueGroupWithZero R)
⊢ a = b
have allEq₂ : Ne (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (↑u : R) : ValueGroupWithZero R)
  (0 : ValueGroupWithZero R)
Tactic: rw [Units.ext_iff, ← hr, ← ht, div_eq_div_iff, ← map_mul, ← map_mul, this.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (hypothesis)
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
⊢ False
have this : Subsingleton (ValueGroupWithZero R)ˣ
Tactic: have := subsingleton_units_valueGroupWithZero_of_trivialRel R Γ
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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)ˣ
⊢ False
have inl : ∀ (hx : Ne (α := ValueGroupWithZero R) 0 0) (hx' : Ne (α := ValueGroupWithZero R) 0 1), False
Tactic: rcases GroupWithZero.eq_zero_or_unit x with rfl | ⟨u, rfl⟩
Cleared hypotheses: x, hx, hx'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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
⊢ False
have inr : ∀ (u : (ValueGroupWithZero R)ˣ) (hx : (↑u : ValueGroupWithZero R) ≠ 0) (hx' : (↑u : ValueGroupWithZero R) ≠ 1), False
Tactic: rcases GroupWithZero.eq_zero_or_unit x with rfl | ⟨u, rfl⟩
Cleared hypotheses: x, hx, hx'
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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
have refine : ∀ x < 1, x ≤ 0
Tactic: refine ⟨⟨0, zero_lt_one, fun x ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (hypothesis)
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
⊢ x < 1 → x ≤ 0
have this : Subsingleton (ValueGroupWithZero R)ˣ
Tactic: have := subsingleton_units_valueGroupWithZero_of_trivialRel R Γ
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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)ˣ
⊢ x < 1 → x ≤ 0
have inl : LT.lt (α := ValueGroupWithZero R) 0 1 → LE.le (α := ValueGroupWithZero R) 0 0
Tactic: rcases GroupWithZero.eq_zero_or_unit x with rfl | ⟨u, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
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
⊢ x < 1 → x ≤ 0
have inr : ∀ (u : (ValueGroupWithZero R)ˣ), (↑u : ValueGroupWithZero R) < 1 → (↑u : ValueGroupWithZero R) ≤ 0
Tactic: rcases GroupWithZero.eq_zero_or_unit x with rfl | ⟨u, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
α : Type u_3
β : Type u_4
f : α → β
hf : Surjective f
x : 𝕎 β
⊢ mapFun f (mk p fun (n : ℕ) ↦ Classical.choose (p := fun (x_1 : α) ↦ f x_1 = x.coeff n) ⋯) = x
have h : ∀ (n : ℕ),
  (mapFun f (mk p fun (n : ℕ) ↦ Classical.choose (p := fun (x_1 : α) ↦ f x_1 = x.coeff n) sorry)).coeff n = x.coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) 0) 0
have 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)
Tactic: map_fun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) 1) 1
have 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)
Tactic: map_fun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ mapFun (⇑f : (a : R) → S) (x + y) = HAdd.hAdd (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) (mapFun (⇑f : (a : R) → S) y)
have 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
Tactic: map_fun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ mapFun (⇑f : (a : R) → S) (x - y) = HSub.hSub (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) (mapFun (⇑f : (a : R) → S) y)
have 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
Tactic: map_fun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ mapFun (⇑f : (a : R) → S) (x * y) = HMul.hMul (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) (mapFun (⇑f : (a : R) → S) y)
have 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
Tactic: map_fun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) (-x)) (-mapFun (⇑f : (a : R) → S) x)
have h : ∀ (n : ℕ), Eq.{u_2 + 1} (α := S) (coeff (mapFun (⇑f : (a : R) → S) (-x)) n) (coeff (-mapFun (⇑f : (a : R) → S) x) n)
Tactic: map_fun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ mapFun (⇑f : (a : R) → S) (n • x) = HSMul.hSMul (β := 𝕎 S) n (mapFun (⇑f : (a : R) → S) x)
have 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
Tactic: map_fun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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
⊢ mapFun (⇑f : (a : R) → S) (z • x) = HSMul.hSMul (β := 𝕎 S) z (mapFun (⇑f : (a : R) → S) x)
have h : ∀ (n : ℕ),
  coeff (mapFun (⇑f : (a : R) → S) (z • x)) n = (HSMul.hSMul (β := 𝕎 S) z (mapFun (⇑f : (a : R) → S) x)).coeff n
Tactic: map_fun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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 : ℕ
⊢ mapFun (⇑f : (a : R) → S) (x ^ n) = HPow.hPow (α := 𝕎 S) (mapFun (⇑f : (a : R) → S) x) n
have 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
Tactic: map_fun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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 : ℕ
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) n.unaryCast) (↑n : 𝕎 S)
have zero : Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (Nat.unaryCast 0)) (↑0 : 𝕎 S)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) n.unaryCast) (↑n : 𝕎 S)
have 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)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (Nat.unaryCast 0)) (↑0 : 𝕎 S)
have zero : Eq.{u_2 + 1} (α := 𝕎 S) 0 (↑0 : 𝕎 S)
Tactic: simp [*, Nat.unaryCast, add, one, zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (n + 1).unaryCast) (↑(n + 1) : 𝕎 S)
have succ : HAdd.hAdd (α := 𝕎 S) (↑n : 𝕎 S) 1 = (↑(n + 1) : 𝕎 S)
Tactic: simp [*, Nat.unaryCast, add, one, zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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 : ℤ
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) n.castDef) (↑n : 𝕎 S)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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)
⊢ Eq.{u_2 + 1} (α := 𝕎 S) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) n.castDef) (↑n : 𝕎 S)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (Int.ofNat a).castDef) (↑(Int.ofNat a) : 𝕎 S)
have ofNat : Eq.{u_2 + 1} (α := 𝕎 S) (↑a : 𝕎 S) (↑(↑a : ℤ) : 𝕎 S)
Tactic: simp [*, Int.castDef, neg, natCast]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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) (mapFun.{u_1, u_2} (α := R) (⇑f : (a : R) → S) (Int.negSucc a).castDef)
    (↑(Int.negSucc a) : 𝕎 S)
have negSucc : Eq.{u_2 + 1} (α := 𝕎 S) (-(↑(a + 1) : 𝕎 S)) (↑(Int.negSucc a) : 𝕎 S)
Tactic: simp [*, Int.castDef, neg, natCast]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) 0) 0
have h : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (ghostFun (p := p) 0 n) (0 n)
Tactic: ghost_fun_tac 0, ![]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) 0) 0
have 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)
Tactic: ghost_fun_tac 0, ![]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) 0) 0
have 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 := sorry })
          ![])
        n)
      Zero.zero
Tactic: ghost_fun_tac 0, ![]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) 1) 1
have h : ∀ (n : ℕ), Eq.{u_1 + 1} (α := R) (ghostFun (p := p) 1 n) (1 n)
Tactic: ghost_fun_tac 1, ![]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) 1) 1
have 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)
Tactic: ghost_fun_tac 1, ![]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := ℕ → R) (ghostFun (p := p) 1) 1
have 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 := sorry }
              (Int.ofNat 1)))
          ![])
        n)
      One.one
Tactic: ghost_fun_tac 1, ![]