Zulip Chat Archive

Stream: new members

Topic: canceling through in rat


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Sep 27 2020 at 02:05):

Thanks!

view this post on Zulip Yakov Pechersky (Sep 27 2020 at 02:07):

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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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] }

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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