awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ truncateFun n (x + y) = truncateFun n x + truncateFun n y
have witt_truncateFun_tac : truncateFun n (x + y) = truncateFun n ((truncateFun n x).out + (truncateFun n y).out)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ :
  truncateFun n (x + y) = truncateFun n ((truncateFun n x).out + (truncateFun n y).out)
⊢ truncateFun n (x + y) = truncateFun n x + truncateFun n y
have a : (truncateFun n (x + y)).out = (truncateFun n ((truncateFun n x).out + (truncateFun n y).out)).out
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ :
  truncateFun n (x + y) = truncateFun n ((truncateFun n x).out + (truncateFun n y).out)
a a₁ : (truncateFun n (x + y)).out = (truncateFun n ((truncateFun n x).out + (truncateFun n y).out)).out
⊢ truncateFun n (x + y) = truncateFun n x + truncateFun n y
have a₂ : init n (x + y) = init n (init n x + init n y)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ truncateFun n (x * y) = truncateFun n x * truncateFun n y
have witt_truncateFun_tac : truncateFun n (x * y) = truncateFun n ((truncateFun n x).out * (truncateFun n y).out)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ :
  truncateFun n (x * y) = truncateFun n ((truncateFun n x).out * (truncateFun n y).out)
⊢ truncateFun n (x * y) = truncateFun n x * truncateFun n y
have a : (truncateFun n (x * y)).out = (truncateFun n ((truncateFun n x).out * (truncateFun n y).out)).out
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ :
  truncateFun n (x * y) = truncateFun n ((truncateFun n x).out * (truncateFun n y).out)
a a₁ : (truncateFun n (x * y)).out = (truncateFun n ((truncateFun n x).out * (truncateFun n y).out)).out
⊢ truncateFun n (x * y) = truncateFun n x * truncateFun n y
have a₂ : init n (x * y) = init n (init n x * init n y)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
⊢ truncateFun n (-x) = -truncateFun n x
have witt_truncateFun_tac : truncateFun n (-x) = truncateFun n (-(truncateFun n x).out)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ : truncateFun n (-x) = truncateFun n (-(truncateFun n x).out)
⊢ truncateFun n (-x) = -truncateFun n x
have a : (truncateFun n (-x)).out = (truncateFun n (-(truncateFun n x).out)).out
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ : truncateFun n (-x) = truncateFun n (-(truncateFun n x).out)
a a₁ : (truncateFun n (-x)).out = (truncateFun n (-(truncateFun n x).out)).out
⊢ truncateFun n (-x) = -truncateFun n x
have a₂ : init n (-x) = init n (-init n x)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ truncateFun n (x - y) = truncateFun n x - truncateFun n y
have witt_truncateFun_tac : truncateFun n (x - y) = truncateFun n ((truncateFun n x).out - (truncateFun n y).out)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ :
  truncateFun n (x - y) = truncateFun n ((truncateFun n x).out - (truncateFun n y).out)
⊢ truncateFun n (x - y) = truncateFun n x - truncateFun n y
have a : (truncateFun n (x - y)).out = (truncateFun n ((truncateFun n x).out - (truncateFun n y).out)).out
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ :
  truncateFun n (x - y) = truncateFun n ((truncateFun n x).out - (truncateFun n y).out)
