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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f : G →g G'
h : (Walk.map f p).IsPath
⊢ Set.InjOn ⇑f {w | w ∈ p.support}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
⊢ G.IsClique (Set.range ⇑f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.IsNClique n ∅ ↔ n = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
a : α
⊢ G.IsNClique n {a} ↔ n = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ G.IsNClique n s → H.IsNClique n s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑(map f s)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ n - 1 ≤ p.tail.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ m - 1 ≤ p.tail.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ p.tail.getVert (n - 1) = p.tail.getVert (m - 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a e ∧ G.Adj b e ∧ {a, b, e} = {a, b, e}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ Set.InjOn p.getVert {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ ¬(#t ≤ 1 ∧ #t = n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj a d
hce : G.Adj a b
hde : G.Adj b d
⊢ G.Adj a d ∧ G.Adj b d ∧ {a, d, b} = {a, b, d}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.reverse.length - n ∈ {i | 1 ≤ i ∧ i ≤ p.reverse.length}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.reverse.length - m ∈ {i | 1 ≤ i ∧ i ≤ p.reverse.length}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (SimpleGraph.map (⇑f) G).IsNClique n t ↔ ∃ s, G.IsNClique n s ∧ map f s = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ ⊥.IsNClique n s ↔ n ≤ 1 ∧ #s = n

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.reverse.getVert (p.reverse.length - n) = p.reverse.getVert (p.reverse.length - m)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ G.IsNClique 0 s ↔ s = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ G.IsNClique 1 s ↔ ∃ a, s = {a}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ Set.InjOn p.getVert {i | i ≤ p.length - 1}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ p.length - 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
⊢ p.snd ≠ p.penultimate

Tactic:
by

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

Goal state before:
pp: case card_eq
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ #(insert a s) = n + 1

Tactic:
rw [card_insert_of_notMem fun ha => (h _ ha).ne rfl, hs.2]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ i = 0 ∨ i = p.length → p.getVert i = u

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsNClique (n + 1) (insert a s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a e ∧ G.Adj b e ∧ {b, a, e} = {a, b, e}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
⊢ ↑(s.erase a) ⊆ ↑s

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u → ¬i = 0 → i = p.length

Tactic:
intro h hi

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i = p.length
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
⊢ #(s.erase a) = n - 1

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ i ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
n✝ : ℕ
hs : G.IsNClique (n✝ + 1) s
w : α
h : w ∈ s.erase b
⊢ G.Adj a w

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hde : G.Adj a b
hcd : G.Adj a c
hce : G.Adj b c
⊢ G.Adj a c ∧ G.Adj b c ∧ {c, a, b} = {a, b, c}

Tactic:
by

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

Goal state before:
pp: case succ
α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
n✝ : ℕ
hs : G.IsNClique (n✝ + 1) s
⊢ G.IsNClique (n✝ + 1) (insert a (s.erase b))

Tactic:
| succ _ =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ p.length ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a b : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
⊢ G.IsNClique n (insert a (s.erase b))

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u ↔ i = 0 ∨ i = p.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ p.length ≤ i + 1

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = u
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ i - 1 ≤ p.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ i - 1 ∈ {i | i ≤ p.length - 1}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a d ∧ G.Adj b d ∧ {b, d, a} = {a, b, d}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ i + 1 ∈ {i | i ≤ p.length - 1}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝ : V
h' : G.Adj u v✝
p : G.Walk v✝ u
x✝ : (cons h' p).tail.IsPath ∧ 3 ≤ (cons h' p).length
h₂ : 3 ≤ p.length + 1
h₁ : p.IsPath
hh : s(u, v✝) ∈ p.edges
⊢ p.support[0] = p.support[p.length - 1]

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.IsCycle ↔ p.tail.IsPath ∧ 3 ≤ p.length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ G.Adj a c ∧ G.Adj b c ∧ {c, b, a} = {a, b, c}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsTrail
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsPath
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsPath

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
x : V
w : G.Walk u v
hw : w.IsTrail
hx : x ∈ w.support
⊢ ((w.takeUntil x hx).edges ++ (w.dropUntil x hx).edges).Nodup

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
⊢ (c.rotate u hu).IsTrail ↔ c.IsTrail

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
⊢ G.IsNClique 3 s ↔ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
⊢ (c.rotate u hu).IsCircuit ↔ c.IsCircuit

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
⊢ (c.rotate u hu).IsCycle ↔ c.IsCycle

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
⊢ (c.takeUntil w h).IsPath

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
⊢ List.count v c.support = 2

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
hu : u ∈ c.support
hv : u ≠ v
⊢ List.count u c.support = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
x✝ : ∃ s a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
w✝² : Finset α
a w✝¹ w✝ : α
hab : G.Adj a w✝¹
hac : G.Adj a w✝
hbc : G.Adj w✝¹ w✝
right✝ : w✝² = {a, w✝¹, w✝}
⊢ ((Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil))).IsTrail ∧
      Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil)) ≠ nil ∧
        (Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil))).support.tail.Nodup) ∧
    (Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil))).length = 3

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
⊢ {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ s, G.IsNClique 3 s) ↔ ∃ u w, w.IsCycle ∧ w.length = 3

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ n ∈ {i | i ≤ p.length}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ p.length ∈ {i | i ≤ p.length}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
⊢ v ∉ (p.takeUntil w hw).support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsNClique n s
⊢ G.IsNClique n (map { toFun := Subtype.val, inj' := ⋯ } s)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
i j : ℕ
x✝³ : i < p.support.length
x✝² : j < p.support.length
x✝¹ : i < j
x✝ : p.support[i] = p.support[j]
p' : G.Walk ((p.take j).getVert i) (p.getVert j) := (p.take j).drop i
⊢ ¬p'.Nil

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
⊢ p.IsPath → ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
v w : α
s : Finset α
n : ℕ
hc : (G ⊔ edge v w).IsNClique n s
hx : v ∈ s
⊢ #(s.erase v) = n - 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝ : Fintype β
f : ⊤.Copy G
⊢ G.IsNClique (Fintype.card β) (map f.toEmbedding univ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
t : Finset ↑s
n : ℕ
⊢ (induce s G).IsNClique n t ↔ G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) t)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle
⊢ p.IsPath

Tactic:
match p with
  | .nil => simp
  | .cons hadj p =>
    have hp := isPath_iff_isSubwalk_imp_not_isCycle ht.of_cons |>.mpr (h · · <| ·.cons hadj)
    refine cons_isPath_iff .. |>.mpr ⟨hp, fun hup ↦ h u (p.takeUntil u hup |>.cons hadj) ?_ ?_⟩
    · rw [isSubwalk_iff_support_isInfix, support_cons, support_cons]
      exact (List.prefix_cons_inj u |>.mpr <| p.support_takeUntil_prefix_support hup).isInfix
    · refine cons_isCycle_iff .. |>.mpr ⟨hp.takeUntil hup, fun he ↦ ?_⟩
      exact ht.edges_nodup.notMem <| p.edges_takeUntil_subset_edges hup he

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
⊢ p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
h : G.Adj u v
⊢ (Walk.cons h Walk.nil).IsPath

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ s(u, v) ∈ (↑(singleton h)).edges

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
h : completeGraph (Fin n) ⊑ G
⊢ ¬G.CliqueFree n

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Path v v
⊢ p = Path.nil

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
p : G.Path v v
⊢ e ∉ (↑p).edges

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Path v u
h : G.Adj u v
he : s(u, v) ∉ (↑p).edges
⊢ (Walk.cons h ↑p).IsCycle

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
this : p.length - 1 = 0
⊢ p.length = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ¬G.CliqueFree n
⊢ completeGraph (Fin n) ↪g G

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.CliqueFree n ↔ IsEmpty ((completeGraph (Fin n)).Copy G)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ p.length = 1

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ p.length = ⋯.toWalk.length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
β : Type u_3
inst✝ : Fintype β
⊢ G.CliqueFree (Fintype.card β) ↔ ⊤.Free G

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Fintype α
f : completeGraph α ⊑ G
⊢ ¬G.CliqueFree (Fintype.card α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : 2 ≤ n
⊢ ⊥.CliqueFree n

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ p = ⋯.toWalk

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
⊢ G.CliqueFree m → G.CliqueFree n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : G.CliqueFree n
⊢ H.CliqueFree n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst✝ : Nonempty α
⊢ (SimpleGraph.map (⇑f) G).CliqueFree n ↔ G.CliqueFree n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
⊢ G.CliqueFree n

Tactic:
by

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

Goal state before:
pp: n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
⊢ Fintype.card ι < Fintype.card (Fin n)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hd : p.support.tail.Disjoint q.support.tail
hl : p.length ≠ 1
⊢ p.edges.Disjoint q.edges

Tactic:
by

Goal state after: