Matrix on edge set for graphs

Stream: Is there code for X?

[Gabriel Moise]

Hello!
I am trying to define the incidence matrix of a graph, but currently fail to do so using the edge set of the graph. Is there any code for that i.e. where the edge set of the graph is used as a fintype for the matrix?

variables (G : simple_graph V) [decidable_rel G.adj] [decidable_eq V]  [preorder V]

-- Some attempts, unsuccessful
--variables (E : finset (sym2 V))
--def E := G.edge_set.to_finset

def incidence_matrix : matrix V E ℤ
| i e := if e ∈ (G.incidence_finset i) then 1 else 0

What I am currently struggling is creating E such that E is a fintype, and also E is the edge set of V so that I can define the incidence matrix of G properly.

[Johan Commelin]

@Alena Gusakov @Kyle Miller will probably know. But I think the adjacency matrix is already defined somewhere.

[Gabriel Moise]

Yes, but the adjancency matrix is defined on the set of vertices V, what I am looking for is a matrix defined on the edge set, if that makes sense.

[Johan Commelin]

Ooh, sorry. I don't know much about graphs

[Johan Commelin]

Can you use {e // e \in G.edge_set}?

[Johan Commelin]

That should give you a type, and hopefully Lean figures out automatically that it is finite if V is finite.

[Gabriel Moise]

So, although we have from the simple_graph file that:

def edge_set : set (sym2 V) := sym2.from_rel G.sym

When I define my set E as:

def E : set (sym2 V) := {e // e ∈ G.edge_set} -- btw what does // mean? is it like the mathematical notation {x | x \in \N, x < 3} or something like that?

I get the error

type mismatch, term
  {e // e ∈ G.edge_set}
has type
  Type u : Type (max 1 (u+1))
but is expected to have type
  set (sym2 V) : Type u

[Johan Commelin]

matrix expects a type n with an instance fintype n. you are trying to feed it a set.

[Johan Commelin]

{x // condition on x} creates a Type* which you can then use for matrix.

[Johan Commelin]

But it still needs the fintype instance.

[Gabriel Moise]

Oh, now I see. Ok, so after the fixes, the thing that is left is this:

def E := {e // e ∈ G.edge_finset}
def inc_matrix : matrix V E ℤ

which gives the error:

type mismatch at application
  matrix V E
term
  E
has type
    Type ? : Type (max ? 1 (?+1))
but is expected to have type
  Type ? : Type (?+1)

Can you please explain what the error means? I often come across error messages like this, but can't see what they precisely mean.

[Eric Wieser]

Lean definitely can't find fintype E there, as you hid it behind a def

[Alena Gusakov]

I wonder if you might be able to just have [fintype G.edge_set] for this?

[Alena Gusakov]

I know fintype/finset stuff is really annoying

[Gabriel Moise]

Can't seem to make it work with that idea, this is how I managed to do it for now, I know it's ugly, but I will improve it when I myself improve at Lean probably :smile:

def E : Type u := {e // e ∈ G.edge_set}

instance edges_fintype' [decidable_eq V] [fintype V] [decidable_rel G.adj] :
  fintype G.E := subtype.fintype _

instance has_mem : has_mem V G.E := { mem := λ v e, v ∈ e.val }

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.E ℤ -- maybe use ℕ instead of ℤ?
| i e := if i ∈ e then 1 else 0

Oh, and I don't seem to find any library containing directed graphs, since I might need them to define the directed incidence matrix. Is there some work in progress towards that? (this is just for learning purposes towards my project, don't want to copy anybody :smile: )

[Kyle Miller]

I'd suggest not defining E and instead use Lean's auto-coercion feature:

import combinatorics.simple_graph.basic
import linear_algebra.matrix

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set ℤ -- maybe use ℕ instead of ℤ?
| i e := if i ∈ e.val then 1 else 0

(By the way, there's also e.val ∈ G.incidence_set i for indicating that an edge and a vertex are incident. It means exactly the same thing as i ∈ e.val but potentially has more useful lemmas about it.)

[Kyle Miller]

Gabriel Moise said:

Oh, and I don't seem to find any library containing directed graphs, since I might need them to define the directed incidence matrix. Is there some work in progress towards that? (this is just for learning purposes towards my project, don't want to copy anybody :smile: )

There's nothing about directed graphs yet. For directed incidence matrices, I've thought it would be nice if there were a type of directed simple graphs, a function to simple_graph that forgets orientations, and a function to prove/calculate things about simple graphs by giving a proof/calculation for directed graphs and a proof that changing the orientation of an edge doesn't change the result. This could be how you'd use directed incidence matrices for a simple graph. (One example: calculate the graph Laplacian from $II^T$ for $I$ a directed incidence matrix of a directed version of a given simple graph.)

[Peter Nelson]

By the time you are talking about an incidence matrix, it will get increasingly cumbersome to think of edges as certain pairs of vertices. Instead, you can model a graph as an incidence structure on a vertex type V and an edge type E together with some some incidence information (such as inc : V \to E \to \nat or head : E \to V, tail : E \to V), the flavour of which could capture simple graphs, multigraphs, digraphs, hypergraphs, etc etc. Defining an incidence matrix is easy if you set things up this way. For directed graphs, I personally like inc : V \to E \to int which takes values 1 and -1.

In some areas of graph theory, such as when you're thinking about induced subgraphs and complements, an edge really 'is' a pair of vertices. However, in other cases, you really want to think of edges as their own entities that are not syntactically bound to vertices. If you want an incidence matrix, this strongly suggests to me that you're in the latter situation.

[Gabriel Moise]

Kyle Miller said:

I'd suggest not defining E and instead use Lean's auto-coercion feature:

import combinatorics.simple_graph.basic
import linear_algebra.matrix

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set ℤ -- maybe use ℕ instead of ℤ?
| i e := if i ∈ e.val then 1 else 0

(By the way, there's also e.val ∈ G.incidence_set i for indicating that an edge and a vertex are incident. It means exactly the same thing as i ∈ e.val but potentially has more useful lemmas about it.)

Following this approach, I get into some trouble with type coercions, for example, here I want to prove something quite simple :

lemma degree_equals_sum_of_incidence_row {i : V} : G.degree i = ∑ (e : G.edge_set), G.inc_matrix i e :=
begin
  unfold inc_matrix,
  simp [finset.sum_ite],
  rw ← card_incidence_set_eq_degree,
  sorry
end

which is very similar to what is already done in the simple_graph module, however I stumble upon the following thing:

fintype.card ↥(G.incidence_set i) = (filter (λ (x : ↥(G.edge_set)), ↑x ∈ G.incidence_set i) univ).card

which is what is left to be proven, but I can't seem to get it done, as I am not very experienced with coercions. My fear is that I will encounter this a lot and it would make code look messy.

[Yakov Pechersky]

Can you give a #mwe?

[Gabriel Moise]

Peter Nelson said:

By the time you are talking about an incidence matrix, it will get increasingly cumbersome to think of edges as certain pairs of vertices. Instead, you can model a graph as an incidence structure on a vertex type V and an edge type E together with some some incidence information (such as inc : V \to E \to \nat or head : E \to V, tail : E \to V), the flavour of which could capture simple graphs, multigraphs, digraphs, hypergraphs, etc etc. Defining an incidence matrix is easy if you set things up this way. For directed graphs, I personally like inc : V \to E \to int which takes values 1 and -1.

In some areas of graph theory, such as when you're thinking about induced subgraphs and complements, an edge really 'is' a pair of vertices. However, in other cases, you really want to think of edges as their own entities that are not syntactically bound to vertices. If you want an incidence matrix, this strongly suggests to me that you're in the latter situation.

With this approach, I see that I can do something like

structure graph (V : Type u) (E : Type v) :=
(incidence : V → E → ℤ)

However, if I want to define a simple_graph as a special case for the more general graph (I am not sure it is necessary for me to do that though, just felt it might be needed), I thought this would work:

def simple_graph (V : Type u) [decidable_eq V] : graph V (sym2 V) :=
{incidence := λ i e, if (i ∈ e) ∧ (¬ sym2.is_diag e) then 1 else 0}

However, this looks much more "unfriendly" than the usual structure of a simple_graph from the library and it doesn't look like I can do much with it right away.

[Gabriel Moise]

Yakov Pechersky said:

Can you give a #mwe?

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators matrix
open finset matrix simple_graph

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set ℕ
| i e := if e.val ∈ G.incidence_set i then 1 else 0

lemma degree_equals_sum_of_incidence_row {i : V} : G.degree i = ∑ (e : G.edge_set), G.inc_matrix i e :=
begin
  unfold inc_matrix,
  simp [finset.sum_ite],
  rw ← card_incidence_set_eq_degree,
  sorry,
end

end simple_graph

[Yakov Pechersky]

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set ℕ -- maybe use ℕ instead of ℤ?
| i e := if i ∈ e.val then 1 else 0

lemma inc_matrix_def : G.inc_matrix = λ i e, ite (i ∈ e.val) 1 0 := rfl

lemma mem_edge_set_of_incidence {G : simple_graph V} {e : sym2 V} {v : V}
  (h : e ∈ G.incidence_set v) : e ∈ G.edge_set :=
set.mem_of_mem_inter_left h

lemma degree_equals_sum_of_incidence_row {i : V} : G.degree i = ∑ (e : G.edge_set), G.inc_matrix i e :=
begin
  rw inc_matrix_def,
  simp only [finset.sum_ite, add_zero, mul_one, nat.cast_id, finset.sum_const, nsmul_eq_mul, finset.sum_const_zero,
  subtype.val_eq_coe],
  rw ← card_incidence_set_eq_degree,
  have : G.incidence_set i = G.incidence_finset i,
    { ext, simp },
  simp_rw this,
  have := fintype.card_coe (G.incidence_finset i),
  convert this using 1,
  { congr },
  { refine finset.card_congr _ _ _ _,
    { intros e he,
      exact e },
    { intros e he,
      simpa [incidence_finset, incidence_set] using he },
    { intros e1 e2 he1 he2 h,
      ext,
      simp only at h,
      simp [h] },
    { intros e he,
      rw mem_incidence_finset at he,
      use [e, mem_edge_set_of_incidence he],
      refine ⟨_, _⟩,
      { simpa [incidence_set] using he.right },
      { simp } } }
end

end simple_graph

[Yakov Pechersky]

That's solving your current problem. I had to provide two tiny pieces of API.

[Yakov Pechersky]

In general, I think there are likely better ways to phrase it such that you don't have to juggle between fintype, finsets, and various coercions.

[Yakov Pechersky]

Here's another version, pick your poison.

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set ℕ -- maybe use ℕ instead of ℤ?
| i e := if (e : sym2 V) ∈ G.incidence_set i then 1 else 0

lemma inc_matrix_def : G.inc_matrix = λ i e, ite ((e : sym2 V) ∈ G.incidence_set i) 1 0 := rfl

lemma mem_edge_set_of_incidence {G : simple_graph V} {e : sym2 V} {v : V}
  (h : e ∈ G.incidence_set v) : e ∈ G.edge_set :=
set.mem_of_mem_inter_left h

lemma degree_equals_sum_of_incidence_row {i : V} : G.degree i = ∑ (e : G.edge_set), G.inc_matrix i e :=
begin
  rw inc_matrix_def,
  rw ← card_incidence_set_eq_degree,
  simp only [finset.sum_boole, nat.cast_id],
  refine finset.card_congr _ _ _ _,
  { rintros ⟨e, he⟩ he',
    exact ⟨e, mem_edge_set_of_incidence he⟩ },
  { rintros ⟨e, he⟩ he',
    simpa using he },
  { rintros ⟨e1, he1⟩ ⟨e2, he2⟩ he1' he2' h,
    ext,
    simp only [subtype.mk_eq_mk] at h,
    simp [h], },
  { rintros ⟨e, he⟩ he',
    use [e],
    { simpa using he' },
    { simp } }
end

end simple_graph

[Gabriel Moise]

Woah, thank you very much! I will try to use a different approach, cause this is actually a lot of work for such a result, so I guess I need a change.

[Yakov Pechersky]

If you check the simps, you'll see absolutely no content about graphs

[Yakov Pechersky]

So that just means some finset/fintype API is missing

[Yakov Pechersky]

One minute

[Yakov Pechersky]

Like so:

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators

lemma fintype.card_coe_filter {α : Sort*} {s t : set α} [fintype s] [fintype t]
  [decidable_pred (λ (x : t), (x : α) ∈ s)] (h : s ⊆ t) :
  fintype.card s = finset.card (finset.filter (λ (x : t), (x : α) ∈ s) finset.univ) :=
begin
  refine finset.card_congr _ _ _ _,
  { rintros ⟨e, he⟩ he',
    exact ⟨e, h he⟩ },
  { rintros ⟨e, he⟩ he',
    simpa only [true_and, finset.mem_univ, finset.mem_filter] using he},
  { rintros ⟨e1, he1⟩ ⟨e2, he2⟩ he1' he2' hr,
    ext,
    simp only [subtype.mk_eq_mk] at hr,
    simp only [hr] },
  { rintros ⟨e, he⟩ he',
    use [e],
    { simpa only [true_and, finset.mem_univ, finset.mem_filter] using he'},
    { simp only [finset.mem_univ, exists_prop_of_true] } }
end

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set ℕ -- maybe use ℕ instead of ℤ?
| i e := if (e : sym2 V) ∈ G.incidence_set i then 1 else 0

lemma inc_matrix_def : G.inc_matrix = λ i e, ite ((e : sym2 V) ∈ G.incidence_set i) 1 0 := rfl

lemma mem_edge_set_of_incidence {G : simple_graph V} {e : sym2 V} {v : V}
  (h : e ∈ G.incidence_set v) : e ∈ G.edge_set :=
set.mem_of_mem_inter_left h

lemma incidence_subset_edge_set (G : simple_graph V) (v : V) : G.incidence_set v ⊆ G.edge_set :=
λ _, set.mem_of_mem_inter_left

lemma degree_equals_sum_of_incidence_row {i : V} : G.degree i = ∑ (e : G.edge_set), G.inc_matrix i e :=
begin
  rw [inc_matrix_def, ←card_incidence_set_eq_degree],
  simpa using fintype.card_coe_filter (G.incidence_subset_edge_set i)
end

end simple_graph

[Yakov Pechersky]

Now you can see that your statement is very simple, and is just the result of the simple implication that any incidence_set is definitionally a subset of the edge_set.

[Gabriel Moise]

Oh, I see what you mean. So, I should either get used to working with finsets and fintypes to continue with this model, or choose a different model.

[Yakov Pechersky]

I see this as just part of the formalization. You have to identify which pieces of what you're working on are the "mathematical content" and which is the "fomalization plumbing". Separating out the two is the skill I've had to gain to be able to do the formalizations I am interested in

[Yakov Pechersky]

In addition, graphs might be some of the more frustrating things in formalization because of the constant jumps between objects, subobjects, choice, finite vs infinite, many different "induction principles"

[Yakov Pechersky]

And working with concrete objects too.

[Gabriel Moise]

Well, I guess I will become good at them with experience and I will see what tools I need to formalize what I want. I will see what I can do to progress with what you proved for me! Thank you again! :smile:

[Kyle Miller]

By the way, incidence_subset_edge_set already exists as simple_graph.incidence_set_subset.

import combinatorics.simple_graph.basic
import linear_algebra.matrix

lemma fintype.card_coe_filter {α : Sort*} {s t : set α} [fintype s] [fintype t]
  [decidable_pred (λ (x : t), (x : α) ∈ s)] (h : s ⊆ t) :
  fintype.card s = (finset.filter (λ (x : t), (x : α) ∈ s) finset.univ).card :=
begin
  refine finset.card_congr _ _ _ _,
  { exact λ ⟨e, he⟩ _, ⟨e, h he⟩ },
  { rintros ⟨e, he⟩ _,
    simpa only [true_and, finset.mem_univ, finset.mem_filter] using he },
  { rintros ⟨e1, he1⟩ ⟨e2, he2⟩ _ _ hr,
    simpa only [subtype.mk_eq_mk] using hr },
  { rintros ⟨e, he⟩ he',
    simpa only [true_and, exists_prop, finset.mem_univ, set_coe.exists,
      subtype.mk_eq_mk, exists_eq_right, finset.mem_filter] using he' }
end

open_locale big_operators

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set ℕ :=
λ i e, if (e : sym2 V) ∈ G.incidence_set i then 1 else 0

lemma degree_equals_sum_of_incidence_row {i : V} :
  G.degree i = ∑ (e : G.edge_set), G.inc_matrix i e :=
by rw [inc_matrix, finset.sum_boole, nat.cast_id,
       ←fintype.card_coe_filter (G.incidence_set_subset i), card_incidence_set_eq_degree]

end simple_graph

[Gabriel Moise]

Can I get some help with this, I encounter this situation very often, when I have to prove stuff about the sum of elements from a type, but I struggle with splitting the sum into two parts based on some property: in the following case, I know that the sum can be split into the sum where x is not the edge between i and j (in which case the sum is 0) and the sum (consisting of one element) when x is the edge (therefore the sum will be 1) and altogether the sum will equal 1 as I need. Can you give me a direction regarding this kind of problems?

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set ℕ -- maybe use ℕ instead of ℤ?
| i e := if (e : sym2 V) ∈ G.incidence_set i then 1 else 0

lemma inc_matrix_def : G.inc_matrix = λ i e, ite ((e : sym2 V) ∈ G.incidence_set i) 1 0 := rfl

lemma adj_sum_of_prod_inc_one {i j : V} :
G.adj i j → ∑ (x : ↥(G.edge_set)), G.inc_matrix i x * G.inc_matrix j x = 1 :=
begin
  intro hyp,
  -- If x is the edge between i and j, then the product is 1, else it is 0, and since there is only
  -- one edge between i and j, the sum will be 1
  sorry
end

end simple_graph

[Johan Commelin]

There is finset.sum_filter that might be helpful for that

[Eric Wieser]

Your statement is probably easier to prove as:

def inc_matrix : matrix V (sym2 V) ℕ := -- maybe use ℕ instead of ℤ?
λ i e, if e ∈ G.incidence_set i then 1 else 0

lemma inc_matrix_def : G.inc_matrix = λ i e, ite ((e : sym2 V) ∈ G.incidence_set i) 1 0 := rfl

lemma adj_sum_of_prod_inc_one {i j : V} :
G.adj i j → ∑ x in G.edge_finset, G.inc_matrix i x * G.inc_matrix j x = 1 :=

The subtype and coercion stuff is a distraction

[Eric Wieser]

This is a good start:

lemma adj_sum_of_prod_inc_one {i j : V} :
G.adj i j → ∑ x in G.edge_finset, G.inc_matrix i x * G.inc_matrix j x = 1 :=
begin
  intro hyp,
  have : ⟦(i, j)⟧ ∈ G.edge_finset := (G.mem_edge_finset _).mpr hyp,
  rw ←finset.insert_erase this,
  rw finset.sum_insert (finset.not_mem_erase _ _),
  convert add_zero 1,
  { sorry, },
  { apply finset.sum_eq_zero,
    intros x hx,
    rw finset.mem_erase at hx,
    sorry}
end

[Gabriel Moise]

Wouldn't it be a mistake to define the incidence matrix on the whole sym2 V type? Like it's definition is on the edge set of the graph from what I know.

[Yakov Pechersky]

When defined over the whole sym2 V type, you'll just have all zero columns

[Gabriel Moise]

Yes, I see that, but I thought it would have been better to follow the mathematical definition of the incidence matrix, but I guess that this solves me a lot of coercion problems since I don't have the G.edge_set type anymore.

[Eric Wieser]

You're always free to have separate inc_matrix' and inc_matrix definitions, where one is the mathetmatically "clean" one, while the other is the one that is easy to prove things about

[Eric Wieser]

Then all you need is a lemma saying how they relate to each other

[Kyle Miller]

@Gabriel Moise There's a missing graph theory lemma that makes this easier. After that, the main (non-math) complexity is to get things into the right form for finset.filter_eq.

import combinatorics.simple_graph.basic
import linear_algebra.matrix

open_locale big_operators

universe u

variables {V : Type u} [fintype V] [decidable_eq V]
variables (G : simple_graph V) [decidable_rel G.adj]

namespace simple_graph

/-- `inc_matrix G` is the matrix `M` with `∀ i ∈ V, ∀ e ∈ V x V :` :
` | M i e = 1` if `i` is endpoint of `e`
` | M i e = 0` otherwise -/
def inc_matrix : matrix V G.edge_set ℕ :=
λ i e, if (e : sym2 V) ∈ G.incidence_set i then 1 else 0

lemma inc_matrix_apply (i : V) (e : G.edge_set) :
  G.inc_matrix i e = if (e : sym2 V) ∈ G.incidence_set i then 1 else 0 := rfl

lemma mem_incidence_sets_iff_eq_of_adj {i j : V} (h : G.adj i j) (e : sym2 V) :
  e ∈ G.incidence_set i ∧ e ∈ G.incidence_set j ↔ e = ⟦(i, j)⟧ :=
begin
  refine quotient.rec_on_subsingleton e (λ p, _),
  rcases p with ⟨v, w⟩,
  rw sym2.eq_iff,
  simp only [incidence_set],
  tidy,
end

lemma adj_sum_of_prod_inc_one {i j : V} (h : G.adj i j) :
  ∑ (e : G.edge_set), G.inc_matrix i e * G.inc_matrix j e = 1 :=
begin
  simp only [inc_matrix_apply, ←ite_and, G.mem_incidence_sets_iff_eq_of_adj h,
    finset.sum_boole, nat.cast_id, boole_mul],
  have key := congr_arg finset.card (finset.filter_eq finset.univ (⟨⟦(i, j)⟧, h⟩ : G.edge_set)),
  simp only [finset.mem_univ, if_true, finset.card_singleton] at key,
  convert key,
  ext x,
  cases x,
  simp only [subtype.coe_mk],
  exact eq_comm,
end

end simple_graph

[Gabriel Moise]

There is also one thing that always appears in my proofs and I always improvise with lemma's that I create specifically for the current thing I am solving, but I was wondering if there is a simple proof for this:

import linear_algebra.matrix

open_locale big_operators

universe u
variables {V : Type u} [fintype V]

lemma sum_simplification {x : V} (f g : V -> ℤ) (h : V → ℤ -> ℤ) (P : V → Prop)
[decidable_pred P] :
∑ (x : V), h x (ite (P x) (f x) (g x)) =
∑ (x : V), ite (P x) (h x (f x)) (h x (g x)) :=
begin
  sorry,
end

It is close to the lemma "sum_apply_ite", however there the function h that is applied is independent of x. I apologize for the narrowing to \Z, but this will perfectly do for my work. I don't need a full solution, some hints are more than welcomed as well :smile:

[Eric Wieser]

I think you want docs#apply_ite?

[Gabriel Moise]

Oh I forgot about working on the internal elements, thank you so much! :smile: