awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
⊢ A i j = 0 ∨ A i j = 1

Tactic:
have := hA.zero_or_one i j
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
this : A i j = 0 ∨ A i j = 1
⊢ (A ⊙ A) i j = A i j

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq V
inst_1 : MonoidWithZero α
inst_2 : IsLeftCancelMulZero α
A : Matrix V V α
simp : A.IsAdjMatrix ↔ (∀ (i j : V), A i j = 0 ∨ A i j = 1) ∧ A.IsSymm ∧ ∀ (x : V), A x x = 0
⊢ A.IsAdjMatrix ↔ A ⊙ A = A ∧ A.IsSymm ∧ 1 ⊙ A = 0

Tactic:
simp only [hadamard_self_eq_self_iff, IsIdempotentElem.iff_eq_zero_or_one,
    one_hadamard_eq_zero_iff, funext_iff, diag, Pi.zero_apply]

Premises used: Matrix.hadamard_self_eq_self_iff, Matrix.diag, funext_iff, Pi.zero_apply, IsIdempotentElem.iff_eq_zero_or_one, Matrix.one_hadamard_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq V
inst_1 : MonoidWithZero α
inst_2 : IsLeftCancelMulZero α
A : Matrix V V α
⊢ A.IsAdjMatrix ↔ (∀ (i j : V), A i j = 0 ∨ A i j = 1) ∧ A.IsSymm ∧ ∀ (x : V), A x x = 0

Tactic:
grind [IsAdjMatrix]

Premises used: Matrix.IsAdjMatrix
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : Zero α
inst_3 : One α
i : V
⊢ A.compl i i = 0

Tactic:
simp [compl]

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : Zero α
inst_3 : One α
i j : V
simp :
  (¬i = j → A i j = 0 → Eq.{u_1 + 1} (α := α) 1 0) ∨
    Eq.{u_1 + 1} (α := α) (if i = j then 0 else if A i j = 0 then 1 else 0) 1
⊢ A.compl i j = 0 ∨ A.compl i j = 1

Tactic:
simp [compl]

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : Zero α
inst_3 : One α
i j : V
⊢ (¬i = j → A i j = 0 → Eq.{u_1 + 1} (α := α) 1 0) ∨
    Eq.{u_1 + 1} (α := α) (if i = j then 0 else if A i j = 0 then 1 else 0) 1

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : Zero α
inst_3 : One α
h : A.IsSymm
a : ∀ (i j : V), A.complᵀ i j = A.compl i j
⊢ A.compl.IsSymm

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : Zero α
inst_3 : One α
h : A.IsSymm
i j : V
⊢ A.complᵀ i j = A.compl i j

Tactic:
simp [compl, h.apply, eq_comm]

Premises used: eq_comm, Matrix.IsSymm.apply, Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : Zero α
inst_3 : One α
h : A.IsSymm
⊢ A.compl.IsSymm

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
inst_2 : Zero α
inst_3 : One α
A B : Matrix V V α
hA : A.IsAdjMatrix
hB : B.IsAdjMatrix
h : A.compl = B.compl
i j : V
⊢ Eq (α := V → V → α) (fun (i j : V) ↦ if i = j then 0 else if A i j = 0 then 1 else 0) fun (i j : V) ↦
    if i = j then 0 else if B i j = 0 then 1 else 0

Tactic:
simp [compl] at h

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
inst_2 : Zero α
inst_3 : One α
A B : Matrix V V α
hA : A.IsAdjMatrix
hB : B.IsAdjMatrix
i j : V
h :
  Eq (α := V → V → α) (fun (i j : V) ↦ if i = j then 0 else if A i j = 0 then 1 else 0) fun (i j : V) ↦
    if i = j then 0 else if B i j = 0 then 1 else 0
⊢ A i j = B i j

Tactic:
grind [congr($h i j), IsAdjMatrix]

