case zero
a : ZMod Nat.zero
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) Nat.zero)

case succ
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) (Nat.succ n))
n : ℕ
a : ZMod n
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) n)
cases' n with n
case zero
a : ℤ
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) 0)
case zero
a : ZMod Nat.zero
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) Nat.zero)
dsimp [ZMod] at a ⊢
no goals
case zero
a : ℤ
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) 0)
calc
  _ = a * Int.sign a := rfl
  _ = a.natAbs := by rw [Int.mul_sign]
  _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]
no goals
a : ℤ
⊢ a * Int.sign a = ↑(Int.natAbs a)
rw [Int.mul_sign]
no goals
a : ℤ
⊢ ↑(Int.natAbs a) = ↑(Nat.gcd (Int.natAbs a) 0)
rw [Nat.gcd_zero_right]
no goals
case succ
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ = ↑(Nat.gcd (val a) (Nat.succ n))
calc
  a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
    rw [nat_cast_self, MulZeroClass.zero_mul, add_zero]
  _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
    push_cast
    rw [nat_cast_zmod_val]
    rfl
  _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl
no goals
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ = a * a⁻¹ + ↑(Nat.succ n) * ↑(Nat.gcdB (val a) (Nat.succ n))
rw [nat_cast_self, MulZeroClass.zero_mul, add_zero]
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n)) =
    ↑(val a) * ↑(Nat.gcdA (val a) (Nat.succ n)) + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n))
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ + ↑(Nat.succ n) * ↑(Nat.gcdB (val a) (Nat.succ n)) =
    ↑(↑(val a) * Nat.gcdA (val a) (Nat.succ n) + ↑(Nat.succ n) * Nat.gcdB (val a) (Nat.succ n))
push_cast
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n)) =
    a * ↑(Nat.gcdA (val a) (Nat.succ n)) + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n))
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n)) =
    ↑(val a) * ↑(Nat.gcdA (val a) (Nat.succ n)) + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n))
rw [nat_cast_zmod_val]
no goals
n : ℕ
a : ZMod (Nat.succ n)
⊢ a * a⁻¹ + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n)) =
    a * ↑(Nat.gcdA (val a) (Nat.succ n)) + (↑n + 1) * ↑(Nat.gcdB (val a) (Nat.succ n))
rfl
n : ℕ
a : ZMod (Nat.succ n)
⊢ ↑↑(Nat.gcd (val a) (Nat.succ n)) = ↑(Nat.gcd (val a) (Nat.succ n))
n : ℕ
a : ZMod (Nat.succ n)
⊢ ↑(↑(val a) * Nat.gcdA (val a) (Nat.succ n) + ↑(Nat.succ n) * Nat.gcdB (val a) (Nat.succ n)) =
    ↑(Nat.gcd (val a) (Nat.succ n))
rw [← Nat.gcd_eq_gcd_ab a.val n.succ]
no goals
n : ℕ
a : ZMod (Nat.succ n)
⊢ ↑↑(Nat.gcd (val a) (Nat.succ n)) = ↑(Nat.gcd (val a) (Nat.succ n))
rfl