awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
hs : G.IsNClique 0 s
⊢ G.IsNClique 0 (insert a (s.erase b))

Tactic:
False.elim <| notMem_empty _ (isNClique_zero.1 hs ▸ hb)

Premises used: False.elim, Finset.notMem_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
a b : α
inst : DecidableEq α
ha : ∀ w ∈ s \ {b}, G.Adj a w
hb : b ∈ s
hs : G.IsNClique 0 s
⊢ G.IsNClique 0 (insert a (s.erase b))

Tactic:
exact False.elim <| notMem_empty _ (isNClique_zero.1 hs ▸ hb)

Premises used: False.elim, Finset.notMem_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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:
exact (hs.erase_of_mem hb).insert fun w h ↦ by aesop

Premises used: SimpleGraph.IsNClique.erase_of_mem, SimpleGraph.IsNClique.insert
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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
zero : ∀ (hs : G.IsNClique 0 s), G.IsNClique 0 (insert a (s.erase b))
succ : ∀ (n : ℕ) (hs : G.IsNClique (n + 1) s), G.IsNClique (n + 1) (insert a (s.erase b))
⊢ G.IsNClique n (insert a (s.erase b))

Tactic:
cases n with
  | zero => exact False.elim <| notMem_empty _ (isNClique_zero.1 hs ▸ hb)
  | succ _ => exact (hs.erase_of_mem hb).insert fun w h ↦ by aesop