Premises used: Matrix.IsAdjMatrix
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
inst_2 : Zero α
inst_3 : One α
A : Matrix V V α
hA : A.IsAdjMatrix
a : ∀ (i j : V), A.compl.compl i j = A i j
⊢ A.compl.compl = A

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
inst_2 : Zero α
inst_3 : One α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
a : (if i = j then 0 else if ¬i = j → A i j = 0 → Eq.{u_1 + 1} (α := α) 1 0 then 1 else 0) = A i j
⊢ A.compl.compl i j = A i j

Tactic:
simp [compl]

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
inst_2 : Zero α
inst_3 : One α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
⊢ (if i = j then 0 else if ¬i = j → A i j = 0 → Eq.{u_1 + 1} (α := α) 1 0 then 1 else 0) = A i j

Tactic:
grind [compl, IsAdjMatrix]

Premises used: Matrix.IsAdjMatrix, Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : Zero α
inst_3 : One α
h : A.IsAdjMatrix
⊢ A.compl.IsAdjMatrix

Tactic:
isAdjMatrix_compl A h.symm

Premises used: Matrix.IsAdjMatrix.symm, Matrix.isAdjMatrix_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h : A.IsAdjMatrix
Adj : ∀ (v w : V), (toGraph (A := A.compl) ⋯).Adj v w ↔ h.toGraphᶜ.Adj v w
⊢ toGraph (A := A.compl) ⋯ = h.toGraphᶜ

Tactic:
ext v w
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h : A.IsAdjMatrix
v w : V
Adj : ∀ (h_1 : A v w = 0), (toGraph (A := A.compl) ⋯).Adj v w ↔ h.toGraphᶜ.Adj v w
Adj₁ : ∀ (h_1 : A v w = 1), (toGraph (A := A.compl) ⋯).Adj v w ↔ h.toGraphᶜ.Adj v w
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h.toGraphᶜ.Adj v w

Tactic:
rcases h.zero_or_one v w with h | h

