-- Mathlib/RingTheory/WittVector/Complete.lean
theorem mem_span_p_pow_iff_le_coeff_eq_zero (x : 𝕎 k) (n : ℕ) :
    x ∈ (Ideal.span {(p ^ n : 𝕎 k)}) ↔ ∀ m, m < n → x.coeff m = 0

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ ∃ c, x = c * ↑p ^ n

Tactic:
use (frobeniusEquiv p k).symm^[n] (x.shift n)

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x = (⇑(frobeniusEquiv p k).symm)^[n] (x.shift n) * ↑p ^ n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ (⇑verschiebung)^[n] (x.shift n) =
    (⇑verschiebung)^[n] ((⇑frobenius)^[n] ((⇑(frobeniusEquiv p k).symm)^[n] (x.shift n)))

Tactic:
congr

Result:
case e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x.shift n = (⇑frobenius)^[n] ((⇑(frobeniusEquiv p k).symm)^[n] (x.shift n))

Proof state:
case e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x.shift n = (⇑frobenius)^[n] ((⇑(frobeniusEquiv p k).symm)^[n] (x.shift n))

Tactic:
rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]

Result:
case e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x.shift n = (⇑frobenius ∘ ⇑(frobeniusEquiv p k).symm)^[n] (x.shift n)

case e_a.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ Function.Commute ⇑frobenius ⇑(frobeniusEquiv p k).symm

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x = (⇑verschiebung)^[n] (x.shift n)

Tactic:
simpa using eq_iterate_verschiebung (x := x) (n := n) h

Result:
no goals

Proof state:
case e_a.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ ∀ (x : 𝕎 k), (frobeniusEquiv p k) ((frobeniusEquiv p k).symm x) = (frobeniusEquiv p k).symm ((frobeniusEquiv p k) x)

Tactic:
simp only [RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply, implies_true]

Result:
no goals

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x = (⇑(frobeniusEquiv p k).symm)^[n] (x.shift n) * ↑p ^ n

Tactic:
rw [← iterate_verschiebung_iterate_frobenius]

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x = (⇑verschiebung)^[n] ((⇑frobenius)^[n] ((⇑(frobeniusEquiv p k).symm)^[n] (x.shift n)))

Proof state:
case e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x.shift n = (⇑((frobeniusEquiv p k).symm.trans (frobeniusEquiv p k)))^[n] (x.shift n)

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
⊢ (∃ c, x = c * ↑p ^ n) ↔ ∀ m < n, x.coeff m = 0

Tactic:
refine ⟨fun ⟨u, hu⟩ m hm ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
x✝ : ∃ c, x = c * ↑p ^ n
m : ℕ
hm : m < n
u : 𝕎 k
hu : x = u * ↑p ^ n
⊢ x.coeff m = 0

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ ∃ c, x = c * ↑p ^ n

Proof state:
case e_a.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ Function.Commute ⇑frobenius ⇑(frobeniusEquiv p k).symm

Tactic:
rw [Function.Commute, Function.Semiconj, ← WittVector.frobeniusEquiv_apply]

Result:
case e_a.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ ∀ (x : 𝕎 k), (frobeniusEquiv p k) ((frobeniusEquiv p k).symm x) = (frobeniusEquiv p k).symm ((frobeniusEquiv p k) x)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
⊢ x ∈ Ideal.span {↑p ^ n} ↔ ∀ m < n, x.coeff m = 0

Tactic:
simp_rw [Ideal.mem_span_singleton, dvd_def, mul_comm]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
⊢ (∃ c, x = c * ↑p ^ n) ↔ ∀ m < n, x.coeff m = 0

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
x✝ : ∃ c, x = c * ↑p ^ n
m : ℕ
hm : m < n
u : 𝕎 k
hu : x = u * ↑p ^ n
⊢ x.coeff m = 0

Tactic:
rw [hu, mul_pow_charP_coeff_zero _ hm]

Result:
no goals

Proof state:
case e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x.shift n = (⇑frobenius ∘ ⇑(frobeniusEquiv p k).symm)^[n] (x.shift n)

Tactic:
rw [← WittVector.frobeniusEquiv_apply, ← RingEquiv.coe_trans]

Result:
case e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
h : ∀ m < n, x.coeff m = 0
⊢ x.shift n = (⇑((frobeniusEquiv p k).symm.trans (frobeniusEquiv p k)))^[n] (x.shift n)