Using one Exists to prove another?

Stream: new members

[ROCKY KAMEN-RUBIO]

This came up in my attempt at the first codewars Lean problem. I want to show that the inductive definition for divisibility by 3 (mult_3) implies that the number can also be written as a multiple of 3. I'm getting stuck at the end of my p_eq_3n proof. I want to extract a k from h, and then use k+3 on my goal state, and I saw another post suggest using classical.some, but then my goal state doesn't seem responsive to rfl. Am I misusing classical.some? Is there another way to do this?

import data.nat.basic
import data.set

open nat

inductive mult_3 : set ℕ
| mult_3_O :
    mult_3 0
| mult_3_SSS : ∀ n,
    mult_3 n →
    mult_3 (n + 3)

open_locale classical
lemma p_eq_3n (n : ℕ) : mult_3 n → ∃ (k:ℕ), n = 3*k :=
begin
intro hn,
apply mult_3.rec_on hn,
apply exists.intro 0,
refl,
intros n hn2 h,
have k := classical.some h,
apply exists.intro (k + 1),
end

[Kenny Lau]

cases h with k hk,

[ROCKY KAMEN-RUBIO]

Kenny Lau said:

cases h with k hk,

Thank you!

[Donald Sebastian Leung]

@ROCKY KAMEN-RUBIO Welcome to Codewars! :tada: :smile: