## 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