ReflGen (r ⊓ Ne)

Stream: Is there code for X?

[Snir Broshi]

A seemingly trivial theorem that I'm struggling to prove:

import Mathlib
theorem foo {α : Type*} (r : α → α → Prop) :
    Relation.ReflGen (r ⊓ Ne) = Relation.ReflGen r := by
  sorry

grind doesn't seem to work, it can't even prove ∀ a b, r a b ∧ a ≠ b → (r ⊓ Ne) a b.
Are there any theorems under Relation which help this? The most relevant one I found is docs#Relation.reflGen_iff but it's still painful to prove the statement after it.

[Snir Broshi]

This works but it's meh

import Mathlib
theorem foo {α : Type*} (r : α → α → Prop) :
    Relation.ReflGen (r ⊓ Ne) = Relation.ReflGen r := by
  ext a b
  simp only [Relation.reflGen_iff, Pi.inf_apply, inf_Prop_eq]
  grind

[Kenny Lau]

import Mathlib

theorem foo {α : Type*} (r : α → α → Prop) :
    Relation.ReflGen (r ⊓ Ne) = Relation.ReflGen r := by
  ext; simpa [Relation.reflGen_iff] using by tauto

[Kenny Lau]

Snir Broshi said:

This works but it's meh

import Mathlib
theorem foo {α : Type*} (r : α → α → Prop) :
    Relation.ReflGen (r ⊓ Ne) = Relation.ReflGen r := by
  ext a b
  simp only [Relation.reflGen_iff, Pi.inf_apply, inf_Prop_eq]
  grind

what's wrong with this? you've done the canonical things here, you used simp to convert the statement to a sensible form and then used grind when the goal was logically obvious