mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
⊢ v ∉ q.support

Tactic:
obtain ⟨p₀, p₁, hp₀, hp₁, happend⟩ := hp.mem_support_iff_exists_append.mp hw

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
p₀ : G.Walk u w
p₁ : G.Walk w v
hp₀ : p₀.IsPath
hp₁ : p₁.IsPath
happend : p = p₀.append p₁
⊢ v ∉ q.support
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
⊢ v ∉ q.support

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∈ q.support
⊢ q = p.concat hadj

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
hh : u' ∈ tail.support
⊢ [] ++ (cons head (tail.takeUntil u' hh)).support.tail ++ (tail.dropUntil u' hh).support.tail = tail.support

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
hh : u' ∈ tail.support
this : (cons head (tail.takeUntil u' hh)).support.tail.Nodup
hhh : s(u', v') ∈ (tail.takeUntil u' hh).edges
⊢ ¬tail.Nil

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w : V
p : G.Walk v w
⊢ p.IsPath ↔ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) p.edges

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this : Nonempty V
inhabited_h : Inhabited V
⊢ {default}ᶜ.card + 1 = Fintype.card V

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
x✝ : ∃ G, p G
G : SimpleGraph V
hp : p G
⊢ G ∈ {G | p G}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
x✝ : ∃ G, p G
G : SimpleGraph V
hp : p G
⊢ ?m.66

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
x✝ : ∃ G, p G
G : SimpleGraph V
hp : p G
G' : SimpleGraph V
hp' : G' ∈ {G | p G}
h : ∀ x' ∈ {G | p G}, #x'.edgeFinset ≤ #G'.edgeFinset
⊢ p G'

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
x✝² : ∃ G, p G
G : SimpleGraph V
hp✝ : p G
G' : SimpleGraph V
hp' : G' ∈ {G | p G}
h : ∀ x' ∈ {G | p G}, #x'.edgeFinset ≤ #G'.edgeFinset
x✝¹ : SimpleGraph V
x✝ : DecidableRel x✝¹.Adj
hp : p x✝¹
⊢ ?m.149 ∈ {G | p G}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
x✝² : ∃ G, p G
G : SimpleGraph V
hp✝ : p G
G' : SimpleGraph V
hp' : G' ∈ {G | p G}
h : ∀ x' ∈ {G | p G}, #x'.edgeFinset ≤ #G'.edgeFinset
x✝¹ : SimpleGraph V
x✝ : DecidableRel x✝¹.Adj
hp : p x✝¹
⊢ #x✝¹.edgeFinset ≤ #G'.edgeFinset

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
⊢ (∃ G x, G.IsExtremal p) ↔ ∃ G, p G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
w : V
hw : w ∈ {default}ᶜ
⊢ w ≠ default

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i : V
⊢ ¬A i i = 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ {x | H.Free x}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
⊢ ¬A i j = 1 ↔ A i j = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
⊢ ¬A i j = 0 ↔ A i j = 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ {x | H.Free x}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsAdjMatrix
⊢ A.diag = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsAdjMatrix
f : W → V
i j : W
⊢ A.submatrix f f i j = 0 ∨ A.submatrix f f i j = 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsAdjMatrix
f : W → V
i : W
⊢ A.submatrix f f i i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
⊢ extremalNumber n H = {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ G ∈ {G | H.Free G}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card V) H

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
f : W → V
hf : Function.Surjective f
⊢ (A.submatrix f f).IsAdjMatrix ↔ A.IsAdjMatrix

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : extremalNumber (Fintype.card V) H < #G.edgeFinset
⊢ H ⊑ G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
hij : A i j = 1
⊢ A j i = 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
h : A.IsAdjMatrix
⊢ DecidableRel h.toGraph.Adj

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
h : ∀ (b : SimpleGraph V), H.Free b → #b.edgeFinset ≤ m
x✝¹ : SimpleGraph V
x✝ : DecidableRel x✝¹.Adj
h' : H.Free x✝¹
⊢ #x✝¹.edgeFinset ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
f : W → V
⊢ ∀ {a b : W}, ⋯.toGraph.Adj a b → h.toGraph.Adj (f a) (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
h : ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m
x✝ : SimpleGraph V
h' : H.Free x✝
⊢ #x✝.edgeFinset ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
f : W ↪ V
⊢ ∀ {a b : W}, h.toGraph.Adj (f a) (f b) ↔ ⋯.toGraph.Adj a b

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ extremalNumber (Fintype.card V) H ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
f : V ≃ W
⊢ ∀ {a b : W}, h.toGraph.Adj (f.symm a) (f.symm b) ↔ ⋯.toGraph.Adj a b

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
x✝ : ∃ G x, H.Free G ∧ m < #G.edgeFinset
w✝¹ : SimpleGraph V
w✝ : DecidableRel w✝¹.Adj
h : H.Free w✝¹
h' : m < #w✝¹.edgeFinset
⊢ m < #w✝¹.edgeFinset

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ m < extremalNumber (Fintype.card V) H ↔ ∃ G x, H.Free G ∧ m < #G.edgeFinset

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝ : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
⊢ A ⊙ A = A

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : Fintype V
R : Type u_3
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ ↑(extremalNumber (Fintype.card V) H) ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → ↑(#G.edgeFinset) ≤ m

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝² : DecidableEq V
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
A : Matrix V V α
⊢ A.IsAdjMatrix ↔ A ⊙ A = A ∧ A.IsSymm ∧ 1 ⊙ A = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i : V
⊢ A.compl i i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : Fintype V
R : Type u_3
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ m < ↑(extremalNumber (Fintype.card V) H) ↔ ∃ G x, H.Free G ∧ m < ↑(#G.edgeFinset)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ A.compl i j = 0 ∨ A.compl i j = 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
⊢ extremalNumber n H' ≤ extremalNumber n H

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsSymm
⊢ A.compl.IsSymm

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A B : Matrix V V α
hA : A.IsAdjMatrix
hB : B.IsAdjMatrix
h : A.compl = B.compl
i j : V
⊢ A i j = B i j

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₁ H₁ = extremalNumber n₂ H₂

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A : Matrix V V α
hA : A.IsAdjMatrix
⊢ A.compl.compl = A

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
⊢ a ≠ default

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.IsExtremal H.Free ↔ H.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) H

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
⊢ ⋯.toGraph = h.toGraphᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝¹ : Zero α
inst✝ : One α
⊢ adjMatrix α ⊥ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝¹ : DecidableEq V
inst✝ : Ring α
⊢ adjMatrix α ⊤ = of fun i j ↦ if i = j then 0 else 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
⊢ (adjMatrix α G)ᵀ = adjMatrix α G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : H.Free G
v : V
⊢ #(G.deleteIncidenceSet v).edgeFinset ≤ extremalNumber (Fintype.card V - 1) H

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
⊢ ∀ (i j : V), adjMatrix α G i j = 0 ∨ adjMatrix α G i j = 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h' : (f a).length ≤ (f b).length
h : (f a).firstDart ⋯ = ((f b).firstDart ⋯).symm
h1 : ((f a).firstDart ⋯).toProd.2 = b
h3 : (f a).tail.length + 1 = (f b).length + 1
⊢ a ≠ default

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
⊢ (adjMatrix α G).diag = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
⊢ ⋯.toGraph = G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : DecidableEq α
inst✝¹ : Zero α
inst✝ : One α
⊢ (adjMatrix α G).compl = adjMatrix α Gᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Zero α
inst✝¹ : One α
H : SimpleGraph W
inst✝ : DecidableRel H.Adj
f : G ↪g H
⊢ (adjMatrix α H).submatrix ⇑f ⇑f = adjMatrix α G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : AddZeroClass α
inst✝¹ : One α
H : SimpleGraph V
inst✝ : DecidableRel H.Adj
h : IsCompl G H
⊢ adjMatrix α G + adjMatrix α H = adjMatrix α G + adjMatrix α Gᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : AddZeroClass α
inst✝¹ : One α
H : SimpleGraph V
inst✝ : DecidableRel H.Adj
h : IsCompl G H
⊢ adjMatrix α G + adjMatrix α Gᶜ = adjMatrix α (completeGraph V)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : DecidableEq α
inst✝¹ : AddMonoid α
inst✝ : One α
⊢ 1 + adjMatrix α G + (adjMatrix α G).compl = of 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq V
⊢ (adjMatrix α (completeGraph V)).compl = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq V
⊢ Matrix.compl 0 = adjMatrix α (completeGraph V)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝² : AddGroup α
inst✝¹ : One α
inst✝ : DecidableEq V
⊢ adjMatrix α (completeGraph V) = of 1 - 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : AddGroup α
inst✝² : One α
inst✝¹ : DecidableEq V
inst✝ : DecidableEq α
⊢ Matrix.compl 0 = of 1 - 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : AddGroup α
inst✝² : One α
inst✝¹ : DecidableEq V
inst✝ : DecidableEq α
⊢ (of 1 - 1).compl = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : MulZeroOneClass α
⊢ adjMatrix α G ⊙ adjMatrix α G = adjMatrix α G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ adjMatrix α G v ⬝ᵥ vec = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ vec ⬝ᵥ adjMatrix α G v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (adjMatrix α G *ᵥ vec) v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (vec ᵥ* adjMatrix α G) v = ∑ u ∈ G.neighborFinset v, vec u

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
M : Matrix V V α
v w : V
⊢ (adjMatrix α G * M) v w = ∑ u ∈ G.neighborFinset v, M u w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
M : Matrix V V α
v w : V
⊢ (M * adjMatrix α G) v w = ∑ u ∈ G.neighborFinset w, M v u

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : AddCommMonoid α
inst✝ : One α
⊢ (adjMatrix α G).trace = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
i : V
⊢ (adjMatrix α G * adjMatrix α G) i i = ↑(G.degree i)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
⊢ ↑(Fintype.card G.Dart) = adjMatrix α G *ᵥ 1 ⬝ᵥ 1

Tactic:
by

Goal state after: