k m : ℕ+
⊢ ↑k ∣ ↑m ↔ mod m k = k
k m : ℕ+
⊢ k ∣ m ↔ mod m k = k
rw [dvd_iff]
k m : ℕ+
⊢ ↑m % ↑k = 0 ↔ mod m k = k
k m : ℕ+
⊢ ↑k ∣ ↑m ↔ mod m k = k
rw [Nat.dvd_iff_mod_eq_zero]
case mp
k m : ℕ+
⊢ ↑m % ↑k = 0 → mod m k = k

case mpr
k m : ℕ+
⊢ mod m k = k → ↑m % ↑k = 0
k m : ℕ+
⊢ ↑m % ↑k = 0 ↔ mod m k = k
constructor
case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ mod m k = k
case mp
k m : ℕ+
⊢ ↑m % ↑k = 0 → mod m k = k
intro h
case mp.a
k m : ℕ+
h : ↑m % ↑k = 0
⊢ ↑(mod m k) = ↑k
case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ mod m k = k
apply PNat.eq
no goals
case mp.a
k m : ℕ+
h : ↑m % ↑k = 0
⊢ ↑(mod m k) = ↑k
rw [mod_coe, if_pos h]
case mpr
k m : ℕ+
h : mod m k = k
⊢ ↑m % ↑k = 0
case mpr
k m : ℕ+
⊢ mod m k = k → ↑m % ↑k = 0
intro h
case pos
k m : ℕ+
h : mod m k = k
h' : ↑m % ↑k = 0
⊢ ↑m % ↑k = 0

case neg
k m : ℕ+
h : mod m k = k
h' : ¬↑m % ↑k = 0
⊢ ↑m % ↑k = 0
case mpr
k m : ℕ+
h : mod m k = k
⊢ ↑m % ↑k = 0
by_cases h' : (m : ℕ) % (k : ℕ) = 0
no goals
case pos
k m : ℕ+
h : mod m k = k
h' : ↑m % ↑k = 0
⊢ ↑m % ↑k = 0
exact h'
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑(mod m k) = ↑k
⊢ ↑m % ↑k = 0
case neg
k m : ℕ+
h : mod m k = k
h' : ¬↑m % ↑k = 0
⊢ ↑m % ↑k = 0
replace h : (mod m k : ℕ) = (k : ℕ) := congr_arg _ h
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑m % ↑k = ↑k
⊢ ↑m % ↑k = 0
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑(mod m k) = ↑k
⊢ ↑m % ↑k = 0
rw [mod_coe, if_neg h'] at h
no goals
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑m % ↑k = ↑k
⊢ ↑m % ↑k = 0
exact ((Nat.mod_lt (m : ℕ) k.pos).ne h).elim