rat.mk_eq

Stream: general

[Kenny Lau]

theorem mk_eq : ∀ {a b c d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0),
  a /. b = c /. d ↔ a * d = c * b :=
suffices ∀ a b c d hb hd, mk_pnat a ⟨b, hb⟩ = mk_pnat c ⟨d, hd⟩ ↔ a * d = c * b,
[...]

[Kenny Lau]

the one in suffices is what I need T_T

[Mario Carneiro]

Just rewrite mk_pnat into /., they are equal

[Kenny Lau]

this is what I did at the end:

theorem rat.mk_pnat_eq_iff (a b c d) : rat.mk_pnat a b = rat.mk_pnat c d ↔ a * d = c * b :=
begin
  cases b with b hb, cases d with d hd,
  simp [rat.mk_pnat_eq],
  rw [rat.mk_eq],
  exact ne_of_gt (int.coe_nat_pos.2 hb),
  exact ne_of_gt (int.coe_nat_pos.2 hd),
end

[Kenny Lau]

this part of the code is not going to be PR'd so the neatness of the proof doesn't really matter ot me

[Kenny Lau]

but I did write a whole bunch of lemmas in the meantime

[Mario Carneiro]

The real question is why are you dealing with mk_pnat? The interface should let you just use field operations and avoid mk entirely

[Kenny Lau]

oh, mk_pnat is not intended to be used?

[Kenny Lau]

I used it because I am using pnat

[Kenny Lau]

or are you going to tell me that pnat is not to be used either

[Mario Carneiro]

Just use n / d where d : N+

[Mario Carneiro]

The only reason you might want mk_pnat is if you care about the efficiency of computing this value (this will translate d to rat by adding ones)