-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem norm_sub_modPart (h : ‖(r : ℚ_[p])‖ ≤ 1) : ‖(⟨r, h⟩ - modPart p r : ℤ_[p])‖ < 1

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ↑p ∣ (⟨↑r, h⟩ - ↑(modPart p r)) * ↑r.den

Tactic:
suffices ↑p ∣ r.num - n * r.den by
  convert (Int.castRingHom ℤ_[p]).map_dvd this
  simp only [n, sub_mul, Int.cast_natCast, eq_intCast, Int.cast_mul, sub_left_inj,
    Int.cast_sub]
  apply Subtype.coe_injective
  simp only [coe_mul, Subtype.coe_mk, coe_natCast]
  rw_mod_cast [@Rat.mul_den_eq_num r]
  rfl

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ↑p ∣ r.num - n * ↑r.den

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ‖⟨↑r, h⟩ - ↑(modPart p r)‖ < 1

Tactic:
rw [norm_lt_one_iff_dvd, ← (isUnit_den r h).dvd_mul_right]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ↑p ∣ (⟨↑r, h⟩ - ↑(modPart p r)) * ↑r.den

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ↑p ∣ r.num - n * ↑r.den

Tactic:
exact norm_sub_modPart_aux r h

Result:
no goals

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ ↑p ∣ (⟨↑r, h⟩ - ↑(modPart p r)) * ↑r.den

Tactic:
convert (Int.castRingHom ℤ_[p]).map_dvd this

Result:
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ (⟨↑r, h⟩ - ↑(modPart p r)) * ↑r.den = (Int.castRingHom ℤ_[p]) (r.num - n * ↑r.den)

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ‖⟨↑r, h⟩ - ↑(modPart p r)‖ < 1

Tactic:
let n := modPart p r

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ‖⟨↑r, h⟩ - ↑(modPart p r)‖ < 1

Proof state:
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ (⟨↑r, h⟩ - ↑(modPart p r)) * ↑r.den = (Int.castRingHom ℤ_[p]) (r.num - n * ↑r.den)

Tactic:
simp only [n, sub_mul, Int.cast_natCast, eq_intCast, Int.cast_mul, sub_left_inj,
  Int.cast_sub]

Result:
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ ⟨↑r, h⟩ * ↑r.den = ↑r.num

Proof state:
case h.e'_4.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
h : ‖↑r‖ ≤ 1
⊢ ↑↑r.num = ↑r.num

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ ⟨↑r, h⟩ * ↑r.den = ↑r.num

Tactic:
apply Subtype.coe_injective

Result:
case h.e'_4.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ (fun a => ↑a) (⟨↑r, h⟩ * ↑r.den) = (fun a => ↑a) ↑r.num

Proof state:
case h.e'_4.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ ↑r * ↑r.den = ↑↑r.num

Tactic:
rw_mod_cast [@Rat.mul_den_eq_num r]

Result:
case h.e'_4.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
h : ‖↑r‖ ≤ 1
⊢ ↑↑r.num = ↑r.num

Proof state:
case h.e'_4.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ (fun a => ↑a) (⟨↑r, h⟩ * ↑r.den) = (fun a => ↑a) ↑r.num

Tactic:
simp only [coe_mul, Subtype.coe_mk, coe_natCast]

Result:
case h.e'_4.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ ↑r * ↑r.den = ↑↑r.num