Quotients and passing an inequality around

Stream: new members

[Kauê Campos]

I've been going through a real analysis book and trying to port it to Lean as an exercise, and I've began to define the rationals on top of integers using Quotient:

instance myratSetoid : Setoid (myrat) where
  r := rel_rat
  iseqv := is_equivalence_rat

def MyRat := Quotient myratSetoid

And I was able to define multiplication and addition normally, using Quot.liftOn₂, but I'm having problems trying to figure out how to do it with the reciprocal:

def inv_fn (a: myrat) (a_neq : a.n ≠ 0) : MyRat := (a.d // a.n) a_neq

private theorem inv_respects (a a' : myrat) (ha: a.n ≠ 0) (ha': a'.n ≠ 0) (haa': a ~ a') : inv_fn a ha = inv_fn a' ha' := by {
  unfold rel_rat at haa'
  apply rel_int_rat
  rw [mul_comm, haa'.symm]
  ring
}

-- I already have this: theorem numerator_neq_zero (x: MyRat) (ha: x ≠ 0) : ∀(n m : MyInt) (hm: m ≠ 0), (n // m) hm = x → n ≠ 0
-- def inv (a: MyRat) (a_neq : a ≠ 0) : MyRat := ???

But the issue I've been having is actually passing the inequality onto Quot.liftOn, the closes thing I've got is to make another structure called temp_rat that actually has this equivalence, then I can use Quot.liftOn on it, allowing me to define inv_temp:

structure temp_rat where
  mk ::
  r: myrat
  n_neq: r.n ≠ 0

def rel_temp_rat (a: temp_rat) (b: temp_rat) : Prop := a.r ~ b.r

private theorem is_equivalence_temp : Equivalence rel_temp_rat where
  refl := fun x => rel_rat_refl x.r
  symm := fun a => rel_rat_symm a
  trans := fun a1 a2 => rel_rat_trans a1 a2

instance tempSetoid : Setoid (temp_rat) where
  r := rel_temp_rat
  iseqv := is_equivalence_temp

def TempRat := Quotient tempSetoid

def inv_temp (a : TempRat) : MyRat :=
  Quot.liftOn a (fun x => inv_fn x.r x.n_neq) (by {
    intro a a' haa'
    exact inv_respects a.r a'.r a.n_neq a'.n_neq haa'
  })

But I don't see a way to define def inv (a: MyRat) (a_neq : a ≠ 0) : MyRat from this in any sane way. I know that mathlib forgoes the zero divisor problem by defining it in the operation, but I'd like to define it like this anyway, this is just an exercise and doing it like this follows closer to the procedure of the book. Can anyone guide me towards a way to do this? I've been stuck in this for a while.