awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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
⊢ ((((((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

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]

Premises used: SimpleGraph.dotProduct_mulVec_adjMatrix, sub_zero, Matrix.toLinearMap₂'_apply', MulZeroClass.zero_mul, SimpleGraph.dotProduct_mulVec_degMatrix, ite_sub_ite, Finset.sum_sub_distrib, ite_mul, SimpleGraph.degree_eq_sum_if_adj, Matrix.sub_mulVec, SimpleGraph.lapMatrix, one_mul, Finset.sum_mul, dotProduct_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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
⊢ (∑ 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:
rw [← add_self_div_two (∑ x_1 : V, ∑ x_2 : V, _)]

Premises used: Finset.univ, Finset.sum, add_self_div_two
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
h : ∀ (i j : V), if G.Adj i j then x i * x i - x i * x j else 0
| 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

Tactic:
enter [1, 2, 2, i, 2, j]
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
h : if G.Adj j i then x i * x i - x i * x j else 0
| if G.Adj i j then x i * x i - x i * x j else 0

Tactic:
rw [if_congr (adj_comm G i j) rfl rfl]

Premises used: if_congr, rfl, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
h : ∀ (i j : V), if G.Adj j i then x i * x i - x i * x j else 0
| 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

Tactic:
enter [1, 2, 2, i, 2, j]; rw [if_congr (adj_comm G i j) rfl rfl]
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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
⊢ 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:
conv_lhs => enter [1, 2, 2, i, 2, j]; rw [if_congr (adj_comm G i j) rfl rfl]
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
enter : ∑ i : V, ∑ j : V, if G.Adj j i then x i * x i - x i * x j else 0
| 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

Tactic:
enter [1, 2]
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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
| ∑ i : V, ∑ j : V, if G.Adj j i then x i * x i - x i * x j else 0

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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
| 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

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

Premises used: Finset.sum_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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
⊢ 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]; rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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
⊢ 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:
simp_rw [← sum_add_distrib, ite_add_ite]

Premises used: Finset.sum_add_distrib, ite_add_ite
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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)
⊢ 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:
congr 2 with i
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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
⊢ 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 j
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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 + (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:
ring_nf
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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

Tactic:
.of_dotProduct_mulVec_nonneg ?_ (fun x ↦ ?_)

Premises used: Matrix.PosSemidef.of_dotProduct_mulVec_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
refine_2 : ∀ (x : V → R), 0 ≤ star x ⬝ᵥ lapMatrix R G *ᵥ x
⊢ (lapMatrix R G).PosSemidef

Tactic:
refine .of_dotProduct_mulVec_nonneg ?_ (fun x ↦ ?_)
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
refine_1₂ refine_1₃ : lapMatrix R G = lapMatrix R G
⊢ (lapMatrix R G).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_eq_transpose_of_trivial, isSymm_lapMatrix]

Premises used: Matrix.conjTranspose_eq_transpose_of_trivial, SimpleGraph.isSymm_lapMatrix, Matrix.IsHermitian
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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
⊢ 0 ≤ star x ⬝ᵥ lapMatrix R G *ᵥ x

Tactic:
rw [star_trivial, ← toLinearMap₂'_apply', lapMatrix_toLinearMap₂']

Premises used: SimpleGraph.lapMatrix_toLinearMap₂', Matrix.toLinearMap₂'_apply', TrivialStar.star_trivial
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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 ≤ HDiv.hDiv (α := R) (∑ i : V, ∑ j : V, if G.Adj i j then HPow.hPow (β := ℕ) (x i - x j) 2 else 0) 2

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
x : V → R
⊢ Eq.{u_2 + 1} (α := 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 :
        R)
      (0 : R) ↔
    ∀ (i j : V), G.Adj i j → x i = x j

Tactic:
simp (disch := intros; positivity)
    [lapMatrix_toLinearMap₂', sum_eq_zero_iff_of_nonneg, sub_eq_zero]

Premises used: SimpleGraph.lapMatrix_toLinearMap₂', sub_eq_zero, Finset.sum_eq_zero_iff_of_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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
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
rw₂ rw₃ : (∀ (i j : V), G.Adj i j → x i = x j) ↔ ∀ (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

Tactic:
rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
      lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]

Premises used: Real, SimpleGraph.posSemidef_lapMatrix, TrivialStar.star_trivial, Matrix.PosSemidef.toLinearMap₂'_zero_iff, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
rw : (∀ (i j : V), G.Adj i j → x i = x j) ↔ ∀ (i j : V), G.Reachable i j → x i = x j
⊢ 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.Reachable i j → x i = x j

Tactic:
rw [lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]

Premises used: SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
⊢ (∀ (i j : V), G.Adj i j → x i = x j) ↔ ∀ (i j : V), G.Reachable i j → x i = x j

Tactic:
⟨?_, fun h i j hA ↦ h i j hA.reachable⟩

Premises used: SimpleGraph.Adj.reachable, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
refine : (∀ (i j : V), G.Adj i j → x i = x j) → ∀ (i j : V), G.Reachable i j → x i = x j
⊢ (∀ (i j : V), G.Adj i j → x i = x j) ↔ ∀ (i j : V), G.Reachable i j → x i = x j

Tactic:
refine ⟨?_, fun h i j hA ↦ h i j hA.reachable⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j : V
this : ∀ (w : G.Walk i j), x i = x j
⊢ G.Reachable i j → x i = x j

Tactic:
⟨w⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j u : V
⊢ x u = x u

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j u v w : V
hA : G.Adj u v
p : G.Walk v w
h' : x v = x w
⊢ x u = x w

Tactic:
(h _ _ hA).trans h'

Premises used: Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j u v w : V
hA : G.Adj u v
p : G.Walk v w
h' : x v = x w
⊢ x u = x w

Tactic:
exact (h _ _ hA).trans h'

Premises used: Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j : V
w : G.Walk i j
nil : ∀ {u : V}, x u = x u
cons : ∀ {u v w : V} (hA : G.Adj u v) (p : G.Walk v w) (h' : x v = x w), x u = x w
⊢ x i = x j

Tactic:
induction w with
  | nil => rfl
  | cons hA _ h' => exact (h _ _ hA).trans h'

Premises used: Finset.cons
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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.Reachable i j → x i = x j
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.Reachable i j → x i = x j
rw₂ rw₃ : (∀ (i j : V), G.Reachable i j → x i = x j) ↔ ∀ (i j : V), G.Reachable i j → x i = x j
⊢ lapMatrix ℝ G *ᵥ x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j

Tactic:
rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
      lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable]

Premises used: Real, SimpleGraph.posSemidef_lapMatrix, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, TrivialStar.star_trivial, Matrix.PosSemidef.toLinearMap₂'_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
rw : ∃ (v : V → ℝ), v ≠ 0 ∧ lapMatrix ℝ G *ᵥ v = 0
⊢ (lapMatrix ℝ G).det = 0

Tactic:
rw [← Matrix.exists_mulVec_eq_zero_iff]

Premises used: Matrix.exists_mulVec_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
h₁ : Ne.{u_1 + 1} (α := V → ℝ) (fun (x : V) ↦ 1) 0 ∧ (lapMatrix ℝ G *ᵥ fun (x : V) ↦ 1) = 0
⊢ ∃ (v : V → ℝ), v ≠ 0 ∧ lapMatrix ℝ G *ᵥ v = 0

Tactic:
use fun _ ↦ 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
⊢ Ne.{u_1 + 1} (α := V → ℝ) (fun (x : V) ↦ 1) 0 ∧ (lapMatrix ℝ G *ᵥ fun (x : V) ↦ 1) = 0

Tactic:
⟨?_, (lapMatrix_mulVec_eq_zero_iff_forall_adj G).mpr fun _ _ _ ↦ rfl⟩

Premises used: Iff.mpr, And.intro, rfl, SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
h₁ : Ne.{u_1 + 1} (α := V → ℝ) (fun (x : V) ↦ 1) 0
⊢ Ne.{u_1 + 1} (α := V → ℝ) (fun (x : V) ↦ 1) 0 ∧ (lapMatrix ℝ G *ᵥ fun (x : V) ↦ 1) = 0

Tactic:
refine ⟨?_, (lapMatrix_mulVec_eq_zero_iff_forall_adj G).mpr fun _ _ _ ↦ rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
h₁ : Set.Nonempty.{u_1} (α := V) (Function.support (M := ℝ) fun (x : V) ↦ 1)
⊢ Ne.{u_1 + 1} (α := V → ℝ) (fun (x : V) ↦ 1) 0

Tactic:
rw [← Function.support_nonempty_iff]

Premises used: Function.support_nonempty_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
h₁ : Membership.mem (γ := Set V) (Function.support (M := ℝ) fun (x : V) ↦ 1) (Classical.choice h)
⊢ Set.Nonempty.{u_1} (α := V) (Function.support (M := ℝ) fun (x : V) ↦ 1)

Tactic:
use Classical.choice h

Premises used: Classical.choice
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : Nonempty V
⊢ Membership.mem (γ := Set V) (Function.support (M := ℝ) fun (x : V) ↦ 1) (Classical.choice h)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
inst_3 : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
rw :
  ∀ (i j : V),
    G.Reachable i j →
      Eq (α := ℝ) (if G.connectedComponentMk i = c then 1 else 0) (if G.connectedComponentMk j = c then 1 else 0)
⊢ Membership.mem (γ := Submodule ℝ (V → ℝ))
    (LinearMap.ker (R₂ := ℝ) (M₂ := V → ℝ) (τ₁₂ := RingHom.id ℝ)
      ((toLin' : (a : Matrix V V ℝ) → (V → ℝ) →ₗ[ℝ] V → ℝ) (lapMatrix ℝ G)))
    fun (i : V) ↦ if G.connectedComponentMk i = c then 1 else 0

Tactic:
rw [LinearMap.mem_ker, toLin'_apply, lapMatrix_mulVec_eq_zero_iff_forall_reachable]

Premises used: LinearMap.mem_ker, SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_reachable, Matrix.toLin'_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
inst_3 : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
⊢ ∀ (i j : V),
    G.Reachable i j →
      Eq (α := ℝ) (if G.connectedComponentMk i = c then 1 else 0) (if G.connectedComponentMk j = c then 1 else 0)

Tactic:
grind [ConnectedComponent.eq]

Premises used: SimpleGraph.ConnectedComponent.eq