awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
a b : α
h : G.Adj a b
e_a :
  ∀ (e : α), Membership.mem (γ := Finset α) {x : α | True ∧ (x = a ∨ x = b)} e ↔ Membership.mem (γ := Finset α) {a, b} e
⊢ Eq (α := Finset α) {x : α | True ∧ (x = a ∨ x = b)} {a, b}

Tactic:
ext e
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e_1 : Sym2 α
inst_3 : Fintype α
a b : α
h : G.Adj a b
e : α
⊢ Membership.mem (γ := Finset α) {x : α | True ∧ (x = a ∨ x = b)} e ↔ Membership.mem (γ := Finset α) {a, b} e

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
h : e ∉ G.edgeSet
⊢ Eq.{u_1 + 1} (α := R) (∑ a : α, incMatrix R G a e) 0

Tactic:
sum_eq_zero fun _ _ => G.incMatrix_of_notMem_incidenceSet fun he => h he.1

Premises used: Finset.sum_eq_zero, And.left, SimpleGraph.incMatrix_of_notMem_incidenceSet
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
simp :
  Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) (if e ∈ G.edgeSet then 2 else 0)
⊢ ((incMatrix R G)ᵀ * incMatrix R G) e e = if e ∈ G.edgeSet then 2 else 0

Tactic:
simp only [Matrix.mul_apply, incMatrix_apply', transpose_apply, ite_zero_mul_ite_zero, one_mul,
    sum_boole, and_self_iff]

Premises used: ite_zero_mul_ite_zero, SimpleGraph.incMatrix_apply', Matrix.mul_apply, and_self_iff, Matrix.transpose_apply, Finset.sum_boole, one_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
pos : ∀ (h : e ∈ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 2
neg : ∀ (h : e ∉ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 0
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) (if e ∈ G.edgeSet then 2 else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
h : e ∈ G.edgeSet
pos : ∀ (h : e ∈ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 2
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 2

Tactic:
revert h
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
⊢ ∀ (h : e ∈ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 2

Tactic:
e.ind ?_

Premises used: Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
pos :
  ∀ (x y : α) (h : s(x, y) ∈ G.edgeSet),
    Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x_1 : α | s(x, y) ∈ G.incidenceSet x_1}) : R) 2
⊢ ∀ (h : e ∈ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 2

Tactic:
refine e.ind ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
pos :
  Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | s(v, w) ∈ G.incidenceSet x}) : R)
    (↑(card (α := α) {(v, w).1, (v, w).2}) : R)
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | s(v, w) ∈ G.incidenceSet x}) : R) 2

Tactic:
rw [← Nat.cast_two, ← card_pair (G.ne_of_adj h)]

Premises used: SimpleGraph.ne_of_adj, Finset.card_pair, Nat.cast_two
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
pos : Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | x = v ∨ x = w}) : R) (↑(card (α := α) {v, w}) : R)
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | s(v, w) ∈ G.incidenceSet x}) : R)
    (↑(card (α := α) {(v, w).1, (v, w).2}) : R)

Tactic:
simp only [mk'_mem_incidenceSet_iff, G.mem_edgeSet.mp h, true_and]

Premises used: Iff.mp, SimpleGraph.mk'_mem_incidenceSet_iff, SimpleGraph.mem_edgeSet, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
pos : Eq (α := Finset α) {x : α | x = v ∨ x = w} {v, w}
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | x = v ∨ x = w}) : R) (↑(card (α := α) {v, w}) : R)

Tactic:
congr 2
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
pos : ∀ (u : α), Membership.mem (γ := Finset α) {x : α | x = v ∨ x = w} u ↔ Membership.mem (γ := Finset α) {v, w} u
⊢ Eq (α := Finset α) {x : α | x = v ∨ x = w} {v, w}

Tactic:
ext u
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∈ G.edgeSet
u : α
⊢ Membership.mem (γ := Finset α) {x : α | x = v ∨ x = w} u ↔ Membership.mem (γ := Finset α) {v, w} u

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
h : e ∉ G.edgeSet
neg : ∀ (h : e ∉ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 0
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 0

Tactic:
revert h
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
⊢ ∀ (h : e ∉ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 0

Tactic:
e.ind ?_

Premises used: Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
neg :
  ∀ (x y : α) (h : s(x, y) ∉ G.edgeSet),
    Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x_1 : α | s(x, y) ∈ G.incidenceSet x_1}) : R) 0
⊢ ∀ (h : e ∉ G.edgeSet), Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | e ∈ G.incidenceSet x}) : R) 0

Tactic:
refine e.ind ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
Goal:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst : NonAssocSemiring R
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
e : Sym2 α
inst_3 : Fintype α
inst_4 : Decidable (e ∈ G.edgeSet)
v w : α
h : s(v, w) ∉ G.edgeSet
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := α) {x : α | s(v, w) ∈ G.incidenceSet x}) : R) 0

Tactic:
simp [mk'_mem_incidenceSet_iff, G.mem_edgeSet.not.mp h]

Premises used: Iff.not, Iff.mp, SimpleGraph.mk'_mem_incidenceSet_iff, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
a b : α
h : G.Adj a b
simp_rw :
  Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := Sym2 α) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b}) : R) 1
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

