Interesting behavior of `simp`

Stream: new members

[Bbbbbbbbba]

import Mathlib

open symmDiff

example {A B C : Set ℕ} (h : C = A ∩ B) : C ∆ (A \ C) = A := by
  -- simp [h] -- Results in (A ∩ B) ∆ (A \ B) = A
  simp; simp [h]

example {A B C : Set ℕ} (h : C = A ∩ B) : A = C ∆ (A \ C) := by
  -- simp [h] -- Results in A = (A ∩ B) ∆ (A \ B)
  simp; simp [h] -- Results in A = A ∩ B ∪ A
  ext; simp; exact fun h1 h2 ↦ h1

[Jakub Nowak]

Hm, looks like simp cannot apply Set.union_eq_right if the goal is t = s ∪ t.
We could add Set.right_eq_union : t = s ∪ t ↔ s ⊆ t to mathlib, but maybe we could fix simp to treat = as symmetrical and work the same regardless of order? Tbh, I though that simp already does that.

[Violeta Hernández]

simp works best if you keep to idiomatic Lean, in particular meaning that complex expressions go on the LHS.

[Bbbbbbbbba]

Hmm, I never noticed that before. Although I just noticed that if I write h as h : A ∩ B = C then I have to use simp [← h].

[Bbbbbbbbba]

I also found it interesting that a single simp [h] does not work.