-- Mathlib/RingTheory/Perfectoid/Untilt.lean
lemma pow_dvd_untiltAux_sub_untiltAux (x : PreTilt O p) {m n : ℕ} (h : m ≤ n) :
    (p : O) ^ m ∣ x.untiltAux m - x.untiltAux n

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
h : m + 1 ≤ n
n' : ℕ := n.pred
⊢ ↑p ^ (m + 1) ∣ x.untiltAux (m + 1) - x.untiltAux n

Tactic:
have : n = n' + 1 := by simp [n', Nat.sub_add_cancel (n := n) (m := 1) (by linarith)]

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
h : m + 1 ≤ n
n' : ℕ := n.pred
this : n = n' + 1
⊢ ↑p ^ (m + 1) ∣ x.untiltAux (m + 1) - x.untiltAux n

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
h : m + 1 ≤ n
n' : ℕ := n.pred
this : n = n' + 1
⊢ ↑p ^ (m + 1) ∣ x.untiltAux (m + 1) - x.untiltAux n

Tactic:
simp only [this, add_le_add_iff_right, untiltAux] at h ⊢

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ ↑p ^ (m + 1) ∣ Quotient.out ((coeff (ModP O p) p m) x) ^ p ^ m - Quotient.out ((coeff (ModP O p) p n') x) ^ p ^ n'

Proof state:
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
h : m + 1 ≤ n
n' : ℕ := n.pred
⊢ 1 ≤ n

Tactic:
linarith

Result:
no goals

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ (coeff (ModP O p) p m) x = (coeff (ModP O p) p n') x ^ p ^ (n' - m)

Tactic:
calc
  _ = (coeff (ModP O p) p (n' - (n' - m))) x := by simp [Nat.sub_sub_self h]
  _ = (coeff (ModP O p) p n') (((frobenius (Ring.Perfection (ModP O p) p) p))^[n' - m] x) :=
    (coeff_iterate_frobenius' x n' (n' - m) (Nat.sub_le n' m)).symm
  _ = _ := by simp [iterate_frobenius]

Result:
no goals

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ (Ideal.Quotient.mk (span {↑p})) (Quotient.out ((coeff (ModP O p) p m) x)) =
    (Ideal.Quotient.mk (span {↑p})) (Quotient.out ((coeff (ModP O p) p (n' - m + m)) x) ^ p ^ (n' - m))

Tactic:
simp only [Ideal.Quotient.mk_out, map_pow, Nat.sub_add_cancel h]

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ (coeff (ModP O p) p m) x = (coeff (ModP O p) p n') x ^ p ^ (n' - m)

Proof state:
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
m n : ℕ
h : m ≤ n
⊢ ↑p ^ m ∣ x.untiltAux m - x.untiltAux n

Tactic:
cases m with
| zero => simp [untiltAux]
| succ m =>
  let n' := n.pred
  have : n = n' + 1 := by simp [n', Nat.sub_add_cancel (n := n) (m := 1) (by linarith)]
  simp only [this, add_le_add_iff_right, untiltAux] at h ⊢
  rw [← Nat.sub_add_cancel h, pow_add _ _ m, pow_mul]
  refine (dvd_sub_pow_of_dvd_sub ?_ m)
  rw [← mem_span_singleton, ← Ideal.Quotient.eq]
  simp only [Ideal.Quotient.mk_out, map_pow, Nat.sub_add_cancel h]
  calc
    _ = (coeff (ModP O p) p (n' - (n' - m))) x := by simp [Nat.sub_sub_self h]
    _ = (coeff (ModP O p) p n') (((frobenius (Ring.Perfection (ModP O p) p) p))^[n' - m] x) :=
      (coeff_iterate_frobenius' x n' (n' - m) (Nat.sub_le n' m)).symm
    _ = _ := by simp [iterate_frobenius]

Result:
no goals

Proof state:
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ (coeff (ModP O p) p n') ((⇑(frobenius (Ring.Perfection (ModP O p) p) p))^[n' - m] x) =
    (coeff (ModP O p) p n') x ^ p ^ (n' - m)

Tactic:
simp [iterate_frobenius]

Result:
no goals

Proof state:
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ (coeff (ModP O p) p m) x = (coeff (ModP O p) p (n' - (n' - m))) x

Tactic:
simp [Nat.sub_sub_self h]

Result:
no goals

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ ↑p ∣ Quotient.out ((coeff (ModP O p) p m) x) - Quotient.out ((coeff (ModP O p) p (n' - m + m)) x) ^ p ^ (n' - m)

Tactic:
rw [← mem_span_singleton, ← Ideal.Quotient.eq]

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ (Ideal.Quotient.mk (span {↑p})) (Quotient.out ((coeff (ModP O p) p m) x)) =
    (Ideal.Quotient.mk (span {↑p})) (Quotient.out ((coeff (ModP O p) p (n' - m + m)) x) ^ p ^ (n' - m))

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ ↑p ^ (m + 1) ∣ Quotient.out ((coeff (ModP O p) p m) x) ^ p ^ m - Quotient.out ((coeff (ModP O p) p n') x) ^ p ^ n'

Tactic:
rw [← Nat.sub_add_cancel h, pow_add _ _ m, pow_mul]

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ ↑p ^ (m + 1) ∣
    Quotient.out ((coeff (ModP O p) p m) x) ^ p ^ m -
      (Quotient.out ((coeff (ModP O p) p (n' - m + m)) x) ^ p ^ (n' - m)) ^ p ^ m

Proof state:
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
h : m + 1 ≤ n
n' : ℕ := n.pred
⊢ n = n' + 1

Tactic:
simp [n', Nat.sub_add_cancel (n := n) (m := 1) (by linarith)]

Result:
no goals

Proof state:
case zero
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n : ℕ
h : 0 ≤ n
⊢ ↑p ^ 0 ∣ x.untiltAux 0 - x.untiltAux n

Tactic:
simp [untiltAux]

Result:
no goals

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ ↑p ^ (m + 1) ∣
    Quotient.out ((coeff (ModP O p) p m) x) ^ p ^ m -
      (Quotient.out ((coeff (ModP O p) p (n' - m + m)) x) ^ p ^ (n' - m)) ^ p ^ m

Tactic:
refine (dvd_sub_pow_of_dvd_sub ?_ m)

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
n' : ℕ := n.pred
this : n = n' + 1
h : m ≤ n'
⊢ ↑p ∣ Quotient.out ((coeff (ModP O p) p m) x) - Quotient.out ((coeff (ModP O p) p (n' - m + m)) x) ^ p ^ (n' - m)

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
h : m + 1 ≤ n
⊢ ↑p ^ (m + 1) ∣ x.untiltAux (m + 1) - x.untiltAux n

Tactic:
let n' := n.pred

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x : PreTilt O p
n m : ℕ
h : m + 1 ≤ n
n' : ℕ := n.pred
⊢ ↑p ^ (m + 1) ∣ x.untiltAux (m + 1) - x.untiltAux n