awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u_2
inst_3 : CommRing S
f g : RingHom.{u_1, u_2} (𝕎 R) S
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
      ((g : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
n : ℕ
hn : HPow.hPow (α := S) (↑p : S) n = 0
x c : 𝕎 R
hc :
  x -
      ∑ i ∈ Finset.Iic n,
        HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) =
    HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c
rw :
  ∑ i ∈ Finset.Iic n,
      HMul.hMul (α := S)
        ((g : (a : 𝕎 R) → S)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R) :
          S)
        (HPow.hPow (α := S) (↑p : S) i) =
    HAdd.hAdd (α := S) (β := S) ((g : (a : 𝕎 R) → S) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c) : S)
      ((g : (a : 𝕎 R) → S)
          (∑ i ∈ Finset.Iic n,
            HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)
⊢ ∑ i ∈ Finset.Iic n,
      HMul.hMul (α := S)
        ((g : (a : 𝕎 R) → S)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R) :
          S)
        (HPow.hPow (α := S) (↑p : S) i) =
    HAdd.hAdd (α := S) (β := S)
      ((g : (a : 𝕎 R) → S)
          (x -
            ∑ i ∈ Finset.Iic n,
              HMul.hMul (α := 𝕎 R)
                ((teichmuller p : (a : R) → 𝕎 R)
                    ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R)
                        (x.coeff i) :
                      R) :
                  𝕎 R)
                (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)
      ((g : (a : 𝕎 R) → S)
          (∑ i ∈ Finset.Iic n,
            HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)

Tactic:
rw [hc]
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u_2
inst_3 : CommRing S
f g : RingHom.{u_1, u_2} (𝕎 R) S
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
      ((g : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
n : ℕ
hn : HPow.hPow (α := S) (↑p : S) n = 0
x c : 𝕎 R
hc :
  x -
      ∑ i ∈ Finset.Iic n,
        HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) =
    HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c
⊢ ∑ i ∈ Finset.Iic n,
      HMul.hMul (α := S)
        ((g : (a : 𝕎 R) → S)
            ((teichmuller p : (a : R) → 𝕎 R)
                ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                  R) :
              𝕎 R) :
          S)
        (HPow.hPow (α := S) (↑p : S) i) =
    HAdd.hAdd (α := S) (β := S) ((g : (a : 𝕎 R) → S) (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c) : S)
      ((g : (a : 𝕎 R) → S)
          (∑ i ∈ Finset.Iic n,
            HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)

Tactic:
simp [pow_succ, hn]

Premises used: pow_succ
-- Module: Mathlib.RingTheory.WittVector.TeichmullerSeries
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst : CommRing R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u_2
inst_3 : CommRing S
f g : RingHom.{u_1, u_2} (𝕎 R) S
h :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S) ((f : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
      ((g : (a : 𝕎 R) → S) ((teichmuller p : (a : R) → 𝕎 R) x : 𝕎 R) : S)
n : ℕ
hn : HPow.hPow (α := S) (↑p : S) n = 0
x c : 𝕎 R
hc :
  x -
      ∑ i ∈ Finset.Iic n,
        HMul.hMul (α := 𝕎 R)
          ((teichmuller p : (a : R) → 𝕎 R)
              ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                R) :
            𝕎 R)
          (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i) =
    HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1) * c
⊢ HAdd.hAdd (α := S) (β := S)
      ((g : (a : 𝕎 R) → S)
          (x -
            ∑ i ∈ Finset.Iic n,
              HMul.hMul (α := 𝕎 R)
                ((teichmuller p : (a : R) → 𝕎 R)
                    ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R)
                        (x.coeff i) :
                      R) :
                  𝕎 R)
                (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S)
      ((g : (a : 𝕎 R) → S)
          (∑ i ∈ Finset.Iic n,
            HMul.hMul (α := 𝕎 R)
              ((teichmuller p : (a : R) → 𝕎 R)
                  ((HPow.hPow (α := R ≃+* R) (RingEquiv.symm (_root_.frobeniusEquiv R p)) i : (a : R) → R) (x.coeff i) :
                    R) :
                𝕎 R)
              (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) i)) :
        S) =
    (g : (a : 𝕎 R) → S) x

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
x y : TruncatedWittVector p n R
h : ∀ (i : Fin n), coeff i x = coeff i y
⊢ x = y

Tactic:
funext h

Premises used: funext, TruncatedWittVector
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
x : Fin n → R
i : Fin n
⊢ coeff i (mk p x) = x i