Tactic:
simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply,
    Set.indicator_apply, Pi.one_apply, sum_boole]

Premises used: Set.indicator_apply, SimpleGraph.incMatrix_apply_mul_incMatrix_apply, Pi.one_apply, Matrix.mul_apply, Matrix.transpose_apply, Finset.sum_boole
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
a b : α
h : G.Adj a b
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1

Tactic:
@Nat.cast_one R _

Premises used: Nat.cast_one
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
a b : α
h : G.Adj a b
h₁ : card.{u_2} (α := Sym2 α) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} = 1
⊢ Eq.{u_1 + 1} (α := R) (↑(card.{u_2} (α := Sym2 α) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b}) : R) 1

Tactic:
convert! @Nat.cast_one R _

Premises used: Nat.cast_one
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
a b : α
h : G.Adj a b
⊢ card (α := Sym2 α) {s(a, b)} = 1

Tactic:
card_singleton s(a, b)

Premises used: Sym2.mk, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
a b : α
h : G.Adj a b
h₁ : Eq (α := Finset (Sym2 α)) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} {s(a, b)}
⊢ card.{u_2} (α := Sym2 α) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} = 1

Tactic:
convert! card_singleton s(a, b)

Premises used: Sym2.mk, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
a b : α
h : G.Adj a b
h₁ : Eq (α := Set (Sym2 α)) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} {s(a, b)}
⊢ Eq (α := Finset (Sym2 α)) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} {s(a, b)}

Tactic:
rw [← coe_eq_singleton, coe_filter_univ]

Premises used: Finset.coe_eq_singleton, Finset.coe_filter_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
a b : α
h : G.Adj a b
⊢ Eq (α := Set (Sym2 α)) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} {s(a, b)}

Tactic:
G.incidenceSet_inter_incidenceSet_of_adj h

Premises used: SimpleGraph.incidenceSet_inter_incidenceSet_of_adj, Set.Mem, setOf, Set.inter
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
a b : α
h : G.Adj a b
⊢ Eq (α := Set (Sym2 α)) {x : Sym2 α | x ∈ G.incidenceSet a ∩ G.incidenceSet b} {s(a, b)}

Tactic:
exact G.incidenceSet_inter_incidenceSet_of_adj h

Premises used: SimpleGraph.incidenceSet_inter_incidenceSet_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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 :
  ∀ (a b : α),
    (incMatrix R G * (incMatrix R G)ᵀ) a b =
      (of : (a : α → α → R) → Matrix α α R)
        (fun (a b : α) ↦ if a = b then (↑(G.degree a) : R) else if G.Adj a b then 1 else 0) a b
⊢ incMatrix R G * (incMatrix R G)ᵀ =
    (of : (a : α → α → R) → Matrix α α R) fun (a b : α) ↦
      if a = b then (↑(G.degree a) : R) else if G.Adj a b then 1 else 0

