# Zulip Chat Archive

## Stream: new members

### Topic: using theorem with existential quantifier

#### Brian Jiang (Mar 20 2020 at 18:00):

I have the following theorem with m and n defined existentially (I defined relatively_prime as coprime already):

theorem relatively_prime_sum_to_one (a b : ℤ) (h : relatively_prime a b) : ∃ m n : ℤ, m * a + n * b = 1 := sorry

I want to use and manipulate the expression ma + nb = 1 in the proof of another theorem, but how can I pull out this expression?

#### Johan Commelin (Mar 20 2020 at 18:02):

Use `cases`

to destruct an existential

#### Johan Commelin (Mar 20 2020 at 18:03):

So

cases relatively_prime_sum_to_one a b h with m n manb_eq_one,

#### Johan Commelin (Mar 20 2020 at 18:03):

Or maybe that's to advanced for `cases`

... then you need `rcases`

(recursive `cases`

), with a slightly different syntax.

#### Johan Commelin (Mar 20 2020 at 18:04):

The cool thing is

rcases? relatively_prime_sum_to_one a b h,

will print a message telling you what to do

#### Brian Jiang (Mar 21 2020 at 02:56):

So far I have the following theorem I've been trying to prove and applied what you suggested with cases:

theorem divides_product_coprime_and_not_coprime (a b n:ℤ) (c: divides n (a*b)) (d: relatively_prime a n): divides n b:= begin cases relatively_prime_sum_to_one a n d with m n manb_eq_one, end

#### Brian Jiang (Mar 21 2020 at 02:58):

what does manb_eq_one do?

#### Brian Jiang (Mar 21 2020 at 02:58):

and can someone show me how to multiply both sides of the resulting expression by a value (b)?

#### Bryan Gin-ge Chen (Mar 21 2020 at 03:43):

In your code, `manb_eq_one`

isn't doing anything. If you want to use `cases`

here, you'll have to use it twice:

def relatively_prime : ℤ → ℤ → Prop := sorry theorem relatively_prime_sum_to_one (a b : ℤ) (h : relatively_prime a b) : ∃ m n : ℤ, m * a + n * b = 1 := sorry def divides : ℤ → ℤ → Prop := sorry theorem divides_product_coprime_and_not_coprime (a b n:ℤ) (c: divides n (a*b)) (d: relatively_prime a n): divides n b:= begin cases relatively_prime_sum_to_one a n d with m h, cases h with n' manb_eq_one, -- m n : ℤ, -- manb_eq_one : m * a + n' * n = 1 have := congr_arg (has_mul.mul b) manb_eq_one, -- this : b * (m * a + n' * n) = b * 1 rw [mul_one] at this, -- this : b * (m * a + n' * n) = b end

As Johan hinted, it's easier to use `rcases`

than `cases`

here:

import tactic.basic def relatively_prime : ℤ → ℤ → Prop := sorry theorem relatively_prime_sum_to_one (a b : ℤ) (h : relatively_prime a b) : ∃ m n : ℤ, m * a + n * b = 1 := sorry def divides : ℤ → ℤ → Prop := sorry theorem divides_product_coprime_and_not_coprime (a b n:ℤ) (c: divides n (a*b)) (d: relatively_prime a n): divides n b:= begin rcases relatively_prime_sum_to_one a n d with ⟨m, n', manb_eq_one⟩, -- m n : ℤ, -- manb_eq_one : m * a + n' * n = 1 have := congr_arg (has_mul.mul b) manb_eq_one, -- this : b * (m * a + n' * n) = b * 1 rw [mul_one] at this, -- this : b * (m * a + n' * n) = b end

Last updated: May 08 2021 at 10:12 UTC