awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
by_contra! : ∀ (hall : ∀ (k : ℕ), x.coeff k = 0), False
⊢ ∃ (k : ℕ), x.coeff k ≠ 0

Tactic:
by_contra! hall
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), x.coeff k = 0
apply : x = 0
⊢ False

Tactic:
apply hx
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), x.coeff k = 0
h : ∀ (i : ℕ), x.coeff i = coeff (p := p) 0 i
⊢ x = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), x.coeff k = 0
i : ℕ
⊢ x.coeff i = coeff (p := p) 0 i

Tactic:
simp only [hall, zero_coeff]

Premises used: WittVector.zero_coeff
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ (k : ℕ), x.coeff k ≠ 0

Tactic:
have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
    by_contra! hall
    apply hx
    ext i
    simp only [hall, zero_coeff]
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ (k : ℕ), x.coeff k ≠ 0
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex
h : (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)
⊢ ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'

Tactic:
use n, x.shift n

Premises used: WittVector.shift
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ (k : ℕ), x.coeff k ≠ 0
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex
⊢ (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)

Tactic:
⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩

Premises used: WittVector.eq_iterate_verschiebung, Classical.not_not, And.intro, Iff.mp, Nat.find_spec
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ (k : ℕ), x.coeff k ≠ 0
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex
h : ∀ (i : ℕ) (hi : i < n), ¬¬x.coeff i = 0
⊢ (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)

Tactic:
refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ (k : ℕ), x.coeff k ≠ 0
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex
i : ℕ
hi : i < n
⊢ ¬¬x.coeff i = 0

Tactic:
Nat.find_min hex hi

Premises used: Nat.find_min
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ (k : ℕ), x.coeff k ≠ 0
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex
i : ℕ
hi : i < n
⊢ ¬¬x.coeff i = 0

Tactic:
exact Nat.find_min hex hi

Premises used: Nat.find_min
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
hx : x ≠ 0
have : ∃ (k : ℕ), x.coeff k ≠ 0
have₁ :
  ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
    ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
have₂ : ∃ (k : ℕ), x.coeff k ≠ 0
have₃ have₄ have₅ :
  ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
    ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'
h :
  ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
    let n := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex;
    (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] (x.shift n)
h₁ :
  ∀ (hex : ∃ (k : ℕ), x.coeff k ≠ 0),
    let n := Nat.find (p := fun (n : ℕ) ↦ x.coeff n ≠ 0) hex;
    ∀ (i : ℕ) (hi : i < n), ¬¬x.coeff i = 0
⊢ ∃ (n : ℕ) (x' : 𝕎 R), x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] x'

Tactic:
classical
  have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
    by_contra! hall
    apply hx
    ext i
    simp only [hall, zero_coeff]
  let n := Nat.find hex
  use n, x.shift n
  refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩
  exact Nat.find_min hex hi
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
x y : 𝕎 R
contrapose! : x ≠ 0 ∧ y ≠ 0 → x * y ≠ 0
⊢ x * y = 0 → x = 0 ∨ y = 0

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
x y : 𝕎 R
ha : x ≠ 0
hb : y ≠ 0
rcases :
  ∀ (na : ℕ) (wa : 𝕎 R) (hwa0 : wa.coeff 0 ≠ 0) (ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0),
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * y ≠ 0
⊢ x * y ≠ 0

Tactic:
rcases verschiebung_nonzero ha with ⟨na, wa, hwa0, rfl⟩

Premises used: WittVector.verschiebung_nonzero, rfl
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
y : 𝕎 R
hb : y ≠ 0
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0
rcases :
  ∀ (nb : ℕ) (wb : 𝕎 R) (hwb0 : wb.coeff 0 ≠ 0) (hb : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0),
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * y ≠ 0

Tactic:
rcases verschiebung_nonzero hb with ⟨nb, wb, hwb0, rfl⟩

Premises used: WittVector.verschiebung_nonzero, rfl
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0

Tactic:
ne_of_apply_ne (fun x => x.coeff (na + nb)) ?_

Premises used: ne_of_apply_ne
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0
refine :
  Ne.{u_1 + 1} (α := R)
    ((fun (x : 𝕎 R) ↦ x.coeff (na + nb))
      ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb))
    ((fun (x : 𝕎 R) ↦ x.coeff (na + nb)) 0)
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0

Tactic:
refine ne_of_apply_ne (fun x => x.coeff (na + nb)) ?_

Premises used: ne_of_apply_ne
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0
rw : wa.coeff 0 ^ p ^ nb * wb.coeff 0 ^ p ^ na ≠ 0
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb).coeff (na + nb) ≠
    coeff (p := p) 0 (na + nb)

Tactic:
rw [iterate_verschiebung_mul_coeff, zero_coeff]

Premises used: WittVector.zero_coeff, WittVector.iterate_verschiebung_mul_coeff
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0
⊢ wa.coeff 0 ^ p ^ nb * wb.coeff 0 ^ p ^ na ≠ 0

