canceling through in rat

Stream: new members

[Yakov Pechersky]

What's the way to prove this? I am unable to get it into a form where library_search or guessing lemma names helps. The lemmas I guess are just for groups, not fields.

import tactic.ring_exp

example (n : ℕ) : (n : ℚ)⁻¹ = 2 / (n * 2) :=
begin
end

[Pedro Minicz]

example (n : ℕ) : (n : ℚ)⁻¹ = 2 / (n * 2) :=
begin
  rw [←one_div, mul_comm, ←div_div_eq_div_mul],
  norm_num
end

[Pedro Minicz]

My strategy was to look for lemmas by creating small examples:

-- For this use, I used `simp` then `squeeze_simp` to find the lemma.
example (a : ℚ) : a⁻¹ = 1 / a :=
by simp only [one_div]

-- This one I tried `simp`, which failed, then `library_search`.
example (a b c : ℚ) : a / (b * c) = (a / b) / c :=
(div_div_eq_div_mul a b c).symm

[Pedro Minicz]

Also, searching for div div in the #docs, I found div_mul_eq_div_mul_one_div, which could have been used:

example (n : ℕ) : (n : ℚ)⁻¹ = 2 / (n * 2) :=
begin
  rw [←one_div, mul_comm, div_mul_eq_div_mul_one_div],
  norm_num
end

[Yakov Pechersky]

Thanks!

[Yakov Pechersky]

norm_num can take lemmas in [] too, so it can be a one liner

[Pedro Minicz]

Yakov Pechersky said:

norm_num can take lemmas in [] too, so it can be a one liner

Oh, cool. I usually forget that. :grinning_face_with_smiling_eyes:

[Heather Macbeth]

Or, with more tactics and fewer (no) lemmas,

example (n : ℕ) : (n : ℚ)⁻¹ = 2 / (n * 2) :=
begin
  by_cases h₁ : n = 0,
  { simp [h₁] },
  { have h₂ : 2 ≠ 0 := by norm_num,
    field_simp [h₁, h₂],
    ring }
end

[Yury G. Kudryashov]

Two more proofs:

example (n : ℕ) : (n : ℚ)⁻¹ = 2 / (n * 2) :=
by { rw [div_mul_left, one_div], norm_num }

example (n : ℕ) : (n : ℚ)⁻¹ = 2 / (n * 2) :=
by { rw [div_mul_left (@two_ne_zero ℚ _), one_div] }

[Yury G. Kudryashov]

My strategy: I know that a / (b * a) = 1 / b should be a theorem about group_with_zero, so I searched algebra/group_with_zero and found docs#div_mul_left

[Scott Morrison]

I like Heather's approach --- certainly it is the "slowest", but it's also the most conceptual and laziest! Lazy is good, of course, when doing mathematics.

[Scott Morrison]

One doesn't really need to "know the names of all the lemmas", because there are lots of usable patterns and tricks to guess lemma names quickly, but it still feels too much like ... botany. :-)