Axiom of choice, quotients, ℚ ⊆ ℝ

Stream: new members

[Pedro Minicz]

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

instance : is_add_subgroup Q :=
{ 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]

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

[Bhavik Mehta]

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

Here's how I did it - I don't think this was at all easy to find though :( Hopefully others can clear it up for you better

[Pedro Minicz]

It seems I wasn't able to leverage the definition of quotient_add_group.left_rel. Thank you!