Tactic:
mul_ne_zero (pow_ne_zero _ hwa0) (pow_ne_zero _ hwb0)

Premises used: pow_ne_zero, mul_ne_zero
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
na : ℕ
wa : 𝕎 R
hwa0 : wa.coeff 0 ≠ 0
ha : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[na] wa ≠ 0
nb : ℕ
wb : 𝕎 R
hwb0 : wb.coeff 0 ≠ 0
hb : (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[nb] wb ≠ 0
⊢ wa.coeff 0 ^ p ^ nb * wb.coeff 0 ^ p ^ na ≠ 0

Tactic:
exact mul_ne_zero (pow_ne_zero _ hwa0) (pow_ne_zero _ hwb0)

Premises used: pow_ne_zero, mul_ne_zero
-- Module: Mathlib.RingTheory.WittVector.Domain
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
inst_2 : IsDomain R
⊢ IsDomain.{u_1} (𝕎 R)

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
        ((bind₁ (xInTermsOfW p ℚ) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (wittPolynomial p ℚ n)) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
rw₁ :
  Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (X n) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)
rw₂ : Eq (α := MvPolynomial ℕ ℚ) ((wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) n) (wittPolynomial p ℚ (n + 1))
rw₃ rw₄ : Eq (α := MvPolynomial ℕ ℚ) (wittPolynomial p ℚ (n + 1)) (wittPolynomial p ℚ (n + 1))
⊢ Eq (α := MvPolynomial ℕ ℚ)
    ((bind₁ fun (n : ℕ) ↦
            (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
              (xInTermsOfW p ℚ n) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
        (wittPolynomial p ℚ n) :
      MvPolynomial ℕ ℚ)
    (wittPolynomial p ℚ (n + 1) : MvPolynomial ℕ ℚ)

Tactic:
rw [← bind₁_bind₁, bind₁_xInTermsOfW_wittPolynomial, bind₁_X_right, Function.comp_apply]

Premises used: bind₁_xInTermsOfW_wittPolynomial, MvPolynomial.bind₁_bind₁, Function.comp_apply, MvPolynomial.bind₁_X_right
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p n : ℕ
rw :
  HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
      (∑ i : Fin n,
        have x := ⋯;
        ∑ j ∈ range (p ^ (n - (↑i : ℕ))),
          HPow.hPow (α := MvPolynomial ℕ ℤ) (X (↑i : ℕ)) p ^ (p ^ (n - (↑i : ℕ)) - (j + 1)) *
              frobeniusPolyAux p (↑i : ℕ) ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - (↑i : ℕ))).choose (j + 1) / p ^ (n - (↑i : ℕ) - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) =
    HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
      (∑ i ∈ range n,
        ∑ j ∈ range (p ^ (n - i)),
          HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ))
rw₁ rw₂ :
  HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
      (∑ i : Fin n,
        have x := ⋯;
        ∑ j ∈ range (p ^ (n - (↑i : ℕ))),
          HPow.hPow (α := MvPolynomial ℕ ℤ) (X (↑i : ℕ)) p ^ (p ^ (n - (↑i : ℕ)) - (j + 1)) *
              frobeniusPolyAux p (↑i : ℕ) ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - (↑i : ℕ))).choose (j + 1) / p ^ (n - (↑i : ℕ) - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) =
    HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
      (∑ i : Fin n,
        ∑ j ∈ range (p ^ (n - (↑i : ℕ))),
          HPow.hPow (α := MvPolynomial ℕ ℤ) (X (↑i : ℕ)) p ^ (p ^ (n - (↑i : ℕ)) - (j + 1)) *
              frobeniusPolyAux p (↑i : ℕ) ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - (↑i : ℕ))).choose (j + 1) / p ^ (n - (↑i : ℕ) - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ))
⊢ frobeniusPolyAux p n =
    HSub.hSub (α := MvPolynomial ℕ ℤ) (X (n + 1))
      (∑ i ∈ range n,
        ∑ j ∈ range (p ^ (n - i)),
          HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ))

Tactic:
rw [frobeniusPolyAux, ← Fin.sum_univ_eq_sum_range]

Premises used: Fin.sum_univ_eq_sum_range, WittVector.frobeniusPolyAux
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n j : ℕ
hj : j < p ^ n
hk : (↑(n - v p (j + 1)) : ℕ∞) ≤ emultiplicity p ((p ^ n).choose (j + 1))
⊢ p ^ (n - v p (j + 1)) ∣ (p ^ n).choose (j + 1)

Tactic:
apply pow_dvd_of_le_emultiplicity

Premises used: pow_dvd_of_le_emultiplicity
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n j : ℕ
hj : j < p ^ n
hk hk₁ : LE.le (α := ℕ∞) (↑(n - v p (j + 1)) : ℕ∞) (↑(n - v p (j + 1)) : ℕ∞)
⊢ (↑(n - v p (j + 1)) : ℕ∞) ≤ emultiplicity p ((p ^ n).choose (j + 1))

