k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
⊢ ∃ m, n * m % k = gcd n k
k n : ℕ
hk : gcd n k < k
⊢ ∃ m, n * m % k = gcd n k
have hk' := Int.ofNat_ne_zero.2 (ne_of_gt (lt_of_le_of_lt (zero_le (gcd n k)) hk))
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : (fun m => Int.toNat (m % ↑k)) ↑(gcd n k) = (fun m => Int.toNat (m % ↑k)) (↑n * gcdA n k + ↑k * gcdB n k)
⊢ ∃ m, n * m % k = gcd n k
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
⊢ ∃ m, n * m % k = gcd n k
have key := congr_arg (fun (m : ℤ) => (m % k).toNat) (gcd_eq_gcd_ab n k)
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : Int.toNat (↑(gcd n k) % ↑k) = Int.toNat ((↑n * gcdA n k + ↑k * gcdB n k) % ↑k)
⊢ ∃ m, n * m % k = gcd n k
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : (fun m => Int.toNat (m % ↑k)) ↑(gcd n k) = (fun m => Int.toNat (m % ↑k)) (↑n * gcdA n k + ↑k * gcdB n k)
⊢ ∃ m, n * m % k = gcd n k
simp only at key
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : gcd n k = Int.toNat (↑n * gcdA n k % ↑k)
⊢ ∃ m, n * m % k = gcd n k
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : Int.toNat (↑(gcd n k) % ↑k) = Int.toNat ((↑n * gcdA n k + ↑k * gcdB n k) % ↑k)
⊢ ∃ m, n * m % k = gcd n k
rw [Int.add_mul_emod_self_left, ← Int.coe_nat_mod, Int.toNat_coe_nat, mod_eq_of_lt hk] at key
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : gcd n k = Int.toNat (↑n * gcdA n k % ↑k)
⊢ Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : gcd n k = Int.toNat (↑n * gcdA n k % ↑k)
⊢ ∃ m, n * m % k = gcd n k
refine' ⟨(n.gcdA k % k).toNat, Eq.trans (Int.ofNat.inj _) key.symm⟩
no goals
k n : ℕ
hk : gcd n k < k
hk' : ↑k ≠ 0
key : gcd n k = Int.toNat (↑n * gcdA n k % ↑k)
⊢ Int.ofNat (n * Int.toNat (gcdA n k % ↑k) % k) = Int.ofNat (Int.toNat (↑n * gcdA n k % ↑k))
rw [Int.ofNat_eq_coe, Int.coe_nat_mod, Int.ofNat_mul, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'),
  Int.ofNat_eq_coe, Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod,
  ← Int.mul_emod]