## Stream: new members

### Topic: canceling through in rat

#### Yakov Pechersky (Sep 27 2020 at 01:55):

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 (Sep 27 2020 at 02:00):

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


#### Pedro Minicz (Sep 27 2020 at 02:01):

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 (Sep 27 2020 at 02:03):

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


Thanks!

#### Yakov Pechersky (Sep 27 2020 at 02:07):

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

#### Pedro Minicz (Sep 27 2020 at 02:09):

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 (Sep 27 2020 at 02:18):

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 (Sep 27 2020 at 02:23):

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 (Sep 27 2020 at 02:24):

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 (Sep 27 2020 at 03:25):

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 (Sep 27 2020 at 03:26):

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. :-)

Last updated: May 15 2021 at 00:39 UTC