a a₁ : (truncateFun n (x - y)).out = (truncateFun n ((truncateFun n x).out - (truncateFun n y).out)).out
⊢ truncateFun n (x - y) = truncateFun n x - truncateFun n y
have a₂ : init n (x - y) = init n (init n x - init n y)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
⊢ truncateFun n (m • x) = m • truncateFun n x
have witt_truncateFun_tac : truncateFun n (m • x) = truncateFun n (m • (truncateFun n x).out)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ : truncateFun n (m • x) = truncateFun n (m • (truncateFun n x).out)
⊢ truncateFun n (m • x) = m • truncateFun n x
have a : (truncateFun n (m • x)).out = (truncateFun n (m • (truncateFun n x).out)).out
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ : truncateFun n (m • x) = truncateFun n (m • (truncateFun n x).out)
a a₁ : (truncateFun n (m • x)).out = (truncateFun n (m • (truncateFun n x).out)).out
⊢ truncateFun n (m • x) = m • truncateFun n x
have a₂ : init n (m • x) = init n (m • init n x)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
⊢ truncateFun n (m • x) = m • truncateFun n x
have witt_truncateFun_tac : truncateFun n (m • x) = truncateFun n (m • (truncateFun n x).out)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ : truncateFun n (m • x) = truncateFun n (m • (truncateFun n x).out)
⊢ truncateFun n (m • x) = m • truncateFun n x
have a : (truncateFun n (m • x)).out = (truncateFun n (m • (truncateFun n x).out)).out
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
witt_truncateFun_tac witt_truncateFun_tac₁ : truncateFun n (m • x) = truncateFun n (m • (truncateFun n x).out)
a a₁ : (truncateFun n (m • x)).out = (truncateFun n (m • (truncateFun n x).out)).out
⊢ truncateFun n (m • x) = m • truncateFun n x
have a₂ : init n (m • x) = init n (m • init n x)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
m : ℕ
⊢ truncateFun n (x ^ m) = truncateFun n x ^ m
have witt_truncateFun_tac : truncateFun n (x ^ m) = truncateFun n ((truncateFun n x).out ^ m)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
m : ℕ
witt_truncateFun_tac witt_truncateFun_tac₁ : truncateFun n (x ^ m) = truncateFun n ((truncateFun n x).out ^ m)
⊢ truncateFun n (x ^ m) = truncateFun n x ^ m
have a : (truncateFun n (x ^ m)).out = (truncateFun n ((truncateFun n x).out ^ m)).out
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
m : ℕ
witt_truncateFun_tac witt_truncateFun_tac₁ : truncateFun n (x ^ m) = truncateFun n ((truncateFun n x).out ^ m)
a a₁ : (truncateFun n (x ^ m)).out = (truncateFun n ((truncateFun n x).out ^ m)).out
⊢ truncateFun n (x ^ m) = truncateFun n x ^ m
have a₂ : init n (x ^ m) = init n (init n x ^ m)
Tactic: witt_truncateFun_tac
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
⊢ Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p n R) (truncate n)) x ↔
    ∀ i < n, x.coeff i = 0
have simp : (∀ (i : Fin n),
    Eq.{u_1 + 1} (α := R)
      (TruncatedWittVector.coeff (p := p) i
        (({ toFun := truncateFun n, map_one' := sorry, map_mul' := sorry } : (a : 𝕎 R) → TruncatedWittVector p n R) x))
      0) ↔
  ∀ i < n, x.coeff i = 0
Tactic: simp only [RingHom.mem_ker, truncate, RingHom.coe_mk, TruncatedWittVector.ext_iff,
    coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
f : ℕ → R
⊢ Eq (α := TruncatedWittVector p n R)
    ((truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) { coeff := f } : TruncatedWittVector p n R)
    (TruncatedWittVector.mk p fun (k : Fin n) ↦ f (↑k : ℕ) : TruncatedWittVector p n R)
have h : ∀ (i : Fin n),
  Eq.{u_1 + 1} (α := R)
    (TruncatedWittVector.coeff (p := p) i ((truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) { coeff := f }))
    (TruncatedWittVector.coeff i (TruncatedWittVector.mk p fun (k : Fin n) ↦ f (↑k : ℕ)))
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : 𝕎 R
⊢ Membership.mem (γ := Submodule (𝕎 R) (𝕎 R))
      (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p m R) (WittVector.truncate m)) x →
    Membership.mem (γ := Submodule (𝕎 R) (𝕎 R))
      (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p n R) (WittVector.truncate n)) x
have simp : (∀ i < m, x.coeff i = 0) → ∀ i < n, x.coeff i = 0
Tactic: simp only [WittVector.mem_ker_truncate]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
x : TruncatedWittVector p n₃ R
⊢ Eq (α := TruncatedWittVector p n₁ R)
    ((truncate h1 : (a : TruncatedWittVector p n₂ R) → TruncatedWittVector p n₁ R)
        ((truncate h2 : (a : TruncatedWittVector p n₃ R) → TruncatedWittVector p n₂ R) x : TruncatedWittVector p n₂ R) :
      TruncatedWittVector p n₁ R)
    ((truncate ⋯ : (a : TruncatedWittVector p n₃ R) → TruncatedWittVector p n₁ R) x : TruncatedWittVector p n₁ R)
have obtain : ∀ (x : 𝕎 R),
  Eq (α := TruncatedWittVector p n₁ R)
    ((truncate h1 : (a : TruncatedWittVector p n₂ R) → TruncatedWittVector p n₁ R)
        ((truncate h2 : (a : TruncatedWittVector p n₃ R) → TruncatedWittVector p n₂ R)
            ((WittVector.truncate n₃ : (a : 𝕎 R) → TruncatedWittVector p n₃ R) x : TruncatedWittVector p n₃ R) :
          TruncatedWittVector p n₂ R) :
      TruncatedWittVector p n₁ R)
    ((truncate sorry : (a : TruncatedWittVector p n₃ R) → TruncatedWittVector p n₁ R)
        ((WittVector.truncate n₃ : (a : 𝕎 R) → TruncatedWittVector p n₃ R) x : TruncatedWittVector p n₃ R) :
      TruncatedWittVector p n₁ R)
