Theorem: ZerosOnesAndTwos.lemma_3 (Compfiles/ZeroesOnesAndTwos.lean)

State before:
a n : ℕ
ha : 0 < a
hm : a % n = 0
⊢ ∃ k, a = n * ↑k
Tactic:
obtain ⟨k', hk'⟩ := exists_eq_mul_right_of_dvd (Nat.dvd_of_mod_eq_zero hm)
State after:
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
⊢ ∃ k, a = n * ↑k

State before:
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
⊢ ∃ k, a = n * ↑k
Tactic:
have hkp : 0 < k' := lt_of_mul_lt_mul_left' (hk' ▸ ha)
State after:
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
hkp : 0 < k'
⊢ ∃ k, a = n * ↑k

State before:
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
hkp : 0 < k'
⊢ ∃ k, a = n * ↑k
Tactic:
exact ⟨⟨k', hkp⟩, hk'⟩
State after:
no goals