## Stream: new members

### Topic: Axiom of choice, quotients, ℚ ⊆ ℝ

#### Pedro Minicz (Jun 17 2020 at 01:10):

The following is an example of an "obvious truth" that feels impossible to prove in Lean. I feel like this is due to my lack of familiarity with AC on Lean.

import data.real.basic
import group_theory.quotient_group

def Q : set ℝ := λ r, ∃ k : ℚ, ↑k = r

{ zero_mem := ⟨0, by push_cast; linarith⟩,
add_mem := λ _ _ ⟨a, _⟩ ⟨b, _⟩, ⟨a + b, by push_cast; linarith⟩,
neg_mem := λ _ ⟨a, _⟩, ⟨-a, by push_cast; linarith⟩ }

def RQ : Type := quotient_add_group.quotient Q
notation ℝ/ℚ := RQ

def RQ.mk : ℝ → ℝ/ℚ := quotient_add_group.mk

noncomputable def rational : ℝ := quot.out (RQ.mk (0 : ℝ))

example : rational ∈ Q := sorry


#### Pedro Minicz (Jun 17 2020 at 01:10):

I guess a proof by contradiction would suffice, but I haven't managed to come up with anything.

#### Bhavik Mehta (Jun 17 2020 at 01:33):

example : rational ∈ Q :=
begin
have : @setoid.r _ (quotient_add_group.left_rel Q) rational 0,
apply quotient.mk_out',
have := quotient.sound' this,

#### Pedro Minicz (Jun 17 2020 at 02:04):
It seems I wasn't able to leverage the definition of quotient_add_group.left_rel. Thank you!