Tactic: obtain ⟨x, rfl⟩ := WittVector.truncate_surjective (p := p) n₃ R x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
⊢ Eq.{u_1 + 1} (α := TruncatedWittVector p n₃ R →+* TruncatedWittVector p n₁ R)
    (RingHom.comp (truncate h1) (truncate h2)) (truncate ⋯)
have a : ∀ (x : TruncatedWittVector p n₃ R),
  Eq (α := TruncatedWittVector p n₁ R)
    ((RingHom.comp (truncate h1) (truncate h2) : (a : TruncatedWittVector p n₃ R) → TruncatedWittVector p n₁ R) x :
      TruncatedWittVector p n₁ R)
    ((truncate sorry : (a : TruncatedWittVector p n₃ R) → TruncatedWittVector p n₁ R) x : TruncatedWittVector p n₁ R)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p n R
⊢ ∃ (a : TruncatedWittVector p m R), (truncate hm : (a : TruncatedWittVector p m R) → TruncatedWittVector p n R) a = x
have obtain : ∀ (x : 𝕎 R),
  ∃ (a : TruncatedWittVector p m R),
    Eq (α := TruncatedWittVector p n R)
      ((truncate hm : (a : TruncatedWittVector p m R) → TruncatedWittVector p n R) a : TruncatedWittVector p n R)
      ((WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
Tactic: obtain ⟨x, rfl⟩ := WittVector.truncate_surjective (p := p) _ R x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
i : Fin n
x : TruncatedWittVector p m R
⊢ coeff (p := p) i ((truncate hm : (a : TruncatedWittVector p m R) → TruncatedWittVector p n R) x) =
    coeff (Fin.castLE hm i) x
have obtain : ∀ (y : 𝕎 R),
  Eq.{u_1 + 1} (α := R)
    (coeff (p := p) i
      ((truncate hm : (a : TruncatedWittVector p m R) → TruncatedWittVector p n R)
        ((WittVector.truncate m : (a : 𝕎 R) → TruncatedWittVector p m R) y : TruncatedWittVector p m R)))
    (coeff (p := p) (Fin.castLE hm i) ((WittVector.truncate m : (a : 𝕎 R) → TruncatedWittVector p m R) y))
Tactic: obtain ⟨y, rfl⟩ := @WittVector.truncate_surjective p _ _ _ _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
⊢ Eq.{u_1 + 1} (α := Ideal (𝕎 R))
    (⨅ (i : ℕ), RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (WittVector.truncate i)) ⊥
have rw : ∀ (x : 𝕎 R),
  Membership.mem (γ := Submodule (𝕎 R) (𝕎 R))
      (⨅ (i : ℕ), RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (WittVector.truncate i)) x →
    x = 0
Tactic: rw [Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
hx :
  Membership.mem (γ := Submodule (𝕎 R) (𝕎 R))
    (⨅ (i : ℕ), RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (WittVector.truncate i)) x
⊢ x = 0
have h : ∀ (n : ℕ), x.coeff n = WittVector.coeff (p := p) 0 n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
hx :
  Membership.mem (γ := Submodule (𝕎 R) (𝕎 R))
    (⨅ (i : ℕ), RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (WittVector.truncate i)) x
n : ℕ
⊢ x.coeff n = WittVector.coeff (p := p) 0 n
have h : ∀ (hx : ∀ (i i_1 : ℕ), i_1 < i → x.coeff i_1 = 0), x.coeff n = 0
Tactic: simp only [WittVector.mem_ker_truncate, Ideal.mem_iInf, WittVector.zero_coeff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
s : S
⊢ Eq (α := TruncatedWittVector p n R)
    ((truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (liftFun f s) : TruncatedWittVector p n R)
    ((f n : (a : S) → TruncatedWittVector p n R) s : TruncatedWittVector p n R)
have h : ∀ (i : Fin n),
  Eq.{u_1 + 1} (α := R)
    (TruncatedWittVector.coeff (p := p) i ((truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (liftFun f s)))
    (TruncatedWittVector.coeff (p := p) i ((f n : (a : S) → TruncatedWittVector p n R) s))
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
s : S
i : Fin n
⊢ Eq.{u_1 + 1} (α := R)
    (TruncatedWittVector.coeff (p := p) i ((truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) (liftFun f s)))
    (TruncatedWittVector.coeff (p := p) i ((f n : (a : S) → TruncatedWittVector p n R) s))
have h : Eq.{u_1 + 1} (α := R)
  (TruncatedWittVector.coeff (p := p) (n := (↑i : ℕ) + 1) (Fin.last (↑i : ℕ))
    ((f ((↑i : ℕ) + 1) : (a : S) → TruncatedWittVector p ((↑i : ℕ) + 1) R) s))
  (TruncatedWittVector.coeff (p := p) i ((f n : (a : S) → TruncatedWittVector p n R) s))
Tactic: simp only [liftFun, TruncatedWittVector.coeff_mk, WittVector.truncate_mk']
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
s : S
i : Fin n
⊢ Eq.{u_1 + 1} (α := R)
    (TruncatedWittVector.coeff (p := p) (n := (↑i : ℕ) + 1) (Fin.last (↑i : ℕ))
      ((f ((↑i : ℕ) + 1) : (a : S) → TruncatedWittVector p ((↑i : ℕ) + 1) R) s))
    (TruncatedWittVector.coeff (p := p) i ((f n : (a : S) → TruncatedWittVector p n R) s))
have h : Eq.{u_1 + 1} (α := R)
  (TruncatedWittVector.coeff (p := p) (Fin.castLE sorry (Fin.last (↑i : ℕ)))
    ((f n : (a : S) → TruncatedWittVector p n R) s))
  (TruncatedWittVector.coeff (p := p) i ((f n : (a : S) → TruncatedWittVector p n R) s))
Tactic: rw [← f_compat (i + 1) n i.is_lt, RingHom.comp_apply, TruncatedWittVector.coeff_truncate]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ RingHom.{u_2, u_1} S (𝕎 R)
have refine_1 : liftFun f 1 = 1
Tactic: refine { toFun := liftFun f
           map_zero' := ?_
           map_one' := ?_
           map_add' := ?_
           map_mul' := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
refine_1 : liftFun f 1 = 1
⊢ RingHom.{u_2, u_1} S (𝕎 R)
have refine_2 : ∀ (x y : S), liftFun f (x * y) = liftFun f x * liftFun f y
Tactic: refine { toFun := liftFun f
           map_zero' := ?_
           map_one' := ?_
           map_add' := ?_
           map_mul' := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
refine_1 : liftFun f 1 = 1
refine_2 : ∀ (x y : S), liftFun f (x * y) = liftFun f x * liftFun f y
⊢ RingHom.{u_2, u_1} S (𝕎 R)
have refine_3 : liftFun f 0 = 0
Tactic: refine { toFun := liftFun f
           map_zero' := ?_
           map_one' := ?_
           map_add' := ?_
           map_mul' := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
refine_1 : liftFun f 1 = 1
refine_2 : ∀ (x y : S), liftFun f (x * y) = liftFun f x * liftFun f y
refine_3 : liftFun f 0 = 0
⊢ RingHom.{u_2, u_1} S (𝕎 R)
have refine_4 : ∀ (x y : S), liftFun f (x + y) = liftFun f x + liftFun f y
Tactic: refine { toFun := liftFun f
           map_zero' := ?_
           map_one' := ?_
           map_add' := ?_
           map_mul' := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ liftFun f 1 = 1
have refine_1 : ∀ (i : ℕ),
  Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
    (liftFun f 1 - 1)
Tactic: rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x y : S
⊢ liftFun f (x * y) = liftFun f x * liftFun f y
have refine_2 : ∀ (i : ℕ),
  Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
    (liftFun f (x * y) - liftFun f x * liftFun f y)
Tactic: rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ liftFun f 0 = 0
have refine_3 : ∀ (i : ℕ),
  Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
    (liftFun f 0 - 0)
Tactic: rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
x y : S
⊢ liftFun f (x + y) = liftFun f x + liftFun f y
have refine_4 : ∀ (i : ℕ),
  Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
    (liftFun f (x + y) - (liftFun f x + liftFun f y))
Tactic: rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Truncated (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
S : Type u_2
inst_2 : Semiring S
f : (k : ℕ) → RingHom.{u_2, u_1} S (TruncatedWittVector p k R)
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), RingHom.comp (TruncatedWittVector.truncate hk) (f k₂) = f k₁
⊢ RingHom.comp (truncate n) (lift f f_compat) = f n
have a : ∀ (x : S),
  Eq.{u_1 + 1} (α := TruncatedWittVector p n R)
    ((RingHom.comp (truncate n) (lift f f_compat) : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
    ((f n : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
Tactic: ext1