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