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

Goal state before:
pp: case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
v : V
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inl (Sum.inl v)) =
    ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inl (Sum.inl v))

pp: case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
w : W
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inl (Sum.inr w)) =
    ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inl (Sum.inr w))

pp: case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
u : U
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inr u) = ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inr u)

Tactic:
<;>

Goal state after:
case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
v : V
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inl (Sum.inl v)) =
    ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inl (Sum.inl v))

case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
w : W
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inl (Sum.inr w)) =
    ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inl (Sum.inr w))

case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
u : U
⊢ (sumAssoc.comp ((f.sumCongr g).sumCongr h)) (Sum.inr u) = ((f.sumCongr (g.sumCongr h)).comp sumAssoc) (Sum.inr u)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
v : V ⊕ W
val✝ : V
huv : (G ⊕g H).Adj (Sum.inl val✝) v
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝)) (Sum.elim (⇑cG) (⇑cH) v)

pp: case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
v : V ⊕ W
val✝ : W
huv : (G ⊕g H).Adj (Sum.inr val✝) v
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝)) (Sum.elim (⇑cG) (⇑cH) v)

Tactic:
<;>

Goal state after:
case inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
v : V ⊕ W
val✝ : V
huv : (G ⊕g H).Adj (Sum.inl val✝) v
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝)) (Sum.elim (⇑cG) (⇑cH) v)

case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
cG : G.Coloring γ
cH : H.Coloring γ
v : V ⊕ W
val✝ : W
huv : (G ⊕g H).Adj (Sum.inr val✝) v
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝)) (Sum.elim (⇑cG) (⇑cH) v)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
u : V
⊢ (c.sumLeft.sum c.sumRight) (Sum.inl u) = c (Sum.inl u)

pp: case inr
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
u : W
⊢ (c.sumLeft.sum c.sumRight) (Sum.inr u) = c (Sum.inr u)

Tactic:
<;>

Goal state after:
case inl
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
u : V
⊢ (c.sumLeft.sum c.sumRight) (Sum.inl u) = c (Sum.inl u)

case inr
V : Type u_3
W : Type u_5
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
c : (G ⊕g H).Coloring γ
u : W
⊢ (c.sumLeft.sum c.sumRight) (Sum.inr u) = c (Sum.inr u)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v v' : V
⊢ Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔ Sum.inl v' ∈ Sum.inl '' G.neighborSet v

pp: case inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w' : W
⊢ Sum.inr w' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔ Sum.inr w' ∈ Sum.inl '' G.neighborSet v

Tactic:
<;>

Goal state after:
case inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v v' : V
⊢ Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔ Sum.inl v' ∈ Sum.inl '' G.neighborSet v

case inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w' : W
⊢ Sum.inr w' ∈ (G ⊕g H).neighborSet (Sum.inl v) ↔ Sum.inr w' ∈ Sum.inl '' G.neighborSet v
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w : W
v' : V
⊢ Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔ Sum.inl v' ∈ Sum.inr '' H.neighborSet w

pp: case inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w w' : W
⊢ Sum.inr w' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔ Sum.inr w' ∈ Sum.inr '' H.neighborSet w

Tactic:
<;>

Goal state after:
case inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w : W
v' : V
⊢ Sum.inl v' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔ Sum.inl v' ∈ Sum.inr '' H.neighborSet w

case inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
w w' : W
⊢ Sum.inr w' ∈ (G ⊕g H).neighborSet (Sum.inr w) ↔ Sum.inr w' ∈ Sum.inr '' H.neighborSet w
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
v : V
⊢ Fintype ↑((G ⊕g H).neighborSet (Sum.inl v))

pp: case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w✝ w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
w : W
⊢ Fintype ↑((G ⊕g H).neighborSet (Sum.inr w))

Tactic:
<;>

Goal state after:
case inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
v : V
⊢ Fintype ↑((G ⊕g H).neighborSet (Sum.inl v))

case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w✝ w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
w : W
⊢ Fintype ↑((G ⊕g H).neighborSet (Sum.inr w))
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
v : V
⊢ Fintype ↑(Sum.inl '' G.neighborSet v)

pp: case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w✝ w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
w : W
⊢ Fintype ↑(Sum.inr '' H.neighborSet w)

Tactic:
<;>

Goal state after:
case inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
v : V
⊢ Fintype ↑(Sum.inl '' G.neighborSet v)

case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w✝ w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
w : W
⊢ Fintype ↑(Sum.inr '' H.neighborSet w)
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: case «0»
v : Fin 2
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨0, ⋯⟩) v ↔ ⊤.Adj ((fun i ↦ i) ⟨0, ⋯⟩) v

