## Stream: new members

### Topic: Simplifying inverses in ring

#### Laurent Bartholdi (Mar 22 2021 at 20:51):

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 (Mar 22 2021 at 21:09):

The mul_assoc rewrite is not failing

#### Patrick Massot (Mar 22 2021 at 21:10):

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

#### Patrick Massot (Mar 22 2021 at 21:11):

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 (Mar 22 2021 at 21:12):

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 (Mar 22 2021 at 21:13):

And library_search does know it:

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


Last updated: May 15 2021 at 02:11 UTC