# Zulip Chat Archive

## 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
```

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

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: Dec 20 2023 at 11:08 UTC