Embarrassingly simple question about Mathlib example

Stream: new members

[Martin Gilchrist]

Hi - this really a two-part question. First, what is the best forum in which to ask simple questions about the Mathlib tutorial? Secondly, I am having difficulty with one example in the Rings section: it asks, show

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by

I think this should be done by a rw clause, but the first thing I want to do is to add -a to the left of each side of the hypothesis, but I can't work out how to express this. I'm sure this is a simple question, but don't yet have the conceptual mindset to do this.

Thanks for any help! Martin

[Pedro Sánchez Terraf]

Hi! #new members is the right place for beginner's questions (perhaps you can move this thread to that channel). You can also use backtics to make your code more readable:

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by

[Pedro Sánchez Terraf]

One idea for this exercise (which actually belongs to Section 2, Basics, of MIL) is to start by rewriting the goal using one of the previous two theorems.

Working at the hypothesis h is also feasible, but you'll learn about that later on.

[Notification Bot]

This topic was moved here from #lean4 > Embarrassingly simple question about Mathlib example by Kyle Miller.

[Kyle Miller]

(@Martin Gilchrist Moved!)

[Martin Gilchrist]

Hi - thanks, Pedro and Kyle - I am sorry, but I just don't understand what it means to "rewrite the goal"! Can you give me an example of how I would (left) add -a to h in order to start the re-writing process? Apologies for really dumb questions.

[Richard Copley]

import Mathlib

variable (R : Type*) [AddCommGroup R]

theorem add_left_cancel' {a b c : R} (h : a + b = a + c) : b = c := by
  rw [← (add_right_injective a).eq_iff]
  sorry

[Yaël Dillies]

Richard, I think this uses too much compared to what the exercise is intending.

[Yaël Dillies]

@Martin Gilchrist, you can start with rw [← add_neg_cancel_right b a].

[Martin Gilchrist]

@Yaël Dillies Thanks - I have proved add_neg_cancel_right, and so I added the following with your hint:

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
rw [← add_neg_cancel_right b a, add_assoc, zero_add]

which I feel should give me three rewrites: -a + a + b = -a + a + c then (-a + a) + b = (-a + a) + c then 0 + b = 0 + c then b = c but instead I get an error that the tactic did not find instance of pattern (see screenshot). I think I must be missing some understanding here.

image.png

Any help would be appreciated. Thanks, Martin

[Matt Diamond]

I can explain why you're getting that issue, but I'm curious why you're trying to rewrite the goal from b = c back to b = c

[Matt Diamond]

if you click after each comma in the rw block, you can see the effect of each individual rewrite in the infoview, which might help clarify things

[Ruben Van de Velde]

There's no 0 + ... anywhere to be seen, so why do you think zero_addapplies?

[Ruben Van de Velde]

But also Matt's point

[Ruben Van de Velde]

You need to get to a point where you can rewrite with h, so you need to get a+b in your goal somehow

[Martin Gilchrist]

@Matt Diamond Hi, Matt - I would really appreciate your help here. Your comment about clicking after each comma is very useful, but as you can see from the following screenshot, I think I have got to the point b = c, but I still see a red underline under by indicating that I have not proved the theorem! I think I'm not clear about what you mean by trying to rewrite from b = c back to b = c because I think I am going from a + b = a+ c to b = c . Am I not?

image.png

[Yaël Dillies]

Yes, you managed to reduce b = c to proving b = c. As Ruben pointed out, this is not what you want to be doing.

[Matt Diamond]

I think I am going from a + b = a+ c to b = c . Am I not?

@Martin Gilchrist rw [] operates on the goal, which is b = c... to rewrite the hypothesis h : a + b = a + c, you would use rw [] at h

[Matt Diamond]

however, you don't necessarily need to rewrite h... you can also solve this by rewriting the goal using h

[Matt Diamond]

the strategy that Ruben is suggesting is to rewrite the goal so that it includes a + b, and then do rw [h]

[Matt Diamond]

also, I think you might have a misunderstanding of how the goal works in the info view... ⊢ b = c doesn't mean that you've proved b = c, it means that b = c is the thing you need to prove

[Martin Gilchrist]

@Matt Diamond and @Yael and @Ruben Van de Velde I am really sorry, and I don't mean to be a pain, but I don't understand what you mean by use rw [] at h. I tried the following (see screenshot) in which I have at h at the end of the line, and I am trying to (I think) add -a to the left of each side of h, but try as I might, I cannot get the syntax right.

image.png

I have tried variations using the left arrow and using a b but I'm afraid that I am missing something syntactical about Lean. It might save time all around, if you can show me a simple solution, and then I can puzzle through the syntax by myself rather than take up your time?

[Matt Diamond]

@Martin Gilchrist No need to apologize! Here's a solution:

import Mathlib

variable (R : Type*) [AddCommGroup R]

theorem add_left_cancel' {a b c : R} (h : a + b = a + c) : b = c := by
  rw [← add_neg_cancel_right b a, add_comm b a, h, add_comm a c, add_neg_cancel_right]

[Martin Gilchrist]

@Matt Diamond Thanks, and I assume that the h in the rw clause is an example of "using h" that you mentioned earlier?

Anyway, @Matt Diamond @Yaël Dillies @Ruben Van de Velde I do appreciate your patience with me. This has been a learning experience for me, and reconfirms my appreciation of the helpfulness and responsiveness of the Lean community!

[Matt Diamond]

I assume that the h in the rw clause is an example of "using h" that you mentioned earlier?

yes, exactly... hypotheses can be used just like any other lemma or theorem

[Ruben Van de Velde]

Essentially the proof here is $b = 0 + b = (-a + a) + b = -a + (a + b) = -a + (a + c) = (-a + a) + c = 0 + c = c$