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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).support = List.drop (min 0 nil.length) nil.support

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).support = List.drop (min (n✝ + 1) nil.length) nil.support

pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).support = List.drop (min n p✝.length) p✝.support
⊢ ((cons h✝ p✝).drop 0).support = List.drop (min 0 (cons h✝ p✝).length) (cons h✝ p✝).support

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).support = List.drop (min n p✝.length) p✝.support
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).support = List.drop (min (n✝ + 1) (cons h✝ p✝).length) (cons h✝ p✝).support

Tactic:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).support = List.drop (min 0 nil.length) nil.support

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).support = List.drop (min (n✝ + 1) nil.length) nil.support

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).support = List.drop (min n p✝.length) p✝.support
⊢ ((cons h✝ p✝).drop 0).support = List.drop (min 0 (cons h✝ p✝).length) (cons h✝ p✝).support

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).support = List.drop (min n p✝.length) p✝.support
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).support = List.drop (min (n✝ + 1) (cons h✝ p✝).length) (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
⊢ n = m

Tactic:
by_cases hn0 : n = 0 <;> by_cases hm0 : m = 0

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : n = 0
hm0 : m = 0
⊢ n = m

case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : n = 0
hm0 : ¬m = 0
⊢ n = m

case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : m = 0
⊢ n = m

case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : ¬m = 0
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ (p.drop n).drop m = (p.drop (n + m)).copy ⋯ ⋯

Tactic:
apply ext_support
  simp_rw [support_copy, drop_support_eq_support_drop_min, drop_length, List.drop_drop]
  grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).tail = nil.copy ⋯ ⋯

pp: case cons
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ (cons h (cons h✝ p✝)).tail = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).tail = nil.copy ⋯ ⋯

case cons
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ (cons h (cons h✝ p✝)).tail = (cons h✝ p✝).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ cons h✝ ((p✝.concat h).dropLast.copy ⋯ ⋯) = (cons h✝ p✝).copy ⋯ ⋯

pp: case hp
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ¬(p✝.concat h).Nil

Tactic:
<;>

Goal state after:
case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ cons h✝ ((p✝.concat h).dropLast.copy ⋯ ⋯) = (cons h✝ p✝).copy ⋯ ⋯

case hp
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ¬(p✝.concat h).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
hp : ¬nil.Nil
⊢ cons ⋯ nil.tail = nil

pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
hp : ¬(cons h✝ p✝).Nil
⊢ cons ⋯ (cons h✝ p✝).tail = cons h✝ p✝

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
hp : ¬nil.Nil
⊢ cons ⋯ nil.tail = nil

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
hp : ¬(cons h✝ p✝).Nil
⊢ cons ⋯ (cons h✝ p✝).tail = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.tail.length = nil.length - 1

pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).tail.length = (cons h✝ p✝).length - 1

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.tail.length = nil.length - 1

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).tail.length = (cons h✝ p✝).length - 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.dropLast.length = nil.length - 1

pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).dropLast.length = (cons h✝ p✝).length - 1

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.dropLast.length = nil.length - 1

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).dropLast.length = (cons h✝ p✝).length - 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
hp : Walk.nil.Nil
⊢ Walk.nil.tail.Nil

pp: case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).Nil
⊢ (cons h✝ p✝).tail.Nil

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
hp : Walk.nil.Nil
⊢ Walk.nil.tail.Nil

case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).Nil
⊢ (cons h✝ p✝).tail.Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
hp : Walk.nil.Nil
⊢ Walk.nil.dropLast.Nil

pp: case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).Nil
⊢ (cons h✝ p✝).dropLast.Nil

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
hp : Walk.nil.Nil
⊢ Walk.nil.dropLast.Nil

case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).Nil
⊢ (cons h✝ p✝).dropLast.Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ nil.tail.getVert n = nil.getVert (n + 1)

pp: case cons
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).tail.getVert n = (cons h✝ p✝).getVert (n + 1)

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ nil.tail.getVert n = nil.getVert (n + 1)

