awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Fintype (Sym2 α)
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Semiring R
inst_4 : (a : α) → Fintype (↑(G.neighborSet a) : Type u_2)
a b : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = if a = b then (↑(G.degree a) : R) else if G.Adj a b then 1 else 0
have pos : ∀ (h : a = b), (incMatrix R G * (incMatrix R G)ᵀ) a b = (↑(G.degree a) : R)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Fintype (Sym2 α)
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Semiring R
inst_4 : (a : α) → Fintype (↑(G.neighborSet a) : Type u_2)
a b : α
pos : ∀ (h : a = b), (incMatrix R G * (incMatrix R G)ᵀ) a b = (↑(G.degree a) : R)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = if a = b then (↑(G.degree a) : R) else if G.Adj a b then 1 else 0
have pos₁ : ∀ (h : ¬a = b) (h' : G.Adj a b), (incMatrix R G * (incMatrix R G)ᵀ) a b = 1
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Fintype (Sym2 α)
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Semiring R
inst_4 : (a : α) → Fintype (↑(G.neighborSet a) : Type u_2)
a b : α
pos : ∀ (h : a = b), (incMatrix R G * (incMatrix R G)ᵀ) a b = (↑(G.degree a) : R)
pos₁ : ∀ (h : ¬a = b) (h' : G.Adj a b), (incMatrix R G * (incMatrix R G)ᵀ) a b = 1
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = if a = b then (↑(G.degree a) : R) else if G.Adj a b then 1 else 0
have neg : ∀ (h : ¬a = b) (h' : ¬G.Adj a b), (incMatrix R G * (incMatrix R G)ᵀ) a b = 0
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.IncMatrix (goal)
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : Fintype (Sym2 α)
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Semiring R
inst_4 : (a : α) → Fintype (↑(G.neighborSet a) : Type u_2)
a b : α
h : a = b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = (↑(G.degree a) : R)
have pos : (incMatrix R G * (incMatrix R G)ᵀ) a a = (↑(G.degree a) : R)
Tactic: subst b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : NonAssocSemiring α
inst_1 : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
⊢ A.IsHermitian
have a : ∀ (i j : V), Aᴴ i j = A i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : NonAssocSemiring α
inst_1 : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
i j : V
⊢ Aᴴ i j = A i j
have a : ∀ (heq : A i j = 0), Aᴴ i j = A i j
Tactic: rcases h.zero_or_one i j with heq | heq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
α : Type u_1
V : Type u_2
inst : NonAssocSemiring α
inst_1 : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
i j : V
a : ∀ (heq : A i j = 0), Aᴴ i j = A i j
⊢ Aᴴ i j = A i j
have a₁ : ∀ (heq : A i j = 1), Aᴴ i j = A i j
Tactic: rcases h.zero_or_one i j with heq | heq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
R : Type u_3
inst_2 : AddCommMonoidWithOne R
i : V
⊢ Eq.{u_3 + 1} (α := R) (↑(card.{u_1} (α := V) (Set.toFinset {w : V | G.Adj i w})) : R)
    (∑ j : V, if G.Adj i j then 1 else 0)
have rw : Eq.{u_3 + 1} (α := R) (↑(card.{u_1} (α := V) (Set.toFinset {w : V | G.Adj i w})) : R)
  (↑(card.{u_1} (α := V) {x : V | G.Adj i x}) : R)
Tactic: rw [sum_boole, Set.toFinset_setOf]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
R : Type u_3
inst_2 : AddCommMonoidWithOne R
i : V
rw :
  Eq.{u_3 + 1} (α := R) (↑(card.{u_1} (α := V) (Set.toFinset {w : V | G.Adj i w})) : R)
    (↑(card.{u_1} (α := V) {x : V | G.Adj i x}) : R)
⊢ Eq.{u_3 + 1} (α := R) (↑(card.{u_1} (α := V) (Set.toFinset {w : V | G.Adj i w})) : R)
    (∑ j : V, if G.Adj i j then 1 else 0)
have rw₁ : Eq.{u_3 + 1} (α := R) (↑(#(filter (G.Adj i) univ)) : R) (↑(card.{u_1} (α := V) {x : V | G.Adj i x}) : R)
Tactic: rw [sum_boole, Set.toFinset_setOf]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : NonAssocSemiring R
v : V
vec : V → R
⊢ (degMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v
have rw : ((diagonal fun (x : V) ↦ (↑(G.degree x) : R)) *ᵥ vec) v = (↑(G.degree v) : R) * vec v
Tactic: rw [degMatrix, mulVec_diagonal]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : NonAssocSemiring R
v : V
vec : V → R
rw : ((diagonal fun (x : V) ↦ (↑(G.degree x) : R)) *ᵥ vec) v = (↑(G.degree v) : R) * vec v
⊢ (degMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v
have rw₁ : (↑(G.degree v) : R) * vec v = (↑(G.degree v) : R) * vec v
Tactic: rw [degMatrix, mulVec_diagonal]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : NonAssocRing R
v : V
vec : V → R
⊢ (lapMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
have simp_rw : ((degMatrix R G - adjMatrix R G) *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
Tactic: simp_rw [lapMatrix, sub_mulVec, Pi.sub_apply, degMatrix_mulVec_apply, adjMatrix_mulVec_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : NonAssocRing R
v : V
vec : V → R
simp_rw : ((degMatrix R G - adjMatrix R G) *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
⊢ (lapMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
have simp_rw₁ : (degMatrix R G *ᵥ vec - adjMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
Tactic: simp_rw [lapMatrix, sub_mulVec, Pi.sub_apply, degMatrix_mulVec_apply, adjMatrix_mulVec_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : NonAssocRing R
v : V
vec : V → R
simp_rw : ((degMatrix R G - adjMatrix R G) *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
simp_rw₁ :
  (degMatrix R G *ᵥ vec - adjMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
⊢ (lapMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
have simp_rw₂ : (degMatrix R G *ᵥ vec) v - (adjMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
Tactic: simp_rw [lapMatrix, sub_mulVec, Pi.sub_apply, degMatrix_mulVec_apply, adjMatrix_mulVec_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : NonAssocRing R
v : V
vec : V → R
simp_rw : ((degMatrix R G - adjMatrix R G) *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
simp_rw₁ :
  (degMatrix R G *ᵥ vec - adjMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
simp_rw₂ :
  (degMatrix R G *ᵥ vec) v - (adjMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
⊢ (lapMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
have simp_rw₃ : (↑(G.degree v) : R) * vec v - (adjMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v - ∑ u ∈ G.neighborFinset v, vec u
Tactic: simp_rw [lapMatrix, sub_mulVec, Pi.sub_apply, degMatrix_mulVec_apply, adjMatrix_mulVec_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : NonAssocRing R
⊢ (lapMatrix R G *ᵥ fun (x : V) ↦ 1) = 0
have h : ∀ (i : V), (lapMatrix R G *ᵥ fun (x : V) ↦ 1) i = 0 i
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : NonAssocRing R
i : V
⊢ (lapMatrix R G *ᵥ fun (x : V) ↦ 1) i = 0 i
have h : HMul.hMul (α := R) (↑(G.degree i) : R) 1 - ∑ u ∈ G.neighborFinset i, 1 = 0 i
Tactic: rw [lapMatrix_mulVec_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
⊢ ((((((toLinearMap₂' R : Matrix V V R ≃ₗ[R] (V → R) →ₗ[R] (V → R) →ₗ[R] R) :
                    (a : Matrix V V R) → (V → R) →ₗ[R] (V → R) →ₗ[R] R)
                  (lapMatrix R G) :
                (V → R) →ₗ[R] (V → R) →ₗ[R] R) :
              (a : V → R) → (V → R) →ₗ[R] R)
            x :
          (V → R) →ₗ[R] R) :
        (a : V → R) → R)
      x =
    HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2
have simp_rw : (∑ 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) =
  HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : 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) =
    HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2
have rw : HAdd.hAdd (α := 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 =
  HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2
Tactic: rw [← add_self_div_two (∑ x_1 : V, ∑ x_2 : V, _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
| HAdd.hAdd (α := 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
have h : ∀ (i j : V), if G.Adj i j then x i * x i - x i * x j else 0
Tactic: enter [1, 2, 2, i, 2, j]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
i j : V
| if G.Adj i j then x i * x i - x i * x j else 0
have h : if G.Adj j i then x i * x i - x i * x j else 0
Tactic: rw [if_congr (adj_comm G i j) rfl rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
| HAdd.hAdd (α := 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
have h : ∀ (i j : V), if G.Adj j i then x i * x i - x i * x j else 0
Tactic: enter [1, 2, 2, i, 2, j]; rw [if_congr (adj_comm G i j) rfl rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
⊢ HAdd.hAdd (α := 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 =
    HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2
have conv_lhs : HAdd.hAdd (α := 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 =
  HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
| HAdd.hAdd (α := 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
have enter : ∑ i : V, ∑ j : V, if G.Adj j i then x i * x i - x i * x j else 0
Tactic: enter [1, 2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
| ∑ i : V, ∑ j : V, if G.Adj j i then x i * x i - x i * x j else 0
have rw : ∑ 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
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
| HAdd.hAdd (α := 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
have enter : ∑ 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
Tactic: enter [1, 2]; rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
⊢ HAdd.hAdd (α := 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 =
    HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2
have conv_lhs : HAdd.hAdd (α := 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 =
  HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2
Tactic: conv_lhs => enter [1, 2]; rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
⊢ HAdd.hAdd (α := 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 =
    HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2
have simp_rw : HDiv.hDiv (α := 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 HAdd.hAdd (α := R) 0 0)
    2 =
  HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2
Tactic: simp_rw [← sum_add_distrib, ite_add_ite]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
⊢ HDiv.hDiv (α := 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 HAdd.hAdd (α := R) 0 0)
      2 =
    HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2
have e_a : ∀ (i : V),
  Eq.{u_2 + 1} (α := R)
    (∑ 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 HAdd.hAdd (α := R) 0 0)
    (∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0)
Tactic: congr 2 with i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : CharZero R
x : V → R
i : V
⊢ Eq.{u_2 + 1} (α := R)
    (∑ 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 HAdd.hAdd (α := R) 0 0)
    (∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0)
have e_a : ∀ (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 HAdd.hAdd (α := R) 0 0) =
    if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0
Tactic: congr 2 with j
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : StarRing R
inst_7 : TrivialStar R
⊢ (lapMatrix R G).PosSemidef
have refine_1 : (lapMatrix R G).IsHermitian
Tactic: refine .of_dotProduct_mulVec_nonneg ?_ (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : StarRing R
inst_7 : TrivialStar R
refine_1 : (lapMatrix R G).IsHermitian
⊢ (lapMatrix R G).PosSemidef
have refine_2 : ∀ (x : V → R), 0 ≤ star x ⬝ᵥ lapMatrix R G *ᵥ x
Tactic: refine .of_dotProduct_mulVec_nonneg ?_ (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : StarRing R
inst_7 : TrivialStar R
⊢ (lapMatrix R G).IsHermitian
have refine_1 : (lapMatrix R G)ᴴ = lapMatrix R G
Tactic: rw [IsHermitian, conjTranspose_eq_transpose_of_trivial, isSymm_lapMatrix]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : StarRing R
inst_7 : TrivialStar R
refine_1 : (lapMatrix R G)ᴴ = lapMatrix R G
⊢ (lapMatrix R G).IsHermitian
have refine_1₁ : (lapMatrix R G)ᵀ = lapMatrix R G
Tactic: rw [IsHermitian, conjTranspose_eq_transpose_of_trivial, isSymm_lapMatrix]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : StarRing R
inst_7 : TrivialStar R
refine_1 : (lapMatrix R G)ᴴ = lapMatrix R G
refine_1₁ : (lapMatrix R G)ᵀ = lapMatrix R G
⊢ (lapMatrix R G).IsHermitian
have refine_1₂ : lapMatrix R G = lapMatrix R G
Tactic: rw [IsHermitian, conjTranspose_eq_transpose_of_trivial, isSymm_lapMatrix]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
R : Type u_2
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
inst_3 : Field R
inst_4 : LinearOrder R
inst_5 : IsStrictOrderedRing R
inst_6 : StarRing R
inst_7 : TrivialStar R
x : V → R
⊢ 0 ≤ star x ⬝ᵥ lapMatrix R G *ᵥ x
have refine_2 : 0 ≤ HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2
Tactic: rw [star_trivial, ← toLinearMap₂'_apply', lapMatrix_toLinearMap₂']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
⊢ lapMatrix ℝ G *ᵥ x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j
have rw : Eq (α := ℝ)
    (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                      (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                    (lapMatrix ℝ G) :
                  (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
              (star x) :
            (V → ℝ) →ₗ[ℝ] ℝ) :
          (a : V → ℝ) → ℝ)
        x :
      ℝ)
    (0 : ℝ) ↔
  ∀ (i j : V), G.Adj i j → x i = x j
Tactic: rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
      lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.LapMatrix (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
rw :
  Eq (α := ℝ)
      (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                        (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                      (lapMatrix ℝ G) :
                    (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                  (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
                (star x) :
              (V → ℝ) →ₗ[ℝ] ℝ) :
            (a : V → ℝ) → ℝ)
          x :
        ℝ)
      (0 : ℝ) ↔
    ∀ (i j : V), G.Adj i j → x i = x j
⊢ lapMatrix ℝ G *ᵥ x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j
have rw₁ : Eq (α := ℝ)
    (((((((toLinearMap₂' ℝ : Matrix V V ℝ ≃ₗ[ℝ] (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                      (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ)
                    (lapMatrix ℝ G) :
                  (V → ℝ) →ₗ[ℝ] (V → ℝ) →ₗ[ℝ] ℝ) :
                (a : V → ℝ) → (V → ℝ) →ₗ[ℝ] ℝ)
              x :
            (V → ℝ) →ₗ[ℝ] ℝ) :
          (a : V → ℝ) → ℝ)
        x :
      ℝ)
    (0 : ℝ) ↔
  ∀ (i j : V), G.Adj i j → x i = x j
Tactic: rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
      lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]