Premises used: SimpleGraph.IsNClique.erase_of_mem, False.elim, Finset.notMem_empty, SimpleGraph.IsNClique.insert
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
simp :
  (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
simp only [isNClique_iff, Set.pairwise_insert_of_symmetric G.symm, coe_insert]

Premises used: SimpleGraph.symm, Set.pairwise_insert_of_symmetric, SimpleGraph.isNClique_iff, Finset.coe_insert
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
pos :
  ∀ (hab : a = b),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
neg :
  ∀ (hab : ¬a = b),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by_cases hab : a = b
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : a = b
pos :
  ∀ (hbc : b = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
neg :
  ∀ (hbc : ¬b = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by_cases hbc : b = c
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : ¬a = b
pos :
  ∀ (hbc : b = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
neg :
  ∀ (hbc : ¬b = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by_cases hbc : b = c
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : a = b
hbc : b = c
pos :
  ∀ (hac : a = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
neg :
  ∀ (hac : ¬a = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by_cases hac : a = c
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : a = b
hbc : ¬b = c
pos :
  ∀ (hac : a = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
neg :
  ∀ (hac : ¬a = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by_cases hac : a = c
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : ¬a = b
hbc : b = c
pos :
  ∀ (hac : a = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
neg :
  ∀ (hac : ¬a = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by_cases hac : a = c
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
pos :
  ∀ (hac : a = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
neg :
  ∀ (hac : ¬a = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
        Finset.card (α := α) {a, b, c} = 3 ↔
      G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by_cases hac : a = c
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : a = b
hbc : b = c
hac : a = c
pos :
  ∀ (hac : c = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b ∈ (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
          ∀ b ∈ insert c (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
        Finset.card (α := α) {c, c, c} = 3 ↔
      G.Adj c c ∧ G.Adj c c ∧ G.Adj c c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : a = b
hbc : b = c
hac : ¬a = c
neg :
  ∀ (hac : ¬c = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b ∈ (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
          ∀ b ∈ insert c (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
        Finset.card (α := α) {c, c, c} = 3 ↔
      G.Adj c c ∧ G.Adj c c ∧ G.Adj c c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : a = b
hbc : ¬b = c
hac : a = c
pos :
  ∀ (hbc : ¬c = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b ∈ (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
          ∀ b ∈ insert c (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
        Finset.card (α := α) {c, c, c} = 3 ↔
      G.Adj c c ∧ G.Adj c c ∧ G.Adj c c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : a = b
hbc : ¬b = c
hac : ¬a = c
neg :
  ∀ (hac : ¬b = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        Finset.card (α := α) {b, b, c} = 3 ↔
      G.Adj b b ∧ G.Adj b c ∧ G.Adj b c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : ¬a = b
hbc : b = c
hac : a = c
pos :
  ∀ (hab : ¬c = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b ∈ (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
          ∀ b ∈ insert c (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
        Finset.card (α := α) {c, c, c} = 3 ↔
      G.Adj c c ∧ G.Adj c c ∧ G.Adj c c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : ¬a = b
hbc : b = c
hac : ¬a = c
neg :
  ∀ (hab : ¬a = c),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b ∈ (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
          ∀ b ∈ insert c (↑{c} : Set α), a ≠ b → G.Adj a b) ∧
        Finset.card (α := α) {a, c, c} = 3 ↔
      G.Adj a c ∧ G.Adj a c ∧ G.Adj c c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
hac : a = c
pos :
  ∀ (hab : ¬c = b),
    (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
          ∀ b_1 ∈ insert b (↑{c} : Set α), c ≠ b_1 → G.Adj c b_1) ∧
        Finset.card (α := α) {c, b, c} = 3 ↔
      G.Adj c b ∧ G.Adj c c ∧ G.Adj b c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
c : α
inst : DecidableEq α
hac : c = c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b ∈ (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
        ∀ b ∈ insert c (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
      Finset.card (α := α) {c, c, c} = 3 ↔
    G.Adj c c ∧ G.Adj c c ∧ G.Adj c c

Tactic:
simp [and_rotate, *]

Premises used: and_rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
c : α
inst : DecidableEq α
hac : ¬c = c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b ∈ (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
        ∀ b ∈ insert c (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
      Finset.card (α := α) {c, c, c} = 3 ↔
    G.Adj c c ∧ G.Adj c c ∧ G.Adj c c

Tactic:
simp [and_rotate, *]

Premises used: and_rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
c : α
inst : DecidableEq α
hbc : ¬c = c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b ∈ (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
        ∀ b ∈ insert c (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
      Finset.card (α := α) {c, c, c} = 3 ↔
    G.Adj c c ∧ G.Adj c c ∧ G.Adj c c

Tactic:
simp [and_rotate, *]

Premises used: and_rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
b c : α
inst : DecidableEq α
hbc hac : ¬b = c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
      Finset.card (α := α) {b, b, c} = 3 ↔
    G.Adj b b ∧ G.Adj b c ∧ G.Adj b c

Tactic:
simp [and_rotate, *]

Premises used: and_rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
c : α
inst : DecidableEq α
hab : ¬c = c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b ∈ (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
        ∀ b ∈ insert c (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
      Finset.card (α := α) {c, c, c} = 3 ↔
    G.Adj c c ∧ G.Adj c c ∧ G.Adj c c

Tactic:
simp [and_rotate, *]

Premises used: and_rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a c : α
inst : DecidableEq α
hac hab : ¬a = c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b ∈ (↑{c} : Set α), c ≠ b → G.Adj c b) ∧
        ∀ b ∈ insert c (↑{c} : Set α), a ≠ b → G.Adj a b) ∧
      Finset.card (α := α) {a, c, c} = 3 ↔
    G.Adj a c ∧ G.Adj a c ∧ G.Adj c c

Tactic:
simp [and_rotate, *]

Premises used: and_rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
b c : α
inst : DecidableEq α
hbc : ¬b = c
hab : ¬c = b
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), c ≠ b_1 → G.Adj c b_1) ∧
      Finset.card (α := α) {c, b, c} = 3 ↔
    G.Adj c b ∧ G.Adj c c ∧ G.Adj b c

Tactic:
simp [and_rotate, *]

Premises used: and_rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : ¬a = b
hbc : ¬b = c
hac : ¬a = c
⊢ (((↑{c} : Set α).Pairwise G.Adj ∧ ∀ b_1 ∈ (↑{c} : Set α), b ≠ b_1 → G.Adj b b_1) ∧
        ∀ b_1 ∈ insert b (↑{c} : Set α), a ≠ b_1 → G.Adj a b_1) ∧
      Finset.card (α := α) {a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
simp [and_rotate, *]

Premises used: and_rotate
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : 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:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
inst : DecidableEq α
refine_1 : ∀ (h : G.IsNClique 3 s), ∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
refine_2 : (∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) → G.IsNClique 3 s
⊢ G.IsNClique 3 s ↔ ∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
inst : DecidableEq α
h : G.IsNClique 3 s
refine_1 :
  ∀ (a b c : α) (hs : s = {a, b, c}), ∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
⊢ ∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
obtain ⟨a, b, c, -, -, -, hs⟩ := card_eq_three.1 h.card_eq

Premises used: SimpleGraph.IsNClique.card_eq, Iff.mp, Finset.card_eq_three
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
inst : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ ∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
⟨a, b, c, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
inst : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
refine_1 : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
⊢ ∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
refine ⟨a, b, c, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
inst : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
refine_1 : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, c} {a, b, c}
refine_1₁ : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ True
refine_1₂ : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
refine_1₃ : G.IsNClique 3 {a, b, c}
refine_1₄ refine_1₅ refine_1₆ refine_1₇ : G.IsNClique 3 s
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
rwa [hs, eq_self_iff_true, and_true, is3Clique_triple_iff.symm, ← hs]

Premises used: and_true, SimpleGraph.is3Clique_triple_iff, eq_self_iff_true, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
a b c : α
hab : G.Adj a b
hbc : G.Adj a c
hca : G.Adj b c
⊢ G.IsNClique 3 {a, b, c}

Tactic:
is3Clique_triple_iff.2 ⟨hab, hbc, hca⟩

Premises used: Iff.mpr, And.intro, SimpleGraph.is3Clique_triple_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
a b c : α
hab : G.Adj a b
hbc : G.Adj a c
hca : G.Adj b c
⊢ G.IsNClique 3 {a, b, c}

Tactic:
exact is3Clique_triple_iff.2 ⟨hab, hbc, hca⟩

Premises used: Iff.mpr, And.intro, SimpleGraph.is3Clique_triple_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
simp_rw :
  (∃ (s : Finset α) (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ↔
    ∃ (u : α) (w : G.Walk u u), (w.IsTrail ∧ w ≠ nil ∧ w.support.tail.Nodup) ∧ w.length = 3
⊢ (∃ (s : Finset α), G.IsNClique 3 s) ↔ ∃ (u : α) (w : G.Walk u u), w.IsCycle ∧ w.length = 3

Tactic:
simp_rw [is3Clique_iff, isCycle_def]

Premises used: SimpleGraph.Walk.isCycle_def, SimpleGraph.is3Clique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
h : ∃ (s : Finset α) (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
w : Finset α
a w_1 w_2 : α
hab : G.Adj a w_1
hac : G.Adj a w_2
hbc : G.Adj w_1 w_2
right : w = {a, w_1, w_2}
⊢ ((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:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
⊢ (∃ (s : Finset α) (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ↔
    ∃ (u : α) (w : G.Walk u u), (w.IsTrail ∧ w ≠ nil ∧ w.support.tail.Nodup) ∧ w.length = 3

Tactic:
exact
    ⟨(fun ⟨_, a, _, _, hab, hac, hbc, _⟩ => ⟨a, cons hab (cons hbc (cons hac.symm nil)), by aesop⟩),
    (fun ⟨_, .cons hab (.cons hbc (.cons hca nil)), _, _⟩ => ⟨_, _, _, _, hab, hca.symm, hbc, rfl⟩)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
simp_rw :
  (∃ (s : Finset α) (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ↔
    ∃ (u : α) (w : G.Walk u u), w.IsCycle ∧ w.length = 3
simp_rw₁ :
  (∃ (s : Finset α) (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ↔
    ∃ (u : α) (w : G.Walk u u), (w.IsTrail ∧ w ≠ nil ∧ w.support.tail.Nodup) ∧ w.length = 3
⊢ (∃ (s : Finset α), G.IsNClique 3 s) ↔ ∃ (u : α) (w : G.Walk u u), w.IsCycle ∧ w.length = 3

Tactic:
classical
  simp_rw [is3Clique_iff, isCycle_def]
  exact
    ⟨(fun ⟨_, a, _, _, hab, hac, hbc, _⟩ => ⟨a, cons hab (cons hbc (cons hac.symm nil)), by aesop⟩),
    (fun ⟨_, .cons hab (.cons hbc (.cons hca nil)), _, _⟩ => ⟨_, _, _, _, hab, hca.symm, hbc, rfl⟩)⟩

Premises used: SimpleGraph.Walk.isCycle_def, SimpleGraph.is3Clique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x : α // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsNClique n s
rw :
  ∀ (cc : (S.induce F).coe.IsClique (↑s : Set (↑(S.induce F).verts : Type u_1)) ∧ #s = n),
    G.IsClique
        (↑(map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ : { x : α // x ∈ F } ↪ α } s) : Set α) ∧
      #(map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ : { x : α // x ∈ F } ↪ α } s) = n
⊢ G.IsNClique n (map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ } s)

Tactic:
rw [isNClique_iff] at cc ⊢

Premises used: SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x : α // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsClique (↑s : Set (↑(S.induce F).verts : Type u_1)) ∧ #s = n
simp :
  G.IsClique
      ((⇑{ toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ } : (a : { x : α // x ∈ F }) → α) ''
        (↑s : Set { x : α // x ∈ F })) ∧
    #s = n
⊢ G.IsClique
      (↑(map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ : { x : α // x ∈ F } ↪ α } s) : Set α) ∧
    #(map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ : { x : α // x ∈ F } ↪ α } s) = n

Tactic:
simp only [coe_map, card_map]

Premises used: Finset.card_map, Finset.coe_map