no goals
m n a : Nat
cmn : coprime m n
dvd : a ∣ m
⊢ coprime (m / a) n
match eq_zero_or_pos a with
| .inl h0 =>
  rw [h0] at dvd
  rw [Nat.eq_zero_of_zero_dvd dvd] at cmn ⊢
  simp; assumption
| .inr hpos =>
  let ⟨k, hk⟩ := dvd
  rw [hk, Nat.mul_div_cancel_left _ hpos]
  rw [hk] at cmn
  exact cmn.coprime_mul_left
m n a : Nat
cmn : coprime m n
dvd : 0 ∣ m
h0 : a = 0
⊢ coprime (m / a) n
m n a : Nat
cmn : coprime m n
dvd : a ∣ m
h0 : a = 0
⊢ coprime (m / a) n
rw [h0] at dvd
m n a : Nat
cmn : coprime 0 n
dvd : 0 ∣ m
h0 : a = 0
⊢ coprime (0 / a) n
m n a : Nat
cmn : coprime m n
dvd : 0 ∣ m
h0 : a = 0
⊢ coprime (m / a) n
rw [Nat.eq_zero_of_zero_dvd dvd] at cmn ⊢
m n a : Nat
cmn : coprime 0 n
dvd : 0 ∣ m
h0 : a = 0
⊢ coprime 0 n
m n a : Nat
cmn : coprime 0 n
dvd : 0 ∣ m
h0 : a = 0
⊢ coprime (0 / a) n
simp
no goals
m n a : Nat
cmn : coprime 0 n
dvd : 0 ∣ m
h0 : a = 0
⊢ coprime 0 n
assumption
m n a : Nat
cmn : coprime m n
dvd : a ∣ m
hpos : a > 0
k : Nat
hk : m = a * k
⊢ coprime (m / a) n
m n a : Nat
cmn : coprime m n
dvd : a ∣ m
hpos : a > 0
⊢ coprime (m / a) n
let ⟨k, hk⟩ := dvd
m n a : Nat
cmn : coprime m n
dvd : a ∣ m
hpos : a > 0
k : Nat
hk : m = a * k
⊢ coprime k n
m n a : Nat
cmn : coprime m n
dvd : a ∣ m
hpos : a > 0
k : Nat
hk : m = a * k
⊢ coprime (m / a) n
rw [hk, Nat.mul_div_cancel_left _ hpos]
m n a : Nat
dvd : a ∣ m
hpos : a > 0
k : Nat
cmn : coprime (a * k) n
hk : m = a * k
⊢ coprime k n
m n a : Nat
cmn : coprime m n
dvd : a ∣ m
hpos : a > 0
k : Nat
hk : m = a * k
⊢ coprime k n
rw [hk] at cmn
no goals
m n a : Nat
dvd : a ∣ m
hpos : a > 0
k : Nat
cmn : coprime (a * k) n
hk : m = a * k
⊢ coprime k n
exact cmn.coprime_mul_left