Premises used: Matrix.IsAdjMatrix.zero_or_one
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h_1 : A.IsAdjMatrix
v w : V
h : A v w = 0
pos : ∀ (hvw : v = w), (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w
neg : ∀ (hvw : ¬v = w), (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w

Tactic:
by_cases hvw : v = w
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h_1 : A.IsAdjMatrix
v w : V
h : A v w = 1
pos : ∀ (hvw : v = w), (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w
neg : ∀ (hvw : ¬v = w), (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w

Tactic:
by_cases hvw : v = w
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h_1 : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : v = w
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w

Tactic:
simp [Matrix.compl, h, hvw]

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h_1 : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : ¬v = w
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w

Tactic:
simp [Matrix.compl, h, hvw]

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h_1 : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : v = w
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w

Tactic:
simp [Matrix.compl, h, hvw]

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq V
A : Matrix V V α
inst_2 : MulZeroOneClass α
inst_3 : Nontrivial α
h_1 : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : ¬v = w
⊢ (toGraph (A := A.compl) ⋯).Adj v w ↔ h_1.toGraphᶜ.Adj v w

Tactic:
simp [Matrix.compl, h, hvw]

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
v w : V
inst_1 : Zero α
inst_2 : One α
⊢ adjMatrix α G v w = if G.Adj v w then 1 else 0

Tactic:
rfl

Premises used: SimpleGraph.adjMatrix, rfl, ite
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : Zero α
inst_1 : One α
a : ∀ (i j : V), adjMatrix α ⊥ i j = 0 i j
⊢ Eq (α := Matrix V V α) (adjMatrix α ⊥) 0

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : Zero α
inst_1 : One α
i j : V
⊢ adjMatrix α ⊥ i j = 0 i j

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq V
inst_1 : Ring α
a : ∀ (i j : V), adjMatrix α ⊤ i j = (of : (a : V → V → α) → Matrix V V α) (fun (i j : V) ↦ if i = j then 0 else 1) i j
⊢ Eq (α := Matrix V V α) (adjMatrix α ⊤) ((of : (a : V → V → α) → Matrix V V α) fun (i j : V) ↦ if i = j then 0 else 1)

Tactic:
ext i j
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : DecidableEq V
inst_1 : Ring α
i j : V
a : i = j → adjMatrix α ⊤ i j = (of : (a : V → V → α) → Matrix V V α) (fun (i j : V) ↦ if i = j then 0 else 1) i j
a₁ : i ≠ j → adjMatrix α ⊤ i j = (of : (a : V → V → α) → Matrix V V α) (fun (i j : V) ↦ if i = j then 0 else 1) i j
⊢ adjMatrix α ⊤ i j = (of : (a : V → V → α) → Matrix V V α) (fun (i j : V) ↦ if i = j then 0 else 1) i j

Tactic:
cases eq_or_ne i j

Premises used: eq_or_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Zero α
inst_2 : One α
a : ∀ (i j : V), (adjMatrix α G)ᵀ i j = adjMatrix α G i j
⊢ (adjMatrix α G)ᵀ = adjMatrix α G

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Zero α
inst_2 : One α
i j : V
⊢ (adjMatrix α G)ᵀ i j = adjMatrix α G i j

Tactic:
simp [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Zero α
inst_2 : One α
⊢ (adjMatrix α G).IsSymm

Tactic:
transpose_adjMatrix G

Premises used: Matrix.IsSymm, SimpleGraph.transpose_adjMatrix
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Zero α
inst_2 : One α
h : ∀ (x : V), (adjMatrix α G).diag x = 0 x
⊢ (adjMatrix α G).diag = 0

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Zero α
inst_2 : One α
x : V
⊢ (adjMatrix α G).diag x = 0 x

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Zero α
inst_2 : One α
⊢ ∀ (i j : V), adjMatrix α G i j = 0 ∨ adjMatrix α G i j = 1

Tactic:
grind [adjMatrix_apply]

Premises used: SimpleGraph.adjMatrix_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
Adj : ∀ (x x_1 : V), (IsAdjMatrix.toGraph (A := adjMatrix α G) ⋯).Adj x x_1 ↔ G.Adj x x_1
⊢ IsAdjMatrix.toGraph (A := adjMatrix α G) ⋯ = G

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
x x_1 : V
Adj : ¬G.Adj x x_1 → False ↔ G.Adj x x_1
⊢ (IsAdjMatrix.toGraph (A := adjMatrix α G) ⋯).Adj x x_1 ↔ G.Adj x x_1

Tactic:
simp only [IsAdjMatrix.toGraph_adj, adjMatrix_apply, ite_eq_left_iff, zero_ne_one]

Premises used: Matrix.IsAdjMatrix.toGraph_adj, SimpleGraph.adjMatrix_apply, ite_eq_left_iff, zero_ne_one
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
x x_1 : V
⊢ ¬G.Adj x x_1 → False ↔ G.Adj x x_1

Tactic:
apply Classical.not_not

Premises used: Classical.not_not
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : DecidableEq α
inst_3 : Zero α
inst_4 : One α
⊢ (adjMatrix α G).compl = adjMatrix α Gᶜ

Tactic:
aesop (add simp [Matrix.compl])

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : AddZeroClass α
inst_3 : One α
H : SimpleGraph V
inst_4 : DecidableRel H.Adj
h : IsCompl G H
⊢ Gᶜ = H

Tactic:
have := h.compl_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : AddZeroClass α
inst_3 : One α
H : SimpleGraph V
inst_4 : DecidableRel H.Adj
h : IsCompl G H
this : Gᶜ = H
subst :
  ∀ [inst_5 : DecidableRel Gᶜ.Adj] (h : IsCompl G Gᶜ), adjMatrix α G + adjMatrix α Gᶜ = adjMatrix α G + adjMatrix α Gᶜ
⊢ adjMatrix α G + adjMatrix α H = adjMatrix α G + adjMatrix α Gᶜ

Tactic:
subst this
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : AddZeroClass α
inst_3 : One α
inst_4 : DecidableRel Gᶜ.Adj
h : IsCompl G Gᶜ
⊢ adjMatrix α G + adjMatrix α Gᶜ = adjMatrix α G + adjMatrix α Gᶜ

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : AddZeroClass α
inst_3 : One α
H : SimpleGraph V
inst_4 : DecidableRel H.Adj
h : IsCompl G H
⊢ adjMatrix α G + adjMatrix α Gᶜ = adjMatrix α (completeGraph V)

Tactic:
aesop (add simp Matrix.compl)

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : DecidableEq α
inst_3 : AddZeroClass α
inst_4 : One α
⊢ adjMatrix α G + (adjMatrix α G).compl = adjMatrix α (completeGraph V)

Tactic:
G.compl_adjMatrix_eq_adjMatrix_compl α ▸
    isCompl_compl.adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph α

Premises used: Eq.rec, SimpleGraph.IsCompl.adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph, isCompl_compl, Eq.symm, SimpleGraph.compl_adjMatrix_eq_adjMatrix_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : DecidableEq V
inst_2 : DecidableEq α
inst_3 : AddMonoid α
inst_4 : One α
⊢ 1 + adjMatrix α G + (adjMatrix α G).compl = (of : (a : V → V → α) → Matrix V V α) 1

Tactic:
aesop (add simp [add_assoc])

Premises used: add_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : Zero α
inst_1 : One α
inst_2 : DecidableEq α
inst_3 : DecidableEq V
⊢ (adjMatrix α (completeGraph V)).compl = 0

Tactic:
aesop (add simp Matrix.compl)

Premises used: Matrix.compl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : Zero α
inst_1 : One α
inst_2 : DecidableEq α
inst_3 : DecidableEq V
⊢ Matrix.compl 0 = adjMatrix α (completeGraph V)

Tactic:
simp [← IsAdjMatrix.compl_inj]

Premises used: Matrix.IsAdjMatrix.compl_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : AddGroup α
inst_1 : One α
inst_2 : DecidableEq V
a :
  ∀ (i j : V),
    adjMatrix α (completeGraph V) i j =
      HSub.hSub (α := Matrix V V α) (β := Matrix V V α) ((of : (a : V → V → α) → Matrix V V α) 1) 1 i j
⊢ adjMatrix α (completeGraph V) = HSub.hSub (α := Matrix V V α) ((of : (a : V → V → α) → Matrix V V α) 1) 1

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : AddGroup α
inst_1 : One α
inst_2 : DecidableEq V
i j : V
⊢ adjMatrix α (completeGraph V) i j =
    HSub.hSub (α := Matrix V V α) (β := Matrix V V α) ((of : (a : V → V → α) → Matrix V V α) 1) 1 i j

Tactic:
simp [one_apply, sub_ite]

Premises used: Matrix.one_apply, sub_ite
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : AddGroup α
inst_1 : One α
inst_2 : DecidableEq V
inst_3 : DecidableEq α
⊢ Matrix.compl 0 = HSub.hSub (α := Matrix V V α) ((of : (a : V → V → α) → Matrix V V α) 1) 1

Tactic:
simp [adjMatrix_completeGraph_eq_of_one_sub_one]

Premises used: SimpleGraph.adjMatrix_completeGraph_eq_of_one_sub_one
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
inst : AddGroup α
inst_1 : One α
inst_2 : DecidableEq V
inst_3 : DecidableEq α
⊢ (HSub.hSub (α := Matrix V V α) ((of : (a : V → V → α) → Matrix V V α) 1) 1).compl = 0

Tactic:
simp [← adjMatrix_completeGraph_eq_of_one_sub_one]

Premises used: SimpleGraph.adjMatrix_completeGraph_eq_of_one_sub_one
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : MulZeroOneClass α
⊢ adjMatrix α G ⊙ adjMatrix α G = adjMatrix α G

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
⊢ adjMatrix α G v ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
simp [neighborFinset_eq_filter, dotProduct, sum_filter]

Premises used: dotProduct, SimpleGraph.neighborFinset_eq_filter, Finset.sum_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
⊢ vec ⬝ᵥ adjMatrix α G v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
simp [neighborFinset_eq_filter, dotProduct, sum_filter]

Premises used: dotProduct, SimpleGraph.neighborFinset_eq_filter, Finset.sum_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
rw : (fun (j : V) ↦ adjMatrix α G v j) ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (∑ u ∈ G.neighborFinset v, vec u) (∑ u ∈ G.neighborFinset v, vec u)
⊢ (adjMatrix α G *ᵥ vec) v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
rw [mulVec, adjMatrix_dotProduct]

Premises used: SimpleGraph.adjMatrix_dotProduct, Matrix.mulVec
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
simp : (vec ⬝ᵥ fun (i : V) ↦ adjMatrix α G i v) = vec ⬝ᵥ adjMatrix α G v
⊢ (vec ᵥ* adjMatrix α G) v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
simp only [← dotProduct_adjMatrix, vecMul]

Premises used: Matrix.vecMul, SimpleGraph.dotProduct_adjMatrix
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ⬝ᵥ fun (i : V) ↦ adjMatrix α G i v) = vec ⬝ᵥ adjMatrix α G v

Tactic:
congr rfl ?_

Premises used: congr, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
refine : (fun (i : V) ↦ adjMatrix α G i v) = adjMatrix α G v
⊢ (vec ⬝ᵥ fun (i : V) ↦ adjMatrix α G i v) = vec ⬝ᵥ adjMatrix α G v

Tactic:
refine congr rfl ?_

Premises used: congr, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
h : ∀ (x : V), adjMatrix α G x v = adjMatrix α G v x
⊢ (fun (i : V) ↦ adjMatrix α G i v) = adjMatrix α G v

Tactic:
ext x
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
v : V
vec : V → α
x : V
h : adjMatrix α G x v = (adjMatrix α G)ᵀ x v
h₁ h₂ : adjMatrix α G x v = adjMatrix α G x v
⊢ adjMatrix α G x v = adjMatrix α G v x

Tactic:
rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]

Premises used: SimpleGraph.adjMatrix, Matrix.transpose_apply, SimpleGraph.transpose_adjMatrix
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
M : Matrix V V α
v w : V
⊢ (adjMatrix α G * M) v w = ∑ u ∈ G.neighborFinset v, M u w

Tactic:
simp [mul_apply, neighborFinset_eq_filter, sum_filter]

Premises used: Matrix.mul_apply, SimpleGraph.neighborFinset_eq_filter, Finset.sum_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
M : Matrix V V α
v w : V
⊢ (M * adjMatrix α G) v w = ∑ u ∈ G.neighborFinset w, M v u

Tactic:
simp [mul_apply, neighborFinset_eq_filter, sum_filter, adj_comm]

Premises used: Matrix.mul_apply, SimpleGraph.neighborFinset_eq_filter, Finset.sum_filter, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : AddCommMonoid α
inst_3 : One α
⊢ (adjMatrix α G).trace = 0

Tactic:
simp [Matrix.trace]

Premises used: Matrix.trace
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
i : V
⊢ (adjMatrix α G * adjMatrix α G) i i = (↑(G.degree i) : α)

Tactic:
simp [filter_true_of_mem]

Premises used: Finset.filter_true_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
⊢ (↑(Fintype.card.{u_2} G.Dart) : α) = adjMatrix α G *ᵥ 1 ⬝ᵥ 1

Tactic:
simp [G.dart_card_eq_sum_degrees, dotProduct_one]

Premises used: SimpleGraph.dart_card_eq_sum_degrees, dotProduct_one
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
a : α
v : V
⊢ (adjMatrix α G *ᵥ Function.const V a) v = (↑(G.degree v) : α) * a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Goal:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst : DecidableRel G.Adj
inst_1 : Fintype V
inst_2 : NonAssocSemiring α
d : ℕ
a : α
hd : G.IsRegularOfDegree d
v : V
⊢ (adjMatrix α G *ᵥ Function.const V a) v = (↑d : α) * a

Tactic:
simp [hd v]