more induction related questions

Stream: new members

[Robert hackman]

Hi,
so I'm still working on the induction examples. This time with unequal signs.

mve:

example (n : ℕ): ∑ k in Finset.Ico 1 n.succ, ((k - 1 )^2 : ℕ ) < ((Nat.zero + 1) ^ (3: ℕ) : ℚ) / 3 := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[Finset.sum_Ico_succ_top]
    rw[← succ_eq_add_one]
    rw[ih]
    rw[succ_eq_add_one]

There is an error at rw[ih] which says that it can't find the target expression. Although it's clearly there, but it's embedded in Rat.blt so maybe that's the problem. If the rewrite is successfull I want to finish the goal by using Nat.succ_lt_succ`. Is that a viable way to go? regards

[Kevin Buzzard]

Natural subtraction is pathological like natural division so you can't expect things to be easy. Also you're making your life more difficult by insisting on summing from 1 to n and then taking away 1, instead of summing from 0 to n-1. As I said several times last week when I was in a field and unable to post code, you should coerce into the rationals immediately if you want these things to be as easy as they are on paper. In particular I'm very strongly of the opinion that this goal should look like

example (n : ℕ): ∑ k in Finset.Ico 1 n.succ, ((k : ℚ) - 1 )^2 ...

As for your current problem, the rw tactic will only consume equalities and iff statements. Think about what the rw tactic does to understand why. In particular it will not consume a statement of the from X < Y (which is what you're feeding it with ih) so you need to rethink your mathematical proof.

[Kevin Buzzard]

Oh, it's probably also worth remarking that your example is of course not at all true: if n is huge then a sum of a bunch of squares is clearly going to be > 1/3.

[Robert hackman]

Ok so about the whole type thing, I'm not yet thinkting in those dimension but I adapted my code.
I can't sum from 0 to n-1 because the statement is not true for 0.

The logic error was a stupid mistake, this is the correct version where it's not ... < ((Nat.zero + 1) ^ 3 ... but ... < ((n + 1) ^ 3 ...
example (n : ℕ): ∑ k in Finset.Ico 1 n.succ, (((k : ℚ) - 1 )^2) < ((n + 1) ^ (3: ℕ) : ℚ) / 3 := by

So I will start to sarch for something that does rewrites for lt

[Kevin Buzzard]

You can sum k from 0 to <n instead of summing k-1 from 1 to <n+1, this doesn't change anything, this is just a change of variables

[Robert hackman]

ah uff sure, sorry

[Robert hackman]

So I've really really tried but am not getting anywhere. So I understand why rewrite doesn't work, instead I think I have to prove thorugh manual calc or some unequality theorem that the replaced(or rewritten) version is true. I've tried to use add_lt_add_right but since I'm trying to prove induction, a+b<c doesn't work because the c is c(n+1) for the goal and c(n) for the induciton hypothisis. I'm probably on the completely wrong track. Any help or tips would be greatly appreciated!

[Kevin Buzzard]

Can you please post a #mwe containing your current work (click on the link to see the details of what this is)? That is the best way to ask questions here.

[Kevin Buzzard]

"can someone help me fill in this sorry in this fully working code" is a better question than "help me I am stuck"

[Moritz Firsching]

The statement in the example does not seem to be true:

example (n : ℕ): ∑ k in Finset.Ico 1 n.succ, ((k - 1 )^2 : ℕ ) < ((Nat.zero + 1) ^ (3: ℕ) : ℚ) / 3

You can check the left hand side and the right hand side:

def n := 2
#eval ∑ k in Finset.Ico 1 n.succ, ((k - 1)^2 : ℕ ) -- gives`1`
#eval ((Nat.zero + 1) ^ (3: ℕ) : ℚ) / 3 --gives (1: Rat)/3

[Kevin Buzzard]

By the way Robert, Lean does not do maths for you -- Lean checks your maths. So is your question "I can't get Lean to understand a maths proof I know" or is it "I don't know how to prove this theorem myself"?

[Robert hackman]

This is the mwe, the first one is obv. false, this one should be correct.

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Data.Num.Lemmas
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.FieldSimp
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Nat.Interval
import Mathlib.Order.LocallyFinite

open Num
open BigOperators
open Finset
open Nat
example (n : ℕ): ∑ k in Finset.Ico 0 n.succ, (((k + 1 : ℚ) - 1 )^2) < (((n + 1) ^ (3: ℕ) : ℚ) / 3 : ℚ) := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[Finset.sum_Ico_succ_top]
    rw[← succ_eq_add_one]
    case succ =>
      rw[add_lt_add_right ih]

      sorry
      -- rw[ih]
      -- rw[add_lt_add_right]
      -- sorry
    case succ.hab => sorry

[Robert hackman]

Kevin Buzzard said:

By the way Robert, Lean does not do maths for you -- Lean checks your maths. So is your question "I can't get Lean to understand a maths proof I know" or is it "I don't know how to prove this theorem myself"?

I do understand this basic induciton, but fail to translate it into the language, any other humiliations you want me to admit? I've put many many hours into the lang and am starting to make sense of the syntax/ logic, please don't let me down lol.

[Mario Carneiro]

Could you explain the proof strategy to us informally?

[Mario Carneiro]

The error I get on that MWE is that add_lt_add_right ih is a proof of a < statement and rw takes equality statements

[Mario Carneiro]

calc is probably the clearest way to go about this:

    case succ =>
      calc
        ∑ k in Finset.Ico 0 n.succ, ((k + 1 : ℚ) - 1) ^ 2 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2
        _ < ↑((n + 1) ^ 3) / 3 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2 := add_lt_add_right ih _
        _ < ↑((Nat.succ n + 1) ^ 3) / 3 := ?_
      sorry

[Mario Carneiro]

or if you like golfing:

    case succ =>
      apply (add_lt_add_right ih _).trans
      sorry

[Robert hackman]

This is very informal though, as thought.
First you show that the sum of k=1 to n +1 (k-1)^2 <... can be written as k=1 to n (k-1)^2 + (n+1-1)^2 <..., then you replace k=1 to n (k-1)^2part of above equation with the ih and prove that thourgh simplifcation until you have smth like n > 0. That's the paper way I guess.

[Robert hackman]

thank you so much for the help!

[Robert hackman]

Really good to know that the add_lt_add_right was the right choice at least I just didn't know how to use it

[Kevin Buzzard]

Yeah, rw eats a list of proofs but each proof must be either an iff or an equality: its job is to replace X by Y so X had better be equal to Y.

[Kyle Miller]

I'm not sure which import you need precisely, but with the whole kitchen sink import Mathlib.Tactic you can replace add_lt_add_right ih _ with by gcongr. It sort of does rewrites with inequalities (or more accurately, it knows the names of lemmas like add_lt_add_right so you don't have to)

[Mario Carneiro]

It also reminds me that generalized rewriting came up a lot in iris-lean, there is a rw' tactic which allows you to rewrite with any kind of transitive relation using a gcongr-like traversal

[Mario Carneiro]

it would be nice if simp supported other relations, it has basically all the tools it needs to do so

[Kevin Buzzard]

gsimp

[Robert hackman]

Ok, I spend another 10 hours and didn't move a cm lol.
So up front here is my mve:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Data.Num.Lemmas
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.FieldSimp
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Nat.Interval
import Mathlib.Order.LocallyFinite

open Num
open BigOperators
open Finset
open Nat

example (n : ℕ): ∑ k in Finset.Ico 0 n.succ, (((k + 1 : ℚ) - 1 )^2) < (((n + 1) ^ (3: ℕ) : ℚ) / 3 : ℚ) := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[Finset.sum_Ico_succ_top]
    rw[← succ_eq_add_one]
    case succ =>
      calc
        ∑ k in Finset.Ico 0 n.succ, ((k + 1 : ℚ) - 1) ^ 2 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2
        _ < ↑((n + 1) ^ 3) / 3 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2 := add_lt_add_right ih _
      field_simp
      rw[div_lt_div_iff]
      case calc.step.b0 =>
        norm_num
      case calc.step.d0 =>
        norm_num
      ring_nf
      simp
      calc
        n * 27 < n * 36 + 12 := by ring_nf
    case succ.hab =>
      sorry

basically I'm currently completely overwhelemed trying to proof 12 + ↑n * 27 < 24 + ↑n * 36(without using gsimp...).
There are many tactics that proof variations of a + b < a + c(or theorems with iff exists) but none for rings (at least I couldn't find them). My idea now was to isolate and simplify until I get some sporadic enlightment or something like that but I'm also failing on that, so any suggestions would be welcome. regards

[Yaël Dillies]

There are many tactics that proof variations of a + b < a + c (or theorems with iff exists) but none for rings

Have you tried the lemmas you found which you thought were not for rings?

[Robert hackman]

yeah I tried many but none worked, I also understand (now...) why they don't work. Edit: I found a few lemmas it was more that I couldn't figure out how to transfrom the term..

[Kevin Buzzard]

The code is full of errors for me. Can you make it error-free by sorrying all the problems rather than just letting them error?

[Kevin Buzzard]

OK so it wasn't too bad to fix the errors: here's one way of finishing the proof.

import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Tactic.FieldSimp

open BigOperators
open Nat

example (n : ℕ): ∑ k in Finset.Ico 0 n.succ, (((k + 1 : ℚ) - 1 )^2) < (((n + 1) ^ (3: ℕ) : ℚ) / 3 : ℚ) := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[Finset.sum_Ico_succ_top]
    rw[← succ_eq_add_one]
    case succ =>
      calc
        ∑ k in Finset.Ico 0 n.succ, ((k + 1 : ℚ) - 1) ^ 2 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2
        _ < ↑((n + 1) ^ 3) / 3 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2 := add_lt_add_right ih _
      field_simp
      rw[div_lt_div_iff]
      case calc.step.b0 =>
        norm_num
      case calc.step.d0 =>
        norm_num
      ring_nf
      simp
      norm_cast
      linarith
    case succ.hab =>
      simp

(note that you don't need all those imports)

[Robert hackman]

Thank you so much. What's confusing to me is that without norm_cast, linarith throws linarith failed to find a contradiction, but if I understand correctly, norm_cast is really only mutating types, that's why I thought the term's pattern wasn't "compatible"(without understanding why...) with linarith

[Alex J. Best]

Well the fact that 12 + q * 27 < 24 + q * 36 isn't true for all rational numbers q. So without the norm_cast step (which essentially makes the argument that 12 + n * 27 < 24 + n * 36 for natural numbers interpreted as rationals if and only if the same inequality over the naturals) linarith doesn't know how to conclude as it doesn't work out that the casts of n must be nonnegative. After norm_cast the correcponding goal is more suitable for linarith
One could argue that linarith should know that a natural number treated as a rational is nonnegative, but it seems it currently doesn't.

[Robert hackman]

Yeah that makes sense, thx!

[Robert hackman]

So I want do finish the example with a manual more insightful proof than linarith (for learning purposes). Apperantly, when just simplifying one can use iff to proof the simplification. Why is that? I thought everyhting would need to be proofed or that just axioms applying?
Now I'm stuck at -9 < 12/n since it's a type missmatch which I don't want to resolve. Instead I want to proof at that point that this Prop is true since it cannot be 12/n cannot get negative, how would I do that?

Here is my mve:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Data.Num.Lemmas
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.FieldSimp
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Nat.Interval
import Mathlib.Order.LocallyFinite

open Num
open BigOperators
open Finset
open Nat

example (n : ℕ): ∑ k in Finset.Ico 0 n.succ, (((k + 1 : ℚ) - 1 )^2) < (((n + 1) ^ (3: ℕ) : ℚ) / 3 : ℚ) := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[Finset.sum_Ico_succ_top]
    rw[← succ_eq_add_one]
    case succ =>
      calc
        ∑ k in Finset.Ico 0 n.succ, ((k + 1 : ℚ) - 1) ^ 2 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2
        _ < ↑((n + 1) ^ 3) / 3 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2 := add_lt_add_right ih _
      field_simp
      rw[div_lt_div_iff]
      case calc.step.b0 =>
        norm_num
      case calc.step.d0 =>
        norm_num
      ring_nf
      simp
      -- norm_cast
      calc
        -- 12 + ↑n * 27 < 24 + ↑n * 36 -- - 12
        27 * n < 12 + ↑n * 36 ↔ -- /n
        27 < 12/n + 36 ↔ -- -36
        (-9: ℚ) < 12/n ↔ -- /12

    case succ.hab =>
      simp

[Kevin Buzzard]

Can you post code with sorrys (and comments saying "this is the sorry I am stuck on") rather than errors, which are very confusing?

[Robert hackman]

Sure, I hope that’s more understandable

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Data.Num.Lemmas
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.FieldSimp
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Nat.Interval
import Mathlib.Order.LocallyFinite

open Num
open BigOperators
open Finset
open Nat

example (n : ℕ): ∑ k in Finset.Ico 0 n.succ, (((k + 1 : ℚ) - 1 )^2) < (((n + 1) ^ (3: ℕ) : ℚ) / 3 : ℚ) := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[Finset.sum_Ico_succ_top]
    rw[← succ_eq_add_one]
    case succ =>
      calc
        ∑ k in Finset.Ico 0 n.succ, ((k + 1 : ℚ) - 1) ^ 2 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2
        _ < ↑((n + 1) ^ 3) / 3 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2 := add_lt_add_right ih _
      field_simp
      rw[div_lt_div_iff]
      case calc.step.b0 =>
        norm_num
      case calc.step.d0 =>
        norm_num
      ring_nf
      simp
      -- norm_cast
      calc
        -- 12 + ↑n * 27 < 24 + ↑n * 36 -- - 12
        27 * n < 12 + ↑n * 36 ↔ -- /n
        27 < 12/n + 36 := by sorry -- -substract 36 and proof of that the natural right side cannot be smaller than the negative left side
       --  (-9: ℚ) < 12/n ↔ -- /12

    case succ.hab =>
      simp

[Alex J. Best]

It looks like the division operation here is the division of natural numbers (where 1 / 2 = 0 as it outputs a natural number).
That's probably not what you want (its not a very well behaved function).
use 12/(n : ℚ) so that lean treats your numbers as rationals before dividing

[Alex J. Best]

You also have a bunch of errors earlier and later in the snippet which I think just confuse things (and leans error reporting).
Try and focus on one sorry at a time, maybe stating things as separate lemmas if needed.

[Alex J. Best]

You'll also probably need to split into cases based on whether n is zero or not, as that will likely be a requirement to apply many lemmas about divisibility

[Robert hackman]

Regarding the bunch of errors, there's that expected := (at line case succ.hab) error that I really don't understand. Even when I'm finishing the last line in succ n ihin the scope of the calc with sorry it's still there. I can't really get rid of it. Up to just now I thought that when I'm prooving the code in the (last)calc section, it would go away but not event than apperantly, I relly can't get rid of it if I'm using the calc mode

[Robert hackman]

example (n : ℕ): ∑ k in Finset.Ico 0 n.succ, (((k + 1 : ℚ) - 1 )^2) < (((n + 1) ^ (3: ℕ) : ℚ) / 3 : ℚ) := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[Finset.sum_Ico_succ_top]
    rw[← succ_eq_add_one]
    case succ =>
      calc
        ∑ k in Finset.Ico 0 n.succ, ((k + 1 : ℚ) - 1) ^ 2 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2
        _ < ↑((n + 1) ^ 3) / 3 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2 := add_lt_add_right ih _
      field_simp
      rw[div_lt_div_iff]
      case calc.step.b0 =>
        norm_num
      case calc.step.d0 =>
        norm_num
      ring_nf
      simp
      -- norm_cast
      -- linarith
      calc
        12 + ↑n * 27 < 24 + ↑n * 36 := by linarith
    case succ.hab =>
      simp

for example throws the error expected := , at line case succ.hab and this version:

example (n : ℕ): ∑ k in Finset.Ico 0 n.succ, (((k + 1 : ℚ) - 1 )^2) < (((n + 1) ^ (3: ℕ) : ℚ) / 3 : ℚ) := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[Finset.sum_Ico_succ_top]
    rw[← succ_eq_add_one]
    case succ =>
      calc
        ∑ k in Finset.Ico 0 n.succ, ((k + 1 : ℚ) - 1) ^ 2 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2
        _ < ↑((n + 1) ^ 3) / 3 + ((Nat.succ n : ℚ) + 1 - 1) ^ 2 := add_lt_add_right ih _
      field_simp
      rw[div_lt_div_iff]
      case calc.step.b0 =>
        norm_num
      case calc.step.d0 =>
        norm_num
      ring_nf
      simp
      -- norm_cast
      -- linarith
      calc
        12 + ↑n * 27
        _ < 24 + ↑n * 36 := by linarith
    case succ.hab =>
      simp

throws invalid 'calc' step, failed to synthesize Trans instance Trans LT.lt LT.lt ?m.1047at the second calc statement although it's technically the same (I think)

[Kevin Buzzard]

I think you don't have the right syntax for calc. Search for examples in the source code.

[Kevin Buzzard]

Here's an example from mathematics in Lean:

theorem my_lemma4 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  calc
    |x * y| = |x| * |y| := sorry
    _ ≤ |x| * ε := sorry
    _ < 1 * ε := sorry
    _ = ε := sorry

Note that the first line is an equality, not a number.

[Robert hackman]

So I'm just very confused at that point.
I want to simplify by transforming both sides of the equasion, for example substracting 12, then dividing both sides by n and then 12.
I spend some time now reading thorugh docs and am still not certain which way to read it.
So I will just assume now that when stating an in- or equality that it always refers to the left side of the equasion and that all of what I wrote above is wrong.

But how do I go about transforming both sides then?

[Damiano Testa]

Are you referring to your latest post? This seems to work and maybe it is useful.

example (n : ℕ): ∑ k in Finset.Ico 0 n.succ, (((k + 1 : ℚ) - 1 )^2) < (((n + 1) ^ (3: ℕ) : ℚ) / 3 : ℚ) := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[Finset.sum_Ico_succ_top (Nat.zero_le ..)]
    rw[← Nat.succ_eq_add_one]
    have := _root_.add_lt_add_right ih (((Nat.succ n : ℚ) + 1 - 1) ^ 2)
    apply this.trans_le
    field_simp
    apply div_le_div ?_ ?_ zero_lt_three rfl.le
    · positivity
    · ring_nf
      apply add_le_add_right
      apply add_le_add_right
      apply add_le_add
      · norm_num
      · norm_cast
        apply Nat.mul_le_mul rfl.le (by decide)

[Robert hackman]

Damiano Testa said:

Are you referring to your latest post? This seems to work and maybe it is useful.

example (n : ℕ): ∑ k in Finset.Ico 0 n.succ, (((k + 1 : ℚ) - 1 )^2) < (((n + 1) ^ (3: ℕ) : ℚ) / 3 : ℚ) := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[Finset.sum_Ico_succ_top (Nat.zero_le ..)]
    rw[← Nat.succ_eq_add_one]
    have := _root_.add_lt_add_right ih (((Nat.succ n : ℚ) + 1 - 1) ^ 2)
    apply this.trans_le
    field_simp
    apply div_le_div ?_ ?_ zero_lt_three rfl.le
    · positivity
    · ring_nf
      apply add_le_add_right
      apply add_le_add_right
      apply add_le_add
      · norm_num
      · norm_cast
        apply Nat.mul_le_mul rfl.le (by decide)

thank you, this is super interesting! Will take me some time to fully understand it

[Robert hackman]

oh this is so cool thanks again, that was exactly what I was looking for!

[Robert hackman]

(deleted)

[Robert hackman]

So I really wanted to have the n > 0part explicetly in the paramters instead of putting +1 all over the goal, that's what I came up with (works..)
But the one thing I don't understand about my code and @Damiano Testa example is the apply add_le_add_right/ add_le_add/ mul_le_mul part. Not because I don't understand the hypothesis but because after applying it, the common parts of the equation are just cut away, but the theorem or the tactitc doesn't state that in anyway, why is it transformed in that way then?

example (n : ℕ) (h: n ≥ 1): ∑ k in Finset.Ico 1 n, ((k - 1 : ℚ) ^ 2) < ((n ^ (3: ℕ) : ℚ) / 3 : ℚ) := by
  cases' h
  case refl =>
    simp
  case step n h =>
    induction n, h using le_induction with
    | base =>
      simp
      norm_num
    | succ n h ih =>
      rw[← succ_eq_add_one]
      have succ_zero_le_succ_one: 1 ≤ Nat.succ (n) := by
        apply succ_le_succ (Nat.zero_le n)
      rw[Finset.sum_Ico_succ_top (succ_zero_le_succ_one ..)]

      have := _root_.add_lt_add_right ih (((Nat.succ n : ℚ) - 1) ^ 2)
      apply this.trans_le

      field_simp
      rw[div_le_div_iff (by norm_num) (by norm_num)]
      ring_nf
      apply add_le_add_right
      apply add_le_add_right
      apply _root_.add_le_add
      · norm_num
      · norm_cast
        apply mul_le_mul rfl.le (by decide)
        norm_num
        apply Nat.zero_le

[Damiano Testa]

I'm on mobile, so I what I is ever more subject to error than normal. The lemmas add_le_add/... prove an inequality of the form a+b ≤ c+d from inequalities of the form a ≤ c and b ≤ d. However, depending on the exact form of add_le_add that you use, say a=c in your case, some of the required inequalities are just true because they are equalities (really, someone proved this once and then you can use the more specialised result).

This is indicated but the right/left suffix that you see in the name of the lemma.

[Damiano Testa]

So, in such situations, if you use the more specialised lemma, some of the proof obligations are already done for you.

[Robert hackman]

Ok that explains why there are "missing"/ non explicit proofs, but I still don't understand why, when the hypothysis is applied, it also substitutes a. Every time add_le_add_right is applied, the goal is simpliefied through the removal of the equal parts on both sides. Is "apply" doing that?

[Ruben Van de Velde]

Is the question about the code you pasted yesterday? Which line exactly is confusing?

[Robert hackman]

yep the last example I posted (since there is no line numeration), this is the part I'm talking about(below ring_nf):

...
 apply add_le_add_right
      apply add_le_add_right
      apply _root_.add_le_add
      · norm_num
...

[Ruben Van de Velde]

So if you look at the definition of add_le_add_right:

#check add_le_add_right
-- add_le_add_right.{u_1} {α : Type u_1} [inst✝ : Add α] [inst✝¹ : LE α]
--   [i : CovariantClass α α (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1] {b c : α}
--   (bc : b ≤ c) (a : α) :
--   b + a ≤ c + a

then you see it states that, under various assumptions that happen to be true for the natural numbers, if b ≤ c, then also b + a ≤ c + a. (In particular, this is because naturals are nonnegative.)

[Ruben Van de Velde]

What the apply tactic does is say: "I'm trying to prove an assertion P and I have a lemma that says that Q implies P. Thanks to that lemma, it's sufficient to prove Q, so change my current goal to Q"

[Ruben Van de Velde]

Does that clarify a bit?

[Robert hackman]

ok, I think I'm a bit at loss :D
But I'm correct in the assumption that the substraction of a(referring to a in add_le_add_right) is done through the apply tactic to get closer to the goal? :melting_face:

[Kevin Buzzard]

No subtraction ever occurs. Cancellation occurs, which is something different.

[Kevin Buzzard]

One way of proving cancellation is using subtraction, but that is not what is being used here, because subtraction on the naturals is poorly behaved.