Seemingly obvious algebraic fact, unsolved by "ring" tactic.

Stream: general

[Eric Chen]

I'm trying to prove the following theorem, and I heard that the Ring tactic should solve the problem directly. However, the goal shows something that is purely an algebraic fact that I don't understand. Why doesn't Ring solve this, and how could I solve this?
Screenshot-2024-03-10-at-3.13.33PM.png
Thank you so much!

[Eric Chen]

My intuition is that it's something to do with the fact that we need n % 3 = 1, but I don't know how or where I could utilize this in the definition of A.

[Ruben Van de Velde]

Right, this is non-obvious because / rounds; (1 / 3) * 3 = 0 * 3 = 0, not 1

[Ruben Van de Velde]

I think you can rewrite with docs#Int.ediv_mul_cancel

[Eric Chen]

That worked :). However, now it wants me to show that 3 | -1 + n, which sounds like a direct application of h2. However, "apply" and "rw" both don't work for this task.

[Matt Diamond]

docs#Int.dvd_sub_of_emod_eq should help there

[Matt Diamond]

you might need to rewrite with add_comm (so that the goal is 3 | n + -1)

[Eric Chen]

Solved, thank you all so much :). I'm new to Lean, and this gives me some intuition about which tactics/theorems to use.

[Kevin Buzzard]

The answer to "why doesn't ring work" is "your goal is not a statement of commutative ring theory" (as it involves division)

[Xiyu Zhai]

Do we have field tactics?

[Daniel Weber]

Kevin Buzzard said:

The answer to "why doesn't ring work" is "your goal is not a statement of commutative ring theory" (as it involves division)

Why does example (x : ℝ) : x/3 * 3 = x := by ring work, then? I think it's a bit stronger

[Daniel Weber]

Xiyu Zhai said:

Do we have field tactics?

There's field_simp

[Ruben Van de Velde]

I'm surprised that it does

[Ruben Van de Velde]

Daniel Weber said:

Xiyu Zhai said:

Do we have field tactics?

There's field_simp

But note that your question didn't involve field division

[Kevin Buzzard]

A preprocessor changes x / (numerical constant c known to be nonzero) in a field to x * (c^{-1}). It won't work with x / y if y isn't numerical. It's like how omega only claims to work with goals without multiplication, but it works on 3 * n because it changes it to n + n + n.

[Mario Carneiro]

more specifically, ring works with multivariate polynomials over $\mathbb{Q}$, and $1/3\in \mathbb{Q}$

[Kim Morrison]

@Eric Chen, please read #mwe, and post questions with standalone code blocks, not screenshots. You'll get much better help.