linarith should split And

[MrQubo]

lean-live

In a proof of example (a b : Nat) (_ : a ≤ b ∧ b ≤ c) (_ : 0 < a) (_ : c < 3) : 0 < a ∧ a < 3 I have to use apply And.intro and then apply linarith separately to both goals. I think we could consider automatically splitting And with linarith.

One problem I can see, is that linarith is able to prove one part of And, and not the other, it would still fail. It might be a good idea to also report in the error which parts it managed to solve.

[b-mehta]

Note that linarith +splitHypotheses does this for And in a hypothesis, which solves half the problem, and avoids the complication of your last paragraph.

[MrQubo]

@b-mehta +splitHypotheses is the default. In the example I gave linarith did successfully used conjuction a ≤ b ∧ b ≤ c hypothesis to prove subgoals 0 < a and a < 3.
My issue is only about the fact, that it couldn't prove 0 < a ∧ a < 3 without splitting to subgoals first.