-- Mathlib/RingTheory/Perfectoid/Untilt.lean
lemma pow_dvd_mul_untiltAux_sub_untiltAux_mul (x y : PreTilt O p) (m : ℕ) :
    (p : O) ^ m ∣ (x * y).untiltAux m - (x.untiltAux m) * (y.untiltAux m)

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

Tactic:
simp only [untiltAux, _root_.map_mul, ← mul_pow]

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

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x y : PreTilt O p
m : ℕ
⊢ ↑p ^ (m + 1) ∣
    Quotient.out ((coeff (ModP O p) p m) x * (coeff (ModP O p) p m) y) ^ p ^ m -
      (Quotient.out ((coeff (ModP O p) p m) x) * Quotient.out ((coeff (ModP O p) p m) y)) ^ 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 y : PreTilt O p
m : ℕ
⊢ ↑p ∣
    Quotient.out ((coeff (ModP O p) p m) x * (coeff (ModP O p) p m) y) -
      Quotient.out ((coeff (ModP O p) p m) x) * Quotient.out ((coeff (ModP O p) p m) y)

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

Tactic:
simp [untiltAux]

Result:
no goals

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

Tactic:
cases m with
| zero => simp [untiltAux]
| succ m =>
  simp only [untiltAux, _root_.map_mul, ← mul_pow]
  refine dvd_sub_pow_of_dvd_sub ?_ m
  rw [← mem_span_singleton, ← Ideal.Quotient.eq]
  simp

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 y : PreTilt O p
m : ℕ
⊢ ↑p ∣
    Quotient.out ((coeff (ModP O p) p m) x * (coeff (ModP O p) p m) y) -
      Quotient.out ((coeff (ModP O p) p m) x) * Quotient.out ((coeff (ModP O p) p m) y)

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 y : PreTilt O p
m : ℕ
⊢ (Ideal.Quotient.mk (span {↑p})) (Quotient.out ((coeff (ModP O p) p m) x * (coeff (ModP O p) p m) y)) =
    (Ideal.Quotient.mk (span {↑p})) (Quotient.out ((coeff (ModP O p) p m) x) * Quotient.out ((coeff (ModP O p) p m) y))

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
x y : PreTilt O p
m : ℕ
⊢ (Ideal.Quotient.mk (span {↑p})) (Quotient.out ((coeff (ModP O p) p m) x * (coeff (ModP O p) p m) y)) =
    (Ideal.Quotient.mk (span {↑p})) (Quotient.out ((coeff (ModP O p) p m) x) * Quotient.out ((coeff (ModP O p) p m) y))

Tactic:
simp

Result:
no goals