awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Truncated
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 : 𝕎 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 ⋯ : (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:
simp only [truncate_wittVector_truncate]

Premises used: TruncatedWittVector.truncate_wittVector_truncate
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
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 ⋯ : (a : TruncatedWittVector p n₃ R) → TruncatedWittVector p n₁ R) x : TruncatedWittVector p n₁ R)
⊢ Eq.{u_1 + 1} (α := TruncatedWittVector p n₃ R →+* TruncatedWittVector p n₁ R)
    (RingHom.comp (truncate h1) (truncate h2)) (truncate ⋯)

Tactic:
ext1 x
-- Module: Mathlib.RingTheory.WittVector.Truncated
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)
    ((RingHom.comp (truncate h1) (truncate h2) : (a : TruncatedWittVector p n₃ R) → TruncatedWittVector p n₁ R) x :
      TruncatedWittVector p n₁ R)
    ((truncate ⋯ : (a : TruncatedWittVector p n₃ R) → TruncatedWittVector p n₁ R) x : TruncatedWittVector p n₁ R)

Tactic:
simp only [truncate_truncate, Function.comp_apply, RingHom.coe_comp]

Premises used: TruncatedWittVector.truncate_truncate, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
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)
⊢ ∃ (a : TruncatedWittVector p m R), (truncate hm : (a : TruncatedWittVector p m R) → TruncatedWittVector p n R) a = x

Tactic:
obtain ⟨x, rfl⟩ := WittVector.truncate_surjective (p := p) _ R x

Premises used: WittVector.truncate_surjective, rfl
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
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:
⟨WittVector.truncate _ x, truncate_wittVector_truncate _ _⟩

Premises used: TruncatedWittVector.truncate_wittVector_truncate, WittVector.truncate, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
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:
exact ⟨WittVector.truncate _ x, truncate_wittVector_truncate _ _⟩
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
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))
⊢ coeff (p := p) i ((truncate hm : (a : TruncatedWittVector p m R) → TruncatedWittVector p n R) x) =
    coeff (Fin.castLE hm i) x

Tactic:
obtain ⟨y, rfl⟩ := @WittVector.truncate_surjective p _ _ _ _ x

Premises used: WittVector.truncate_surjective, rfl
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
i : Fin n
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:
simp only [truncate_wittVector_truncate, WittVector.coeff_truncate, Fin.val_castLE]

Premises used: WittVector.coeff_truncate, TruncatedWittVector.truncate_wittVector_truncate, Fin.val_castLE
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_2
inst : Fintype R
⊢ Fintype.card.{u_2} (TruncatedWittVector p n R) = Fintype.card R ^ n

Tactic:
simp only [TruncatedWittVector, Fintype.card_fin, Fintype.card_fun]

Premises used: Fintype.card_fin, Fintype.card_fun, TruncatedWittVector
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
rw :
  ∀ (x : 𝕎 R),
    Membership.mem (γ := Submodule (𝕎 R) (𝕎 R))
        (⨅ (i : ℕ), RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (WittVector.truncate i)) x →
      x = 0
⊢ Eq.{u_1 + 1} (α := Ideal (𝕎 R))
    (⨅ (i : ℕ), RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (WittVector.truncate i)) ⊥

Tactic:
rw [Submodule.eq_bot_iff]

Premises used: Submodule.eq_bot_iff
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
h : ∀ (n : ℕ), x.coeff n = WittVector.coeff (p := p) 0 n
⊢ x = 0

Tactic:
ext
-- Module: Mathlib.RingTheory.WittVector.Truncated
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 : ℕ
h : ∀ (hx : ∀ (i i_1 : ℕ), i_1 < i → x.coeff i_1 = 0), x.coeff n = 0
⊢ x.coeff n = WittVector.coeff (p := p) 0 n

Tactic:
simp only [WittVector.mem_ker_truncate, Ideal.mem_iInf, WittVector.zero_coeff] at hx ⊢

Premises used: WittVector.mem_ker_truncate, WittVector.zero_coeff, Ideal.mem_iInf
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ (i i_1 : ℕ), i_1 < i → x.coeff i_1 = 0
⊢ x.coeff n = 0

Tactic:
hx _ _ (Nat.lt_succ_self _)

Premises used: Nat.lt_succ_self
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
hx : ∀ (i i_1 : ℕ), i_1 < i → x.coeff i_1 = 0
⊢ x.coeff n = 0

