Why doesn't this simp work?

Stream: lean4

[Markus Schmaus]

The following three examples look all very similar to me and can be proven by a combination of Nat.add_le_add and the given hypotheses, but only in the first two example is simp [Nat.add_le_add, *] successful. Why is that? And how could this be fixed?

example {a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : Nat}
    (h₁ : a₁ ≤ b₁) (h₂ : a₂ ≤ b₂) (h₃ : a₃ ≤ b₃) (h₄ : a₄ ≤ b₄) :
    a₁ + a₂ + (a₃ + a₄) ≤ b₁ + b₂ + (b₃ + b₄) :=
  by
    simp [Nat.add_le_add, *]

example {a₁ a₂ a₃ b₁ b₂ b₃ : Nat}
    (h₁ : a₁ ≤ b₁) (h₂ : a₂ ≤ b₂) (h₃ : a₃ ≤ b₃) :
    a₁ + a₂ + a₃ ≤ b₁ + b₂ + b₃ :=
  by
    simp [Nat.add_le_add, *]

example {a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : Nat}
    (h₁ : a₁ ≤ b₁) (h₂ : a₂ ≤ b₂) (h₃ : a₃ ≤ b₃) (h₄ : a₄ ≤ b₄) :
    a₁ + a₂ + a₃ + a₄ ≤ b₁ + b₂ + b₃ + b₄ :=
  by
    simp [Nat.add_le_add, *] -- simp makes no progress

[Alex J. Best]

simp isn't really intended for proving goals like this (where the proof is essentially a _nested_ sequence of lemma applications). simp instead tries to prove things by rewriting, usually using equality or iff (or some other equivalence relation at best).
What's happening in your proofs is that simp sees a lemma it can apply, and recursively calls simp to prove the side conditions. By default simp uses a fairly conservative limit on how many times it repeats this process, as it is normally used to discharge side goals which are much easier to prove than the original. You can override this if you like

example {a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : Nat}
    (h₁ : a₁ ≤ b₁) (h₂ : a₂ ≤ b₂) (h₃ : a₃ ≤ b₃) (h₄ : a₄ ≤ b₄) :
    a₁ + a₂ + a₃ + a₄ ≤ b₁ + b₂ + b₃ + b₄ :=
  by
    simp (config := {maxDischargeDepth := 6}) [Nat.add_le_add, *]

but much better is to use a tool that is meant for this job, like

example {a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : Nat}
    (h₁ : a₁ ≤ b₁) (h₂ : a₂ ≤ b₂) (h₃ : a₃ ≤ b₃) (h₄ : a₄ ≤ b₄) :
    a₁ + a₂ + a₃ + a₄ ≤ b₁ + b₂ + b₃ + b₄ :=
  by
    apply_rules [Nat.add_le_add]

[Markus Schmaus]

Thanks for the explanation, this makes sense. How come apply_rules isn't used more often? I have been looking at a lot of proofs in core and Mathlib lately, and I have never seen this tactic.

[Kevin Buzzard]

I guess your example is quite artificial? Also apply_rules is probably being used under the hood in tactics like aesop and aesop_cat, which are being applied invisibly to solve goals in certain structure fields which aren't being supplied by the user.