Tactic for proving simple inequalities (in ℕ∞)

Stream: Is there code for X?

[Lessness]

I'm trying to prove that from H1: a <= 1 and H2: b <= 1 the goal a+b<=2 follows.
For now I'm not very successful. :sweat_smile:

Which tactic should I use?

[Lessness]

I've heard that Omega isn't ready yet, but maybe there is something less powerful?

[Kevin Buzzard]

linarith

[Lessness]

Oh, those were ℕ∞, not Nat. That explains much.

[Lessness]

I have such goal, caused by my choice to use encard:

S1: Set V
S2: Set V
T1: Set V
T2: Set V
H7: Set.encard S1 ≤ Set.encard T1
H8: Set.encard S2 ≤ Set.encard T2
H9: Set.encard T1 ≤ 1
H10: Set.encard T2 ≤ 1
⊢ Set.encard S1 + Set.encard S2 ≤ 2

Any suggestions?

[Damiano Testa]

Does apply (add_le_add H7 H8).trans work?

[Lessness]

Ooo, yes! It changes the goal to Set.encard T1 + Set.encard T2 ≤ 2

[Damiano Testa]

So, one more step and you should get to 1 + 1 ≤ 2!

[Lessness]

Thank you very much! :)
Yes, it's done.

[Lessness]

(I will put this here, too, to avoid too many topics.)
How can I prove this? Thanks in advance.

neighbors: Set V
H0: Set.encard neighbors ≤ 2
⊢ Set.encard neighbors = 0 ∨ Set.encard neighbors = 1 ∨ Set.encard neighbors = 2

[Ruben Van de Velde]

Does fin_cases Set.encard neighbors <;> simp work? Probably not in ℕ∞

[Lessness]

Right now it causes error unexpected syntax. Do I need to import something?

[Ruben Van de Velde]

Mathlib.Tactic.FinCases

[Lessness]

Still unexpected syntax, at least for me. It seems that it isn't working, not with ℕ∞ :(

[Lessness]

I almost proved it, using theorem Set.encard_le_coe_iff, but I still have one sorry.

import Mathlib

def test (w: Nat) (h: w ≤ 2): w = 0 ∨ w = 1 ∨ w = 2 := by
  linarith
  sorry

Here linarith does not want to work. :| Any suggestions?

[Lessness]

For now I proved it by destructing w enough times.

[Shreyas Srinivas]

import Mathlib.Tactic

theorem test (w: Nat) (h: w ≤ 2): w = 0 ∨ w = 1 ∨ w = 2 := by
  interval_cases w
  ·  left; rfl;
  ·  right;left;rfl;
  ·  right;right;rfl;
  done

[Shreyas Srinivas]

Much shorter:

import Mathlib.Tactic

theorem test (w: Nat) (h: w ≤ 2): w = 0 ∨ w = 1 ∨ w = 2 := by
  interval_cases w <;> simp only
  done

[Shreyas Srinivas]

A third option which uses tauto:

import Mathlib.Tactic

theorem test (w: Nat) (h: w ≤ 2): w = 0 ∨ w = 1 ∨ w = 2 := by
  interval_cases w <;> tauto
  done

[Ruben Van de Velde]

Oh duh, I was thinking of interval_cases, not fin_cases. Sorry for the confusion

[Lessness]

Thank you!