Tactic:
exact hx _ _ (Nat.lt_succ_self _)

Premises used: Nat.lt_succ_self
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
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))
⊢ 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)

Tactic:
ext i
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
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))
⊢ 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:
simp only [liftFun, TruncatedWittVector.coeff_mk, WittVector.truncate_mk']

Premises used: TruncatedWittVector.coeff_mk, WittVector.liftFun, WittVector.truncate_mk'
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
h :
  Eq.{u_1 + 1} (α := R)
    (TruncatedWittVector.coeff (p := p) (Fin.castLE ⋯ (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))
⊢ 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:
rw [← f_compat (i + 1) n i.is_lt, RingHom.comp_apply, TruncatedWittVector.coeff_truncate]

Premises used: Fin.is_lt, Fin.val, HAdd.hAdd, RingHom.comp_apply, TruncatedWittVector.coeff_truncate, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Truncated
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) (Fin.castLE ⋯ (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:
congr 1 with _
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
refine_4 : ∀ (x y : S), liftFun f (x + y) = liftFun f x + liftFun f y
⊢ RingHom.{u_2, u_1} S (𝕎 R)

Tactic:
refine { toFun := liftFun f
           map_zero' := ?_
           map_one' := ?_
           map_add' := ?_
           map_mul' := ?_ }
-- Module: Mathlib.RingTheory.WittVector.Truncated
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 :
  ∀ (i : ℕ),
    Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
      (liftFun f 1 - 1)
⊢ liftFun f 1 = 1

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Premises used: Ideal.mem_bot, TruncatedWittVector.iInf_ker_truncate, sub_eq_zero, Ideal.mem_iInf
-- Module: Mathlib.RingTheory.WittVector.Truncated
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₁
⊢ ∀ (i : ℕ),
    Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
      (liftFun f 1 - 1)

Tactic:
simp [RingHom.mem_ker, f_compat]

Premises used: RingHom.mem_ker
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
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)
⊢ liftFun f (x * y) = liftFun f x * liftFun f y

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Premises used: Ideal.mem_bot, TruncatedWittVector.iInf_ker_truncate, sub_eq_zero, Ideal.mem_iInf
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
⊢ ∀ (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:
simp [RingHom.mem_ker, f_compat]

Premises used: RingHom.mem_ker
-- Module: Mathlib.RingTheory.WittVector.Truncated
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_3 :
  ∀ (i : ℕ),
    Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
      (liftFun f 0 - 0)
⊢ liftFun f 0 = 0

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Premises used: Ideal.mem_bot, TruncatedWittVector.iInf_ker_truncate, sub_eq_zero, Ideal.mem_iInf
-- Module: Mathlib.RingTheory.WittVector.Truncated
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₁
⊢ ∀ (i : ℕ),
    Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
      (liftFun f 0 - 0)

Tactic:
simp [RingHom.mem_ker, f_compat]

Premises used: RingHom.mem_ker
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
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))
⊢ liftFun f (x + y) = liftFun f x + liftFun f y

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Premises used: Ideal.mem_bot, TruncatedWittVector.iInf_ker_truncate, sub_eq_zero, Ideal.mem_iInf
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
⊢ ∀ (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:
simp [RingHom.mem_ker, f_compat]

Premises used: RingHom.mem_ker
-- Module: Mathlib.RingTheory.WittVector.Truncated
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.{u_1 + 1} (α := TruncatedWittVector p n R)
    ((truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) ((lift f f_compat : (a : S) → 𝕎 R) s : 𝕎 R) :
      TruncatedWittVector p n R)
    ((f n : (a : S) → TruncatedWittVector p n R) s : TruncatedWittVector p n R)

Tactic:
truncate_liftFun _ f_compat s

Premises used: WittVector.liftFun, WittVector.truncate_liftFun
-- Module: Mathlib.RingTheory.WittVector.Truncated
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₁
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)
⊢ RingHom.comp (truncate n) (lift f f_compat) = f n

Tactic:
ext1
-- Module: Mathlib.RingTheory.WittVector.Truncated
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 : S
a :
  Eq.{u_1 + 1} (α := TruncatedWittVector p n R)
    ((truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) ((lift f f_compat : (a : S) → 𝕎 R) x : 𝕎 R) :
      TruncatedWittVector p n R)
    ((f n : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
a₁ a₂ :
  Eq.{u_1 + 1} (α := TruncatedWittVector p n R)
    ((f n : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
    ((f n : (a : S) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)
⊢ 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:
rw [RingHom.comp_apply, truncate_lift]

Premises used: WittVector.truncate_lift, RingHom.comp_apply
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p : ℕ
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₁
g : RingHom.{u_2, u_1} S (𝕎 R)
g_compat : ∀ (k : ℕ), RingHom.comp (truncate k) g = f k
a : ∀ (x : S), Eq.{u_1 + 1} (α := 𝕎 R) ((lift f f_compat : (a : S) → 𝕎 R) x : 𝕎 R) ((g : (a : S) → 𝕎 R) x : 𝕎 R)
⊢ lift f f_compat = g

Tactic:
ext1 x
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p : ℕ
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₁
g : RingHom.{u_2, u_1} S (𝕎 R)
g_compat : ∀ (k : ℕ), RingHom.comp (truncate k) g = f k
x : S
a :
  ∀ (i : ℕ),
    Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
      (HSub.hSub (α := 𝕎 R) (β := 𝕎 R) ((lift f f_compat : (a : S) → 𝕎 R) x : 𝕎 R) ((g : (a : S) → 𝕎 R) x : 𝕎 R))
⊢ Eq.{u_1 + 1} (α := 𝕎 R) ((lift f f_compat : (a : S) → 𝕎 R) x : 𝕎 R) ((g : (a : S) → 𝕎 R) x : 𝕎 R)

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]

Premises used: Ideal.mem_bot, TruncatedWittVector.iInf_ker_truncate, sub_eq_zero, Ideal.mem_iInf
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p : ℕ
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₁
g : RingHom.{u_2, u_1} S (𝕎 R)
g_compat : ∀ (k : ℕ), RingHom.comp (truncate k) g = f k
x : S
i : ℕ
⊢ Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p i R) (truncate i))
    (HSub.hSub (α := 𝕎 R) (β := 𝕎 R) ((lift f f_compat : (a : S) → 𝕎 R) x : 𝕎 R) ((g : (a : S) → 𝕎 R) x : 𝕎 R))

Tactic:
simp only [RingHom.mem_ker, g_compat, ← RingHom.comp_apply, truncate_comp_lift, map_sub, sub_self]

Premises used: WittVector.truncate_comp_lift, map_sub, sub_self, RingHom.mem_ker, RingHom.comp_apply
-- Module: Mathlib.RingTheory.WittVector.Truncated
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₁
g : RingHom.{u_2, u_1} S (𝕎 R)
k₁ : ℕ
_ :
  ∀ (k₂ : ℕ) (hk : k₁ ≤ k₂),
    Eq (α := RingHom.{u_2, u_1} S (TruncatedWittVector p k₁ R))
      (RingHom.comp (TruncatedWittVector.truncate hk) ((fun (k : ℕ) ↦ RingHom.comp (truncate k) g) k₂))
      ((fun (k : ℕ) ↦ RingHom.comp (truncate k) g) k₁)
⊢ ∀ (k₂ : ℕ) (hk : k₁ ≤ k₂),
    Eq (α := RingHom.{u_2, u_1} S (TruncatedWittVector p k₁ R))
      (RingHom.comp (TruncatedWittVector.truncate hk) ((fun (k : ℕ) ↦ RingHom.comp (truncate k) g) k₂))
      ((fun (k : ℕ) ↦ RingHom.comp (truncate k) g) k₁)

Tactic:
_
-- Module: Mathlib.RingTheory.WittVector.Truncated
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₁
g : RingHom.{u_2, u_1} S (𝕎 R)
k₁ k₂ : ℕ
h : k₁ ≤ k₂
⊢ Eq (α := RingHom.{u_2, u_1} S (TruncatedWittVector p k₁ R))
    (RingHom.comp (TruncatedWittVector.truncate h) ((fun (k : ℕ) ↦ RingHom.comp (truncate k) g) k₂))
    ((fun (k : ℕ) ↦ RingHom.comp (truncate k) g) k₁)

Tactic:
simp only [← RingHom.comp_assoc, truncate_comp_wittVector_truncate]

Premises used: RingHom.comp_assoc, TruncatedWittVector.truncate_comp_wittVector_truncate