using theorem with existential quantifier

Stream: new members

[Brian Jiang]

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]

Use cases to destruct an existential

[Johan Commelin]

So

  cases relatively_prime_sum_to_one a b h with m n manb_eq_one,

[Johan Commelin]

Or maybe that's to advanced for cases... then you need rcases (recursive cases), with a slightly different syntax.

[Johan Commelin]

The cool thing is

rcases? relatively_prime_sum_to_one a b h,

will print a message telling you what to do

[Brian Jiang]

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]

what does manb_eq_one do?

[Brian Jiang]

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

[Bryan Gin-ge Chen]

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