p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑(r.num - r.num * gcdA r.den p % ↑p * ↑r.den) = 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑p ∣ r.num - r.num * gcdA r.den p % ↑p * ↑r.den
rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑r.num - ↑(r.num * gcdA r.den p % ↑p) * ↑r.den = 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑(r.num - r.num * gcdA r.den p % ↑p * ↑r.den) = 0
simp only [Int.cast_ofNat, ZMod.nat_cast_mod, Int.cast_mul, Int.cast_sub]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : (fun x => ↑x % ↑p) ↑(Nat.gcd r.den p) = (fun x => ↑x % ↑p) (↑r.den * gcdA r.den p + ↑p * gcdB r.den p)
⊢ ↑r.num - ↑(r.num * gcdA r.den p % ↑p) * ↑r.den = 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑r.num - ↑(r.num * gcdA r.den p % ↑p) * ↑r.den = 0
have := congr_arg (fun x => x % p : ℤ → ZMod p) (gcd_eq_gcd_ab r.den p)
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ↑r.num - ↑(r.num * gcdA r.den p % ↑p) * ↑r.den = 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : (fun x => ↑x % ↑p) ↑(Nat.gcd r.den p) = (fun x => ↑x % ↑p) (↑r.den * gcdA r.den p + ↑p * gcdB r.den p)
⊢ ↑r.num - ↑(r.num * gcdA r.den p % ↑p) * ↑r.den = 0
simp only [Int.cast_ofNat, CharP.cast_eq_zero, EuclideanDomain.mod_zero, Int.cast_add,
  Int.cast_mul, zero_mul, add_zero] at this
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ↑r.num - ↑r.num * ↑(gcdA r.den p) * ↑r.den = 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ↑r.num - ↑(r.num * gcdA r.den p % ↑p) * ↑r.den = 0
push_cast
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ↑r.num - ↑r.num * ↑(Nat.gcd r.den p) = 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ↑r.num - ↑r.num * ↑(gcdA r.den p) * ↑r.den = 0
rw [mul_right_comm, mul_assoc, ← this]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
rdcp : coprime r.den p
⊢ ↑r.num - ↑r.num * ↑(Nat.gcd r.den p) = 0

case rdcp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ coprime r.den p
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ↑r.num - ↑r.num * ↑(Nat.gcd r.den p) = 0
suffices rdcp : r.den.coprime p
case rdcp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ coprime p r.den
case rdcp
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ coprime r.den p
apply coprime.symm
case rdcp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ¬p ∣ r.den
case rdcp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ coprime p r.den
apply (coprime_or_dvd_of_prime hp_prime.1 _).resolve_right
case rdcp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ 1 ≤ ‖↑↑r.den‖
case rdcp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ¬p ∣ r.den
rw [← Int.coe_nat_dvd, ← norm_int_lt_one_iff_dvd, not_lt]
case rdcp.a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ‖↑↑r.den‖ = 1
case rdcp.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ 1 ≤ ‖↑↑r.den‖
apply ge_of_eq
case rdcp.a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ IsUnit ↑↑r.den
case rdcp.a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ ‖↑↑r.den‖ = 1
rw [← isUnit_iff]
no goals
case rdcp.a.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
⊢ IsUnit ↑↑r.den
exact isUnit_den r h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
rdcp : coprime r.den p
⊢ ↑r.num - ↑r.num * ↑1 = 0
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
rdcp : coprime r.den p
⊢ ↑r.num - ↑r.num * ↑(Nat.gcd r.den p) = 0
rw [rdcp.gcd_eq_one]
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(Nat.gcd r.den p) = ↑r.den * ↑(gcdA r.den p)
rdcp : coprime r.den p
⊢ ↑r.num - ↑r.num * ↑1 = 0
simp only [mul_one, cast_one, sub_self]