gcongr does not work with ite

Stream: mathlib4

[Michael Stoll]

I'd expect this to work, but it fails:

import Mathlib

open Classical

example (P : ℕ → Prop) (n : ℕ) {a b : ℝ} (h : a ≤ b) :
    (if P n then 0 else a) ≤ if P n then 0 else b := by
  gcongr -- gcongr did not make progress

Is there an easy fix?

[Edward van de Meent]

use split

[Eric Wieser]

I think we could add a lemma for this for gcongr

[Eric Wieser]

Though this doesn't work either

import Mathlib

@[gcongr]
theorem  ite_le_ite {α : Type*} (P : Prop) [Decidable P] [LE α] {a b c d : α} (h : a ≤ c) (h : b ≤ d):
    (if P then a else b) ≤ if P then c else d := by
  split <;> assumption

example (P : ℕ → Prop) [DecidablePred P] (n : ℕ) {a b : ℝ} (h : a ≤ b) :
    (if P n then 0 else a) ≤ if P n then 0 else b := by
  gcongr

[Heather Macbeth]

You need to add more gcongr lemmas, for the other possible choices for the set of "varying arguments":

@[gcongr]
theorem ite_le_ite_left {α : Type*} (P : Prop) [Decidable P] [Preorder α] {a b c : α} (h : a ≤ c) :
    (if P then a else b) ≤ if P then c else b :=
  ite_le_ite P h (le_refl _)

@[gcongr]
theorem ite_le_ite_right {α : Type*} (P : Prop) [Decidable P] [Preorder α] {a b d : α} (h : b ≤ d) :
    (if P then a else b) ≤ if P then a else d :=
  ite_le_ite P (le_refl _) h

[Eric Wieser]

Would it be possible to make that clearer in the docstring, or am I guilty of not being able to read?

[Eric Wieser]

(also, I'm struggling to work out what @[gcongr wat] means, which appears to be legal syntax)

[Michael Stoll]

Where should these lemmas go to make it work with, say, import Mathlib.Tactic?