Symmetric difference of two subgraphs

Stream: Is there code for X?

[Lessness]

Hello! Here is tiny code.
1) Is there already a definition that can be used instead of XOR that's defined here?
2) What's the best way to replace use of theorem aux with some tactics?
3) How to show Lean that it can get from instances [DecidableRel M1.Adj] and [DecidableRel M2.Adj] to instance [DecidableRel (GraphSymmDiff M1 M2).Adj]?

import Mathlib

def XOR (P1 P2: Prop): Prop := P1 ∧ ¬ P2 ∨ ¬ P1 ∧ P2

theorem aux {V} {G: SimpleGraph V} (M: G.Subgraph): ∀ (x y: V), M.Adj x y → G.Adj x y := by
  induction M
  simp
  assumption

def GraphSymmDiff {V} {G: SimpleGraph V} (M1 M2: G.Subgraph): G.Subgraph :=
  SimpleGraph.Subgraph.mk
  (@Set.univ V)
  (fun x y => XOR (M1.Adj x y) (M2.Adj x y))
  (by
    intros x y H
    simp [XOR] at H
    let W1 := aux M1 x y
    let W2 := aux M2 x y
    tauto)
  (by
    intros x y H
    simp)
  (by
    simp [Symmetric, XOR]
    intros x y H
    tauto)

[Kevin Buzzard]

For aux you don't want a tactic -- this is a theorem in the API for subgraphs:

theorem aux {V} {G: SimpleGraph V} (M: G.Subgraph) (x y: V) :
    M.Adj x y → G.Adj x y :=
  SimpleGraph.Subgraph.adj_sub M

If you like, the tactic is exact?

[Kyle Miller]

Usually we write M.adj_sub for this (and note that docs#SimpleGraph.Subgraph.adj_sub is one of the axioms for a subgraph)

[Kyle Miller]

What's the definition of the symmetric difference of two subgraphs? It doesn't seem right to set it to have V be the vertex set. It's ignoring the vertex sets of M1 and M2.

[Lessness]

1) Thank you both!
2) I was interested in the edges only, so it seemed okay to leave V. :thinking: :question:

[Kyle Miller]

Be sure then that you are interested in G.Subgraph then rather than those H : SimpleGraph V such that H ≤ G. For SimpleGraph V, if you have G G' : SimpleGraph V, then you should be able to write G ∆ G' for the symmetric difference, assuming you have the module for docs#symmDiff imported.