case cons
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).tail.getVert n = (cons h✝ p✝).getVert (n + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
⊢ G.IsClique (Subtype.val '' A)

Tactic:
by
  simp only [Set.Pairwise, Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
  intro _ ⟨_, ainA⟩ _ ⟨_, binA⟩ anb
  exact S.adj_sub (c ainA binA (Subtype.coe_ne_coe.mp anb)).2.2

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.LocallyLinear

Tactic:
simp [LocallyLinear]

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.LocallyLinear

Tactic:
by simp [LocallyLinear]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
hp : Walk.nil.IsPath
hnil : ¬Walk.nil.Nil
hmem : ((u✝, w) = (u✝, Walk.nil.snd) ∨ (u✝, w) = (u✝, Walk.nil.snd).swap) ∨ s(u✝, w) ∈ Walk.nil.tail.edges
⊢ u✝ ∉ Walk.nil.tail.support

pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  p✝.IsPath →
    ¬p✝.Nil → ((v✝, w) = (v✝, p✝.snd) ∨ (v✝, w) = (v✝, p✝.snd).swap) ∨ s(v✝, w) ∈ p✝.tail.edges → v✝ ∉ p✝.tail.support
hp : (cons h✝ p✝).IsPath
hnil : ¬(cons h✝ p✝).Nil
hmem : ((u✝, w) = (u✝, (cons h✝ p✝).snd) ∨ (u✝, w) = (u✝, (cons h✝ p✝).snd).swap) ∨ s(u✝, w) ∈ (cons h✝ p✝).tail.edges
⊢ u✝ ∉ (cons h✝ p✝).tail.support

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
hp : Walk.nil.IsPath
hnil : ¬Walk.nil.Nil
hmem : ((u✝, w) = (u✝, Walk.nil.snd) ∨ (u✝, w) = (u✝, Walk.nil.snd).swap) ∨ s(u✝, w) ∈ Walk.nil.tail.edges
⊢ u✝ ∉ Walk.nil.tail.support

case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  p✝.IsPath →
    ¬p✝.Nil → ((v✝, w) = (v✝, p✝.snd) ∨ (v✝, w) = (v✝, p✝.snd).swap) ∨ s(v✝, w) ∈ p✝.tail.edges → v✝ ∉ p✝.tail.support
hp : (cons h✝ p✝).IsPath
hnil : ¬(cons h✝ p✝).Nil
hmem : ((u✝, w) = (u✝, (cons h✝ p✝).snd) ∨ (u✝, w) = (u✝, (cons h✝ p✝).snd).swap) ∨ s(u✝, w) ∈ (cons h✝ p✝).tail.edges
⊢ u✝ ∉ (cons h✝ p✝).tail.support
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
h✝ : x = v
⊢ Sym2.ToRel {s(v, w)} x y

pp: case neg
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
h✝ : ¬x = v
⊢ Sym2.ToRel {s(v, w)} x y

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
h✝ : x = v
⊢ Sym2.ToRel {s(v, w)} x y

case neg
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
h✝ : ¬x = v
⊢ Sym2.ToRel {s(v, w)} x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

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

Tactic:
isClique_bot_iff

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
⊢ (↑s).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ (↑s).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n

Tactic:
refine and_congr_left ?_

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
⊢ #s = n → ((↑s).Subsingleton ↔ n ≤ 1)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

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

pp: case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
Module: Mathlib.Combinatorics.SimpleGraph.Clique

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

pp: case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : ¬b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

pp: case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

pp: case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : ¬b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
Module: Mathlib.Combinatorics.SimpleGraph.Clique

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

pp: case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

pp: case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : ¬b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

pp: case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : ¬b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

pp: case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

pp: case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

pp: case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

pp: case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : ¬b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : a = b
hbc : ¬b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case pos
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
hac : a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

case neg
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
hac : ¬a = c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mpr.refine_1
α : Type u_1
G : SimpleGraph α
a b : α
hab✝ : a ≠ b
hab : G.Adj a b
c : α
hac : G.Adj a c
hbc : G.Adj b c
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ {a, b, c} = {a, b, c}

pp: case mpr.refine_2
α : Type u_1
G : SimpleGraph α
a b : α
hab✝ : a ≠ b
hab : G.Adj a b
c : α
hac : G.Adj a c
hbc : G.Adj b c
⊢ a ∈ {a, b, c} ∧ b ∈ {a, b, c}

Tactic:
<;>

Goal state after:
case mpr.refine_1
α : Type u_1
G : SimpleGraph α
a b : α
hab✝ : a ≠ b
hab : G.Adj a b
c : α
hac : G.Adj a c
hbc : G.Adj b c
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ {a, b, c} = {a, b, c}

case mpr.refine_2
α : Type u_1
G : SimpleGraph α
a b : α
hab✝ : a ≠ b
hab : G.Adj a b
c : α
hac : G.Adj a c
hbc : G.Adj b c
⊢ a ∈ {a, b, c} ∧ b ∈ {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : False ↔ x ≠ y
⊢ completeGraph (Fin n) ⊑ G

Tactic:
false_iff,

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : ¬x ≠ y
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mpr.refine_1
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    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}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ {a, b, c} = {a, b, c}

pp: case mpr.refine_2
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    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}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ G.Adj d e ∧ G.Adj d f ∧ G.Adj e f ∧ {d, e, f} = {d, e, f}

Tactic:
<;>

Goal state after:
case mpr.refine_1
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    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}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ {a, b, c} = {a, b, c}

case mpr.refine_2
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    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}}
hG :
  ∀ ⦃e : Sym2 α⦄,
    ¬e.IsDiag → {s | (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ e ∈ s.sym2}.Subsingleton
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
d e f : α
hde : G.Adj d e
hdf : G.Adj d f
hef : G.Adj e f
g : α
hg₁ : g ∈ {a, b, c}
hg₂ : g ∈ {d, e, f}
h : α
hh₁ : h ∈ {a, b, c}
hh₂ : h ∈ {d, e, f}
hgh : ¬g = h
⊢ G.Adj d e ∧ G.Adj d f ∧ G.Adj e f ∧ {d, e, f} = {d, e, f}