-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem norm_sub_modPart_aux (r : ℚ) (h : ‖(r : ℚ_[p])‖ ≤ 1) :
    ↑p ∣ r.num - r.num * r.den.gcdA p % p * ↑r.den

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ↑r.num - ↑r.num * ↑(r.den.gcd p) = 0

Tactic:
suffices rdcp : r.den.Coprime p by
  rw [rdcp.gcd_eq_one]
  simp only [mul_one, cast_one, sub_self]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ r.den.Coprime p

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑(r.num - r.num * r.den.gcdA p % ↑p * ↑r.den) = 0

Tactic:
simp only [Int.cast_natCast, ZMod.natCast_mod, Int.cast_mul, Int.cast_sub]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0

Proof state:
case a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ‖↑↑r.den‖ = 1

Tactic:
rw [← isUnit_iff]

Result:
case a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ IsUnit ↑↑r.den

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0

Tactic:
have := congr_arg (fun x => x % p : ℤ → ZMod p) (gcd_eq_gcd_ab r.den p)

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : (fun x => ↑x % ↑p) ↑(r.den.gcd p) = (fun x => ↑x % ↑p) (↑r.den * r.den.gcdA p + ↑p * r.den.gcdB p)
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ↑r.num - ↑r.num * ↑(r.den.gcdA p) * ↑r.den = 0

Tactic:
rw [mul_right_comm, mul_assoc, ← this]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ↑r.num - ↑r.num * ↑(r.den.gcd p) = 0

Proof state:
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ¬p ∣ r.den

Tactic:
rw [← Int.natCast_dvd_natCast, ← norm_int_lt_one_iff_dvd, not_lt]

Result:
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ 1 ≤ ‖↑↑r.den‖

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ r.den.Coprime p

Tactic:
apply Coprime.symm

Result:
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ p.Coprime r.den

Proof state:
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ p.Coprime r.den

Tactic:
apply (coprime_or_dvd_of_prime hp_prime.1 _).resolve_right

Result:
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ¬p ∣ r.den

Proof state:
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ 1 ≤ ‖↑↑r.den‖

Tactic:
apply ge_of_eq

Result:
case a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ‖↑↑r.den‖ = 1

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0

Tactic:
push_cast

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ↑r.num - ↑r.num * ↑(r.den.gcdA p) * ↑r.den = 0

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
rdcp : r.den.Coprime p
⊢ ↑r.num - ↑r.num * ↑1 = 0

Tactic:
simp only [mul_one, cast_one, sub_self]

Result:
no goals

Proof state:
case a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ IsUnit ↑↑r.den

Tactic:
exact isUnit_den r h

Result:
no goals

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

Tactic:
rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑(r.num - r.num * r.den.gcdA p % ↑p * ↑r.den) = 0

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : (fun x => ↑x % ↑p) ↑(r.den.gcd p) = (fun x => ↑x % ↑p) (↑r.den * r.den.gcdA p + ↑p * r.den.gcdB p)
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0

Tactic:
simp only [Int.cast_natCast, CharP.cast_eq_zero, EuclideanDomain.mod_zero, Int.cast_add,
  Int.cast_mul, zero_mul, add_zero] at this

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
rdcp : r.den.Coprime p
⊢ ↑r.num - ↑r.num * ↑(r.den.gcd p) = 0

Tactic:
rw [rdcp.gcd_eq_one]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
rdcp : r.den.Coprime p
⊢ ↑r.num - ↑r.num * ↑1 = 0