Tactic:
rfl

Premises used: TruncatedWittVector.coeff, rfl, TruncatedWittVector.mk
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
h : ∀ (i : Fin n), coeff i (mk p fun (i : Fin n) ↦ coeff i x) = coeff i x
⊢ (mk p fun (i : Fin n) ↦ coeff i x) = x

Tactic:
ext i
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
i : Fin n
h h₁ : coeff i x = coeff i x
⊢ coeff i (mk p fun (i : Fin n) ↦ coeff i x) = coeff i x

Tactic:
rw [coeff_mk]

Premises used: TruncatedWittVector.coeff_mk
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : TruncatedWittVector p n R
i : Fin n
rw :
  WittVector.coeff (p := p) { coeff := fun (i : ℕ) ↦ if h : i < n then coeff (⟨i, h⟩ : Fin n) x else 0 } (↑i : ℕ) =
    coeff i x
⊢ x.out.coeff (↑i : ℕ) = coeff i x

Tactic:
rw [out]

Premises used: TruncatedWittVector.out
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : TruncatedWittVector p n R
i : Fin n
dsimp : (if h : (↑i : ℕ) < n then coeff (⟨(↑i : ℕ), h⟩ : Fin n) x else 0) = coeff i x
⊢ WittVector.coeff (p := p) { coeff := fun (i : ℕ) ↦ if h : i < n then coeff (⟨i, h⟩ : Fin n) x else 0 } (↑i : ℕ) =
    coeff i x

Tactic:
dsimp only
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : TruncatedWittVector p n R
i : Fin n
rw : coeff (⟨(↑i : ℕ), ⋯⟩ : Fin n) x = coeff i x
rw₁ rw₂ : coeff i x = coeff i x
⊢ (if h : (↑i : ℕ) < n then coeff (⟨(↑i : ℕ), h⟩ : Fin n) x else 0) = coeff i x

Tactic:
rw [dif_pos i.is_lt, Fin.eta]

Premises used: dif_pos, Fin.is_lt, Fin.eta
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x y : TruncatedWittVector p n R
h : x.out = y.out
h₁ : ∀ (i : Fin n), coeff i x = coeff i y
⊢ x = y

Tactic:
ext i
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x y : TruncatedWittVector p n R
h : x.out = y.out
i : Fin n
h₁ : ∀ (h : ∀ (n_1 : ℕ), x.out.coeff n_1 = y.out.coeff n_1) (i : Fin n), coeff i x = coeff i y
⊢ coeff i x = coeff i y

Tactic:
rw [WittVector.ext_iff] at h

Premises used: WittVector.ext_iff
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x y : TruncatedWittVector p n R
h : ∀ (n_1 : ℕ), x.out.coeff n_1 = y.out.coeff n_1
i : Fin n
⊢ coeff i x = coeff i y

Tactic:
simpa only [coeff_out] using h ↑i

Premises used: TruncatedWittVector.coeff_out, Fin.val
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
x : 𝕎 R
i : Fin n
rw : TruncatedWittVector.coeff i (TruncatedWittVector.mk p fun (i : Fin n) ↦ x.coeff (↑i : ℕ)) = x.coeff (↑i : ℕ)
rw₁ rw₂ : x.coeff (↑i : ℕ) = x.coeff (↑i : ℕ)
⊢ TruncatedWittVector.coeff i (truncateFun n x) = x.coeff (↑i : ℕ)

Tactic:
rw [truncateFun, TruncatedWittVector.coeff_mk]

Premises used: TruncatedWittVector.coeff_mk, WittVector.truncateFun
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
h : ∀ (i : ℕ), (truncateFun n x).out.coeff i = (init n x).coeff i
⊢ (truncateFun n x).out = init n x

Tactic:
ext i
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
i : ℕ
h :
  (if h : i < n then TruncatedWittVector.coeff (⟨i, h⟩ : Fin n) (truncateFun n x) else 0) =
    if i < n then x.coeff i else 0
⊢ (truncateFun n x).out.coeff i = (init n x).coeff i

Tactic:
dsimp [TruncatedWittVector.out, init, select, coeff_mk]

Premises used: WittVector.select, WittVector.init, WittVector.coeff_mk, TruncatedWittVector.out
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
i : ℕ
pos : ∀ (hi : i < n), TruncatedWittVector.coeff (⟨i, hi⟩ : Fin n) (truncateFun n x) = x.coeff i
neg : ∀ (hi : ¬i < n), Eq.{u_1 + 1} (α := R) 0 0
⊢ (if h : i < n then TruncatedWittVector.coeff (⟨i, h⟩ : Fin n) (truncateFun n x) else 0) =
    if i < n then x.coeff i else 0