pp: case «1»
v : Fin 2
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨1, ⋯⟩) v ↔ ⊤.Adj ((fun i ↦ i) ⟨1, ⋯⟩) v

Tactic:
<;>

Goal state after:
case «0»
v : Fin 2
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨0, ⋯⟩) v ↔ ⊤.Adj ((fun i ↦ i) ⟨0, ⋯⟩) v

case «1»
v : Fin 2
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨1, ⋯⟩) v ↔ ⊤.Adj ((fun i ↦ i) ⟨1, ⋯⟩) v
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case succ.zero
n n✝ : ℕ
a✝ : ∀ (m : ℕ) (hm : m < n + 3), n✝ ≤ ↑⟨m, hm⟩ → ↑((cycleCons n ⟨m, hm⟩).getVert n✝) = (↑⟨m, hm⟩ - n✝) % (n + 3)
hm : 0 < n + 3
hi : n✝ + 1 ≤ ↑⟨0, hm⟩
⊢ ↑((cycleCons n ⟨0, hm⟩).getVert (n✝ + 1)) = (↑⟨0, hm⟩ - (n✝ + 1)) % (n + 3)

pp: case succ.succ
n n✝¹ : ℕ
a✝ : ∀ (m : ℕ) (hm : m < n + 3), n✝¹ ≤ ↑⟨m, hm⟩ → ↑((cycleCons n ⟨m, hm⟩).getVert n✝¹) = (↑⟨m, hm⟩ - n✝¹) % (n + 3)
n✝ : ℕ
hm : n✝ + 1 < n + 3
hi : n✝¹ + 1 ≤ ↑⟨n✝ + 1, hm⟩
⊢ ↑((cycleCons n ⟨n✝ + 1, hm⟩).getVert (n✝¹ + 1)) = (↑⟨n✝ + 1, hm⟩ - (n✝¹ + 1)) % (n + 3)

Tactic:
<;>

Goal state after:
case succ.zero
n n✝ : ℕ
a✝ : ∀ (m : ℕ) (hm : m < n + 3), n✝ ≤ ↑⟨m, hm⟩ → ↑((cycleCons n ⟨m, hm⟩).getVert n✝) = (↑⟨m, hm⟩ - n✝) % (n + 3)
hm : 0 < n + 3
hi : n✝ + 1 ≤ ↑⟨0, hm⟩
⊢ ↑((cycleCons n ⟨0, hm⟩).getVert (n✝ + 1)) = (↑⟨0, hm⟩ - (n✝ + 1)) % (n + 3)

case succ.succ
n n✝¹ : ℕ
a✝ : ∀ (m : ℕ) (hm : m < n + 3), n✝¹ ≤ ↑⟨m, hm⟩ → ↑((cycleCons n ⟨m, hm⟩).getVert n✝¹) = (↑⟨m, hm⟩ - n✝¹) % (n + 3)
n✝ : ℕ
hm : n✝ + 1 < n + 3
hi : n✝¹ + 1 ≤ ↑⟨n✝ + 1, hm⟩
⊢ ↑((cycleCons n ⟨n✝ + 1, hm⟩).getVert (n✝¹ + 1)) = (↑⟨n✝ + 1, hm⟩ - (n✝¹ + 1)) % (n + 3)
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: case «0».«0»
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ↔ ⊤.Adj ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ↔ ⊤.Adj ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«0»
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ↔ ⊤.Adj ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«1»
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ↔ ⊤.Adj ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ↔ ⊤.Adj ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ↔ ⊤.Adj ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ↔ ⊤.Adj ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
⊢ (pathGraph 2).Adj ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ↔ ⊤.Adj ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

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

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

Tactic:
<;>

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

case inr
α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
i j : V
h : A i j = 1
⊢ ¬A i j = 1 ↔ A i j = 0
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 = 1

Tactic:
Classical.not_not

Goal state after:
α : 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 = 1
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
h : (A.submatrix f f).IsAdjMatrix
⊢ A.IsAdjMatrix

Tactic:
← A.submatrix_id_id,

Goal state after:
α : 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
h : (A.submatrix f f).IsAdjMatrix
⊢ (A.submatrix id id).IsAdjMatrix
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

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

pp: case inr
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

case inr
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: case pos
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

pp: case neg
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : ¬v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

pp: case pos
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

pp: case neg
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : ¬v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

case neg
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : ¬v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

