-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem lapMatrix_toLinearMap₂' [Field R] [CharZero R] (x : V → R) :
    toLinearMap₂' R (G.lapMatrix R) x x =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j)^2 else 0) / 2

Proof state:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ ((∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
        ∑ y : V, ∑ x_1 : V, if G.Adj y x_1 then x x_1 * x x_1 - x x_1 * x y else 0) /
      2 =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
simp_rw [← sum_add_distrib, ite_add_ite]

Result:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ (∑ x_1 : V,
        ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 + (x x_2 * x x_2 - x x_2 * x x_1) else 0 + 0) /
      2 =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Proof state:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ (∑ x_1 : V,
        ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 + (x x_2 * x x_2 - x x_2 * x x_1) else 0 + 0) /
      2 =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
congr 2 with i

Result:
case e_a.e_f.h
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i : V
⊢ (∑ x_1 : V, if G.Adj i x_1 then x i * x i - x i * x x_1 + (x x_1 * x x_1 - x x_1 * x i) else 0 + 0) =
    ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0

Proof state:
case e_a.e_f.h.e_f.h
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i j : V
⊢ (if G.Adj i j then x i * x i - x i * x j + (x j * x j - x j * x i) else 0 + 0) =
    if G.Adj i j then (x i - x j) ^ 2 else 0

Tactic:
ring_nf

Result:
no goals

Proof state:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ ((∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
        ∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) /
      2 =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
conv_lhs => enter [1,2,2,i,2,j]; rw [if_congr (adj_comm G i j) rfl rfl]

Result:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ ((∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
        ∑ i : V, ∑ j : V, if G.Adj j i then x i * x i - x i * x j else 0) /
      2 =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Proof state:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ (((toLinearMap₂' R) (lapMatrix R G)) x) x = (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
simp_rw [toLinearMap₂'_apply', lapMatrix, sub_mulVec, dotProduct_sub, dotProduct_mulVec_degMatrix,
  dotProduct_mulVec_adjMatrix, ← sum_sub_distrib, degree_eq_sum_if_adj, sum_mul, ite_mul, one_mul,
  zero_mul, ← sum_sub_distrib, ite_sub_ite, sub_zero]

Result:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ (∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Proof state:
case e_a.e_f.h
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i : V
⊢ (∑ x_1 : V, if G.Adj i x_1 then x i * x i - x i * x x_1 + (x x_1 * x x_1 - x x_1 * x i) else 0 + 0) =
    ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0

Tactic:
congr 2 with j

Result:
case e_a.e_f.h.e_f.h
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i j : V
⊢ (if G.Adj i j then x i * x i - x i * x j + (x j * x j - x j * x i) else 0 + 0) =
    if G.Adj i j then (x i - x j) ^ 2 else 0

Proof state:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ ((∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
        ∑ i : V, ∑ j : V, if G.Adj j i then x i * x i - x i * x j else 0) /
      2 =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
conv_lhs => enter [1,2]; rw [Finset.sum_comm]

Result:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ ((∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
        ∑ y : V, ∑ x_1 : V, if G.Adj y x_1 then x x_1 * x x_1 - x x_1 * x y else 0) /
      2 =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Proof state:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ (∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
rw [← add_self_div_two (∑ x_1 : V, ∑ x_2 : V, _)]

Result:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ ((∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) +
        ∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) /
      2 =
    (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2