Simplifying inverses in ring

Stream: new members

[Laurent Bartholdi]

Still working on @Kevin Buzzard 's homework, I stumbled on the following problem: how to simplify A*A⁻¹*B in a ring? I tried everything I could, with library_search, but got nowhere. First, a version that works:

lemma xxx (A B C ε : ℝ) (h0 : A ≠ 0) (h1 : C-0 = ε/A) (h2 : B = A) : B*C = ε := begin
  rw sub_zero at h1,
  calc B*C = A*(ε/A) : by rw [h1,h2]
  ... = ε : mul_div_cancel' ε h0
end

Now let's say I didn't care to use sub_zero but just hit it with ring (which is how my trouble started): ring will replace ε/A by A⁻¹*ε, thus

lemma xxx_fail (A B C ε : ℝ) (h0 : A ≠ 0) (h1 : C-0 = ε/A) (h2 : B = A) : B*C = ε := begin
  ring at h1,
  calc B*C = A*(A⁻¹*ε) : by rw [h1,h2]
  ... = (A*A⁻¹)*ε : by rw mul_assoc -- fails
  ... = ε : by rw mul_cancel_right -- fails
end

Again, I have a question and metaquestion: (1) can someone who reached enlightenment show me the way in xxx_fail? (2) I tried a lot of library_search, which did help a little (though it gave long-to-type suggestions of the form tactic.ring.xxxx). I also tried hint which waited for a long time without returning anything. Is there something like Isabelle's "sledgehammer", or a more efficient way of finding lemmas?

[Patrick Massot]

The mul_assoc rewrite is not failing

[Patrick Massot]

And mul_cancel_right doesn't seem to exist. The naming convention here would have mul_inv_cancel, not mul_cancel alone

[Patrick Massot]

import data.real.basic

lemma xxx_fail (A B C ε : ℝ) (h0 : A ≠ 0) (h1 : C-0 = ε/A) (h2 : B = A) : B*C = ε := begin
  ring at h1,
  calc B*C = A*(A⁻¹*ε) : by rw [h1,h2]
  ... = (A*A⁻¹)*ε : by rw mul_assoc
  ... = ε : by rw [mul_inv_cancel h0, one_mul]
end

[Patrick Massot]

But you don't need to know all those names:

import data.real.basic

lemma xxx_fail (A B C ε : ℝ) (h0 : A ≠ 0) (h1 : C-0 = ε/A) (h2 : B = A) : B*C = ε := begin
  ring at h1,
  calc B*C = A*(A⁻¹*ε) : by rw [h1,h2]
  ... = (A*A⁻¹)*ε : by ring
  ... = ε : by field_simp [h0]
end

[Patrick Massot]

And library_search does know it:

example (A : ℝ)(h0 : A ≠ 0) : A*A⁻¹ = 1 :=
by library_search