case pos
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

case neg
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : ¬v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

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

pp: case inr
α : Type u_1
V : Type u_2
inst✝¹ : DecidableEq V
inst✝ : Ring α
i j : V
h✝ : i ≠ j
⊢ adjMatrix α ⊤ i j = of (fun i j ↦ if i = j then 0 else 1) i j

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
V : Type u_2
inst✝¹ : DecidableEq V
inst✝ : Ring α
i j : V
h✝ : i = j
⊢ adjMatrix α ⊤ i j = of (fun i j ↦ if i = j then 0 else 1) i j

case inr
α : Type u_1
V : Type u_2
inst✝¹ : DecidableEq V
inst✝ : Ring α
i j : V
h✝ : i ≠ j
⊢ adjMatrix α ⊤ i j = of (fun i j ↦ if i = j then 0 else 1) i j
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: case zero.inl
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u : V
⊢ (adjMatrix α G ^ 0) u u = ↑(#(G.finsetWalkLength 0 u u))

pp: case zero.inr
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u v : V
h : u ≠ v
⊢ (adjMatrix α G ^ 0) u v = ↑(#(G.finsetWalkLength 0 u v))

Tactic:
<;>

Goal state after:
case zero.inl
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u : V
⊢ (adjMatrix α G ^ 0) u u = ↑(#(G.finsetWalkLength 0 u u))

case zero.inr
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u v : V
h : u ≠ v
⊢ (adjMatrix α G ^ 0) u v = ↑(#(G.finsetWalkLength 0 u v))
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: case inl
α : Type u_1
V : Type u_2
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst✝ : DecidableEq α
i j : V
h' : A i j = 0
⊢ adjMatrix α h.toGraph i j = A i j

pp: case inr
α : Type u_1
V : Type u_2
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst✝ : DecidableEq α
i j : V
h' : A i j = 1
⊢ adjMatrix α h.toGraph i j = A i j

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
V : Type u_2
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst✝ : DecidableEq α
i j : V
h' : A i j = 0
⊢ adjMatrix α h.toGraph i j = A i j

case inr
α : Type u_1
V : Type u_2
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst✝ : DecidableEq α
i j : V
h' : A i j = 1
⊢ adjMatrix α h.toGraph i j = A i j
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case inl
n : ℕ
u v : Fin n
h : ↑u + 1 = ↑v
⊢ decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)

pp: case inr
n : ℕ
u v : Fin n
h : ↑v + 1 = ↑u
⊢ decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)

Tactic:
<;>

Goal state after:
case inl
n : ℕ
u v : Fin n
h : ↑u + 1 = ↑v
⊢ decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)

case inr
n : ℕ
u v : Fin n
h : ↑v + 1 = ↑u
⊢ decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
this : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
⊢ False

Tactic:
have : v ∉ s := this ∘ s.reachable_of_mem_supp rfl

Goal state after:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
this✝ : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this : v ∉ s
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬(c u = true ↔ c v = true)

Tactic:
← Bool.eq_iff_iff

Goal state after:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬c u = c v
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case inl
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : u - v = 1
⊢ ¬(↑u % 2 = 0 ↔ ↑v % 2 = 0)

Tactic:
rw [← add_eq_of_eq_sub' huv.symm, ← Fin.even_iff_mod_of_even h,
          ← Fin.even_iff_mod_of_even h, Fin.even_add_one_iff_odd]
        apply Classical.not_iff.mpr
        simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case inr
n✝ n : ℕ
h : Even (n + 2)
u v : Fin (n + 2)
huv : v - u = 1
⊢ ¬(↑u % 2 = 0 ↔ ↑v % 2 = 0)

Tactic:
rw [← add_eq_of_eq_sub' huv.symm, ← Fin.even_iff_mod_of_even h,
          ← Fin.even_iff_mod_of_even h, Fin.even_add_one_iff_odd]
        apply Classical.not_iff.mpr
        simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case neg.inl
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ¬(↑v + 1) % 2 = ↑v % 2

Tactic:
show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; lia,

Goal state after:
case neg.inl
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ¬(Even (↑v + 1) ↔ Even ↑v)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case neg.inr
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ¬↑u % 2 = (↑u + 1) % 2

Tactic:
show ∀ x y : ℕ, x % 2 = y % 2 ↔ (Even x ↔ Even y) by simp [Nat.even_iff]; lia,

Goal state after:
case neg.inr
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ¬(Even ↑u ↔ Even (↑u + 1))