Tactic:
rw [hp.out.emultiplicity_choose_prime_pow hj j.succ_ne_zero]

Premises used: Nat.Prime.emultiplicity_choose_prime_pow, Nat.succ_ne_zero, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
generalize : ∀ (m : ℕ) (h : v p (j + 1) = m), j - m + n = i + j + (n - i - m)
⊢ j - v p (j + 1) + n = i + j + (n - i - v p (j + 1))

Tactic:
generalize h : v p (j + 1) = m

Premises used: multiplicity, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
rsuffices : ∀ (h₁ : m ≤ n - i) (h₂ : m ≤ j), j - m + n = i + j + (n - i - m)
rsuffices₁ : m ≤ n - i ∧ m ≤ j
⊢ j - m + n = i + j + (n - i - m)

Tactic:
rsuffices ⟨h₁, h₂⟩ : m ≤ n - i ∧ m ≤ j
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
rw : j + n - m = i + j + (n - i - m)
rw₁ : j + n - m = j + i + (n - i - m)
rw₂ : j + (n - m) = j + i + (n - i - m)
rw₃ : j + (n - m) = j + (i + (n - i - m))
rw₄ : j + (n - m) = j + (i + (n - m - i))
rw₅ : j + (n - m) = j + (n - m - i + i)
rw₆ rw₇ : j + (n - m) = j + (n - m)
⊢ j - m + n = i + j + (n - i - m)

Tactic:
rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)),
      add_assoc, tsub_right_comm, add_comm i,
      tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]

Premises used: add_tsub_assoc_of_le, add_assoc, tsub_right_comm, tsub_add_cancel_of_le, Nat.sub_le, le_tsub_iff_left, add_comm, tsub_add_eq_add_tsub, Iff.mp, le_tsub_of_add_le_right, LE.le.trans
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
⊢ p ^ m ≤ j + 1

Tactic:
have hle : p ^ m ≤ j + 1 := h ▸ Nat.le_of_dvd j.succ_pos (pow_multiplicity_dvd _ _)
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
hle : p ^ m ≤ j + 1
⊢ m ≤ n - i ∧ m ≤ j

Tactic:
⟨(Nat.pow_le_pow_iff_right hp.1.one_lt).1 (hle.trans hj),
     Nat.le_of_lt_succ ((m.lt_pow_self hp.1.one_lt).trans_le hle)⟩

Premises used: Nat.lt_pow_self, Nat.Prime.one_lt, LT.lt.trans_le, Nat.le_of_lt_succ, And.intro, Iff.mp, Nat.pow_le_pow_iff_right, LE.le.trans, Fact.out
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
hle : p ^ m ≤ j + 1
⊢ m ≤ n - i ∧ m ≤ j

Tactic:
exact ⟨(Nat.pow_le_pow_iff_right hp.1.one_lt).1 (hle.trans hj),
     Nat.le_of_lt_succ ((m.lt_pow_self hp.1.one_lt).trans_le hle)⟩
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw :
  HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
⊢ (MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPoly p n) =
    frobeniusPolyRat p n

Tactic:
rw [frobeniusPoly, map_add, map_mul, map_pow, map_C, map_X, eq_intCast, Int.cast_natCast,
    frobeniusPolyRat]

Premises used: Int.cast_natCast, map_add, eq_intCast, map_pow, WittVector.frobeniusPolyRat, map_mul, MvPolynomial.map_C, MvPolynomial.map_X, WittVector.frobeniusPoly
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)

Tactic:
Nat.strong_induction_on n ?_

Premises used: Nat.strong_induction_on
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine :
  ∀ (n : ℕ),
    (∀ m < n,
        HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
            HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
              ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                  (frobeniusPolyAux p m) :
                MvPolynomial ℕ ℚ) =
          (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
            (xInTermsOfW p ℚ m)) →
      HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
          HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
            ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
              MvPolynomial ℕ ℚ) =
        (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
          (xInTermsOfW p ℚ n)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)

Tactic:
refine Nat.strong_induction_on n ?_
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
rw :
  HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
      (HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ))
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)

Tactic:
rw [xInTermsOfW_eq]

Premises used: xInTermsOfW_eq
-- Module: Mathlib.RingTheory.WittVector.Frobenius
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
simp :
  HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    HMul.hMul (β := MvPolynomial ℕ ℚ)
      (HSub.hSub (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (X n) :
          MvPolynomial ℕ ℚ)
        (∑ x ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) x) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ)
                ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
                    (xInTermsOfW p ℚ x) :
                  MvPolynomial ℕ ℚ)
                (p ^ (n - x))) :
          MvPolynomial ℕ ℚ))
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
          (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
        MvPolynomial ℕ ℚ)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
      (HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ))

Tactic:
simp only [map_sum, map_sub, map_mul, map_pow (bind₁ _), bind₁_C_right]

Premises used: map_sub, MvPolynomial.bind₁_C_right, map_pow, map_sum, MvPolynomial.bind₁, map_mul