cases n with
| zero =>
  simp [isCoprime_zero_right] at h
  rw [ZMod.mul_inv_eq_gcd, Nat.gcd_zero_right, Nat.cast_eq_one]
  simp only [ZMod.val]
  rw [Int.cast_id, Int.IsUnit.natAbs_eq h]
| succ n =>
  haveI := n.succ_pos
  rw [← Int.gcd_eq_one_iff_coprime, Int.gcd_comm, Int.gcd_val] at h
  rw [ZMod.mul_inv_eq_gcd, ← Int.coe_nat_gcd, ZMod.val_int_cast, h, Nat.cast_one]
n : ℕ
x : ℤ
h : IsCoprime x ↑n
⊢ ↑x * (↑x)⁻¹ = 1
no goals