Tactic:
ext a b
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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 : α
a₁ : (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
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b =
    (of : (a : α → α → R) → Matrix α α R)
      (fun (a b : α) ↦ if a = b then (↑(G.degree a) : R) else if G.Adj a b then 1 else 0) a b

Tactic:
dsimp
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
neg : ∀ (h : ¬a = b) (h' : ¬G.Adj a b), (incMatrix R G * (incMatrix R G)ᵀ) a b = 0
⊢ (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

Tactic:
split_ifs with h h'
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
pos : (incMatrix R G * (incMatrix R G)ᵀ) a a = (↑(G.degree a) : R)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = (↑(G.degree a) : R)

Tactic:
subst b
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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 : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = (↑(G.degree a) : R)

Tactic:
incMatrix_mul_transpose_diag (R := R) G

Premises used: SimpleGraph.incMatrix_mul_transpose_diag
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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 : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = (↑(G.degree a) : R)

Tactic:
exact incMatrix_mul_transpose_diag (R := R) G

Premises used: SimpleGraph.incMatrix_mul_transpose_diag
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
h' : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

Tactic:
G.incMatrix_mul_transpose_apply_of_adj h'

Premises used: SimpleGraph.incMatrix_mul_transpose_apply_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
h' : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

Tactic:
exact G.incMatrix_mul_transpose_apply_of_adj h'

Premises used: SimpleGraph.incMatrix_mul_transpose_apply_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix
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
h' : ¬G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 0

Tactic:
simp only [Matrix.mul_apply, Matrix.transpose_apply,
      G.incMatrix_apply_mul_incMatrix_apply_of_not_adj h h', sum_const_zero]

Premises used: SimpleGraph.incMatrix_apply_mul_incMatrix_apply_of_not_adj, Matrix.mul_apply, Finset.sum_const_zero, Matrix.transpose_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
α : Type u_1
V : Type u_2
inst : NonAssocSemiring α
inst_1 : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
a : ∀ (i j : V), Aᴴ i j = A i j
⊢ A.IsHermitian

Tactic:
ext i j
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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₁ : ∀ (heq : A i j = 1), Aᴴ i j = A i j
⊢ Aᴴ i j = A i j

Tactic:
rcases h.zero_or_one i j with heq | heq

Premises used: Matrix.IsAdjMatrix.zero_or_one
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
α : Type u_1
V : Type u_2
inst : NonAssocSemiring α
inst_1 : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
i j : V
heq : A i j = 0
⊢ Aᴴ i j = A i j

Tactic:
simp [heq, h.symm.apply]

Premises used: Matrix.IsAdjMatrix.symm, Matrix.IsSymm.apply
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
α : Type u_1
V : Type u_2
inst : NonAssocSemiring α
inst_1 : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
i j : V
heq : A i j = 1
⊢ Aᴴ i j = A i j

Tactic:
simp [heq, h.symm.apply]

Premises used: Matrix.IsAdjMatrix.symm, Matrix.IsSymm.apply
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
Goal:
V : Type u_1
R : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : NonAssocSemiring R
inst_2 : StarRing R
⊢ (adjMatrix R G).IsHermitian

Tactic:
G.isAdjMatrix_adjMatrix R |>.isHermitian

Premises used: SimpleGraph.isAdjMatrix_adjMatrix, Matrix.IsAdjMatrix.isHermitian
-- Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix
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)
rw₁ rw₂ : Eq.{u_3 + 1} (α := R) (↑(#(filter (G.Adj i) univ)) : 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)

Tactic:
rw [sum_boole, Set.toFinset_setOf]

Premises used: Finset.sum_boole, Set.toFinset_setOf
-- 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 : AddMonoidWithOne R
⊢ (degMatrix R G).IsSymm

Tactic:
isSymm_diagonal _

Premises used: SimpleGraph.degMatrix, Matrix.isSymm_diagonal
-- 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 : NonAssocSemiring R
inst_4 : StarRing R
⊢ ∀ (i : V), IsSelfAdjoint.{u_2} (R := R) (↑(G.degree i) : R)

Tactic:
simp
-- 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 : AddGroupWithOne R
⊢ (lapMatrix R G).IsSymm

Tactic:
G.isSymm_degMatrix R |>.sub G.isSymm_adjMatrix

Premises used: SimpleGraph.isSymm_adjMatrix, SimpleGraph.isSymm_degMatrix, SimpleGraph.lapMatrix, Matrix.IsSymm.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 : NonAssocRing R
inst_4 : StarRing R
⊢ (lapMatrix R G).IsHermitian

Tactic:
G.isHermitian_degMatrix R |>.sub <| G.isHermitian_adjMatrix R

Premises used: SimpleGraph.isHermitian_adjMatrix, SimpleGraph.isHermitian_degMatrix, SimpleGraph.lapMatrix, Matrix.IsHermitian.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 : NonAssocSemiring R
v : V
vec : V → R
rw : ((diagonal fun (x : V) ↦ (↑(G.degree x) : R)) *ᵥ vec) v = (↑(G.degree v) : R) * vec v
rw₁ rw₂ : (↑(G.degree v) : R) * vec v = (↑(G.degree v) : R) * vec v
⊢ (degMatrix R G *ᵥ vec) v = (↑(G.degree v) : R) * vec v

Tactic:
rw [degMatrix, mulVec_diagonal]

Premises used: SimpleGraph.degMatrix, Matrix.mulVec_diagonal
-- 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 : 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
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
⊢ (lapMatrix 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]

Premises used: SimpleGraph.adjMatrix_mulVec_apply, Matrix.sub_mulVec, SimpleGraph.lapMatrix, SimpleGraph.degMatrix_mulVec_apply, Pi.sub_apply
-- 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 : NonAssocRing R
h : ∀ (i : V), (lapMatrix R G *ᵥ fun (x : V) ↦ 1) i = 0 i
⊢ (lapMatrix R G *ᵥ fun (x : V) ↦ 1) = 0

Tactic:
ext1 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 : NonAssocRing R
i : V
h : HMul.hMul (α := R) (↑(G.degree i) : R) 1 - ∑ u ∈ G.neighborFinset i, 1 = 0 i
⊢ (lapMatrix R G *ᵥ fun (x : V) ↦ 1) i = 0 i

Tactic:
rw [lapMatrix_mulVec_apply]

Premises used: SimpleGraph.lapMatrix_mulVec_apply
-- 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 : NonAssocRing R
i : V
⊢ HMul.hMul (α := R) (↑(G.degree i) : R) 1 - ∑ u ∈ G.neighborFinset i, 1 = 0 i

Tactic:
simp
-- 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 : CommSemiring R
x : V → R
⊢ x ⬝ᵥ degMatrix R G *ᵥ x = ∑ i : V, (↑(G.degree i) : R) * x i * x i

Tactic:
simp only [dotProduct, degMatrix, mulVec_diagonal, ← mul_assoc, mul_comm]

Premises used: dotProduct, mul_assoc, SimpleGraph.degMatrix, mul_comm, Matrix.mulVec_diagonal