Tactic:
split_ifs with hi
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
i : ℕ
hi : ¬i < n
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
pos : x.coeff (↑(⟨i, hi⟩ : Fin n) : ℕ) = x.coeff i
pos₁ pos₂ : x.coeff i = x.coeff i
⊢ TruncatedWittVector.coeff (⟨i, hi⟩ : Fin n) (truncateFun n x) = x.coeff i

Tactic:
rw [coeff_truncateFun, Fin.val_mk]

Premises used: Fin.val_mk, WittVector.coeff_truncateFun
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
x : TruncatedWittVector p n R
⊢ WittVector.truncateFun n x.out = x

Tactic:
simp only [WittVector.truncateFun, coeff_out, mk_coeff]

Premises used: TruncatedWittVector.coeff_out, TruncatedWittVector.mk_coeff, WittVector.truncateFun
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
i : Fin n
change : Eq.{u_1 + 1} (α := R) (coeff (p := p) i (truncateFun n 0)) 0
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) i 0) 0

Tactic:
change coeff i (truncateFun _ 0 : TruncatedWittVector p n R) = 0

Premises used: TruncatedWittVector.coeff, WittVector.truncateFun, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
i : Fin n
rw : Eq.{u_1 + 1} (α := R) (WittVector.coeff (p := p) 0 (↑i : ℕ)) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) (coeff (p := p) i (truncateFun n 0)) 0

Tactic:
rw [coeff_truncateFun, WittVector.zero_coeff]

Premises used: WittVector.coeff_truncateFun, WittVector.zero_coeff
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := 𝕎 R) (truncateFun n)

Tactic:
Function.RightInverse.surjective TruncatedWittVector.truncateFun_out

Premises used: TruncatedWittVector.truncateFun_out, Function.RightInverse.surjective
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
⊢ Eq.{u_1 + 1} (α := TruncatedWittVector p n R) (truncateFun n 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
⊢ Eq.{u_1 + 1} (α := TruncatedWittVector p n R) (truncateFun n 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
a₂ a₃ : init n (x + y) = init n (init n x + init n y)
⊢ truncateFun n (x + y) = truncateFun n x + truncateFun n y

Tactic:
witt_truncateFun_tac
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
a₂ a₃ : init n (x * y) = init n (init n x * init n y)
⊢ truncateFun n (x * y) = truncateFun n x * truncateFun n y

Tactic:
witt_truncateFun_tac
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
a₂ a₃ : init n (-x) = init n (-init n x)
⊢ truncateFun n (-x) = -truncateFun n x

Tactic:
witt_truncateFun_tac
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
a₂ a₃ : init n (x - y) = init n (init n x - init n y)
⊢ truncateFun n (x - y) = truncateFun n x - truncateFun n y

Tactic:
witt_truncateFun_tac
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
a₂ a₃ : init n (m • x) = init n (m • init n x)
⊢ truncateFun n (m • x) = m • truncateFun n x

Tactic:
witt_truncateFun_tac
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
a₂ a₃ : init n (m • x) = init n (m • init n x)
⊢ truncateFun n (m • x) = m • truncateFun n x

Tactic:
witt_truncateFun_tac
-- Module: Mathlib.RingTheory.WittVector.Truncated
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
a₂ a₃ : init n (x ^ m) = init n (init n x ^ m)
⊢ truncateFun n (x ^ m) = truncateFun n x ^ m

Tactic:
witt_truncateFun_tac
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
⊢ Eq.{u_1 + 1} (α := TruncatedWittVector p n R) (truncateFun n (↑m : 𝕎 R)) (↑m : TruncatedWittVector p n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℤ
⊢ Eq.{u_1 + 1} (α := TruncatedWittVector p n R) (truncateFun n (↑m : 𝕎 R)) (↑m : TruncatedWittVector p n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := 𝕎 R) (β := TruncatedWittVector p n R)
    (⇑(truncate n) : (a : 𝕎 R) → TruncatedWittVector p n R)

Tactic:
truncateFun_surjective p n R

Premises used: WittVector.truncateFun_surjective, WittVector.truncateFun, TruncatedWittVector.mk
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
i : Fin n
⊢ TruncatedWittVector.coeff (p := p) i ((truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) x) = x.coeff (↑i : ℕ)

Tactic:
coeff_truncateFun _ _

Premises used: TruncatedWittVector.coeff, WittVector.coeff_truncateFun, WittVector.truncateFun, TruncatedWittVector.mk
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
simp :
  (∀ (i : Fin n),
      Eq.{u_1 + 1} (α := R)
        (TruncatedWittVector.coeff (p := p) i
          (({ toFun := truncateFun n, map_one' := ⋯, map_mul' := ⋯ } : (a : 𝕎 R) → TruncatedWittVector p n R) x))
        0) ↔
    ∀ i < n, x.coeff i = 0
⊢ Membership.mem (γ := Ideal (𝕎 R)) (RingHom.ker (F := 𝕎 R →+* TruncatedWittVector p n R) (truncate n)) x ↔
    ∀ i < n, x.coeff i = 0

Tactic:
simp only [RingHom.mem_ker, truncate, RingHom.coe_mk, TruncatedWittVector.ext_iff,
    coeff_zero]

Premises used: RingHom.mem_ker, TruncatedWittVector.coeff_zero, WittVector.truncate, TruncatedWittVector.ext_iff, RingHom.coe_mk
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
⊢ (∀ (i : Fin n),
      Eq.{u_1 + 1} (α := R)
        (TruncatedWittVector.coeff (p := p) i
          (({ toFun := truncateFun n, map_one' := ⋯, map_mul' := ⋯ } : (a : 𝕎 R) → TruncatedWittVector p n R) x))
        0) ↔
    ∀ i < n, x.coeff i = 0

Tactic:
Fin.forall_iff

Premises used: TruncatedWittVector.coeff, Fin.forall_iff, WittVector.truncateFun, TruncatedWittVector.mk
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
⊢ (∀ (i : Fin n),
      Eq.{u_1 + 1} (α := R)
        (TruncatedWittVector.coeff (p := p) i
          (({ toFun := truncateFun n, map_one' := ⋯, map_mul' := ⋯ } : (a : 𝕎 R) → TruncatedWittVector p n R) x))
        0) ↔
    ∀ i < n, x.coeff i = 0

Tactic:
exact Fin.forall_iff

Premises used: Fin.forall_iff
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
f : ℕ → R
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 : ℕ)))
⊢ 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)

