## Stream: new members

### Topic: Using one Exists to prove another?

#### ROCKY KAMEN-RUBIO (Apr 10 2020 at 04:50):

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 (Apr 10 2020 at 04:52):

cases h with k hk,


#### ROCKY KAMEN-RUBIO (Apr 10 2020 at 05:14):

Kenny Lau said:

cases h with k hk,


Thank you!

#### Donald Sebastian Leung (Apr 10 2020 at 05:35):

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

Last updated: May 06 2021 at 22:13 UTC