real.mul_inv

Stream: general

[Bolton Bailey]

I spent some time looking for the lemma (a * b)⁻¹ = a⁻¹ * b⁻¹ for reals. I eventually found mul_inv₀, but it seems like this would be hard for someone to guess, or find in the docs. Can we make real.mul_inv an alias for the real version of this lemma?

[Eric Rodriguez]

I think this is pretty sensible; mul_inv for groups, mul_inv₀ for groups with zero [like (R,*)]. I feel like it's surprising the first time but thenforth fine. Maybe in undergraduate mode...

[Heather Macbeth]

I don't think we should provide aliases of a lemma about a typeclass for every instance of that typeclass. That's what library_search is for.

import data.real.basic

example (a b : ℝ) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by library_search

[Heather Macbeth]

More generally, do you know about the automation we have for such things, like ring and field_simp?

[Bolton Bailey]

Yes I know about the automation, but in my case, ring and field_simp failed to resolve or make noticeable progress on the goal.
I suppose I could have tried library_search. I guess the reason I didn't here is that I decided that if the lemma existed, I would probably be able to find it by searching "mul inv" in the docs, but I did that and didn't find it. Then I went to the definition of group_with_zero in algebra/group_with_zero/defs.lean and didn't find it nearby, then later realized that what I needed was in algebra/group_with_zero/basic.lean.

[Bolton Bailey]

I just felt my confusion would have been avoided if this lemma, which is identical to mul_inv, had the same name.

[Bolton Bailey]

Perhaps I don't know as much about the proof automation as I think. Is there a single-tactic or two-tactic proof of the following lemma:

import data.real.basic
lemma equality4 {x : ℝ} (h : x ≠ 0) : 2 * x / 3 * log 4 / (x * log 4) = 2 / 3 :=
begin
  sorry,
end

[Heather Macbeth]

import analysis.special_functions.log

open real

lemma equality4 {x : ℝ} (h : x ≠ 0) : 2 * x / 3 * log 4 / (x * log 4) = 2 / 3 :=
begin
  have : log 4 ≠ 0 := real.log_ne_zero_of_pos_of_ne_one (by norm_num) (by norm_num),
  field_simp,
  ring
end