Tactic:
ext i
-- Module: Mathlib.RingTheory.WittVector.Truncated
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
f : ℕ → R
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:
simp only [coeff_truncate, TruncatedWittVector.coeff_mk]

Premises used: WittVector.coeff_truncate, TruncatedWittVector.coeff_mk
-- 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
simp : (∀ i < m, x.coeff i = 0) → ∀ i < n, x.coeff i = 0
⊢ 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

Tactic:
simp only [WittVector.mem_ker_truncate]

Premises used: WittVector.mem_ker_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
x : 𝕎 R
h : ∀ i < m, x.coeff i = 0
i : ℕ
hi : i < n
⊢ x.coeff i = 0

Tactic:
h i (lt_of_lt_of_le hi hm)

Premises used: lt_of_lt_of_le
-- 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
h : ∀ i < m, x.coeff i = 0
i : ℕ
hi : i < n
⊢ x.coeff i = 0

Tactic:
exact h i (lt_of_lt_of_le hi hm)

Premises used: lt_of_lt_of_le
-- 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
⊢ Eq.{u_1 + 1} (α := 𝕎 R →+* TruncatedWittVector p n R) (RingHom.comp (truncate hm) (WittVector.truncate m))
    (WittVector.truncate n)

Tactic:
RingHom.liftOfRightInverse_comp _ _ _ _

Premises used: WittVector.truncate, TruncatedWittVector.truncate, RingHom.liftOfRightInverse_comp
-- 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
⊢ Eq (α := TruncatedWittVector p n R)
    ((truncate hm : (a : TruncatedWittVector p m R) → TruncatedWittVector p n R)
        ((WittVector.truncate m : (a : 𝕎 R) → TruncatedWittVector p m R) x : TruncatedWittVector p m R) :
      TruncatedWittVector p n R)
    ((WittVector.truncate n : (a : 𝕎 R) → TruncatedWittVector p n R) x : TruncatedWittVector p n R)

Tactic:
RingHom.liftOfRightInverse_comp_apply _ _ _ _ _

Premises used: RingHom.liftOfRightInverse_comp_apply
-- 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
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 ⋯ : (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)
⊢ 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)

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

Premises used: WittVector.truncate_surjective, rfl