What should be my next step here?

Stream: maths

[Nicholas McConnell]

import tactic
universe u
local attribute [instance] classical.prop_decidable

lemma bezout (a p : ℕ) (hp : prime p) (ha : ¬(divides p a)) :
  ∃(x:ℤ), (∃(y:ℤ), (x*a + y*p = 1)) :=
begin
rw prime at hp,
cases hp with hp1,
have zero_lt_one := nat.lt_succ_self 0,
have p_pos := lt_trans zero_lt_one hp1,
have dh : ∃ (d : ℕ), 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d := LCex a p p_pos,
let d := nat.find(dh),
have dx : 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d := nat.find_spec dh,
have dm : ∀ d', (0 < d' ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d') → d ≤ d' := λ d', nat.find_min' dh,
cases dx with dx1 dx2,
have h := lt_trichotomy 1 d,
cases h with h1 h2,
have r1 := div_alg a d dx1,
cases r1 with r hr,
cases hr with q hq,
cases hq with hq1 hq2,
cases dx2 with x_ex hx,
cases hx with y_ex hy,
have thing := dm r,
have htr := lt_trichotomy 0 r,
cases htr with htr1 htr2,
have claim : (1-x_ex*q) * ↑a + (-y_ex*q) * ↑p = ↑r,
ring,
rw sub_mul,
rw one_mul,
rw hq1,
rw hq1 at hy,

-- ...
end

I'm not sure how to deal with this subordinate claim with all the differences between integers and naturals:

4 goals
a p : ℕ,
ha : ¬divides p a,
hp1 : 1 < p,
hp2 : ∀ (k : ℕ), divides k p → k = 1 ∨ k = p,
zero_lt_one : 0 < 1,
p_pos : 0 < p,
dh : ∃ (d : ℕ), 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d,
d : ℕ := nat.find dh,
dm : ∀ (d' : ℕ), (0 < d' ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d') → d ≤ d',
dx1 : 0 < d,
h1 : 1 < d,
r q : ℕ,
hq1 : a = d * q + r,
hq2 : r < d,
x_ex y_ex : ℤ,
thing : (0 < r ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑r) → d ≤ r,
htr1 : 0 < r,
hy : x_ex * ↑(d * q + r) + y_ex * ↑p = ↑d
⊢ ↑(d * q + r) - x_ex * ↑q * ↑(d * q + r) - y_ex * ↑q * ↑p = ↑r

[Scott Morrison]

I'm not going to look at this now --- but, when Mario suggested a "minimum working example", the "minimum" part is helpful advice. If I'm stuck on a proof, I really try to minimise it. You might consider things like

• use clear to discard irrelevant hypotheses
• use extract_goal to restate the current goal as a lemma, and try proving that earlier in the file

[Mario Carneiro]

oh, I hadn't noticed extract_goal, that looks really nice for this

[Mario Carneiro]

also those imports don't work for me

[Nicholas McConnell]

Yikes :