case intro
m n✝ a✝ b✝ c d b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = gcd a n * g
⊢ coprime a n
m n✝ a✝ b✝ c d b a n : ℕ
h : a * b ≡ 1 [MOD n]
⊢ coprime a n
obtain ⟨g, hh⟩ := Nat.gcd_dvd_right a n
case intro
m n✝ a✝ b✝ c d b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = gcd a n * g
⊢ 1 ≡ 0 [MOD gcd a n]
case intro
m n✝ a✝ b✝ c d b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = gcd a n * g
⊢ coprime a n
rw [Nat.coprime_iff_gcd_eq_one, ← Nat.dvd_one, ← Nat.modEq_zero_iff_dvd]
no goals
case intro
m n✝ a✝ b✝ c d b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = gcd a n * g
⊢ 1 ≡ 0 [MOD gcd a n]
calc
  1 ≡ a * b [MOD a.gcd n] := (hh ▸ h).symm.of_mul_right g
  _ ≡ 0 * b [MOD a.gcd n] := (Nat.modEq_zero_iff_dvd.mpr (Nat.gcd_dvd_left _ _)).mul_right b
  _ = 0 := by rw [zero_mul]
no goals
m n✝ a✝ b✝ c d b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = gcd a n * g
⊢ 0 * b = 0
rw [zero_mul]