awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
⊢ #(s.erase a) = n - 1
have rw : #s - 1 = n - 1
Tactic: rw [card_erase_of_mem ha, hs.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
rw : #s - 1 = n - 1
⊢ #(s.erase a) = n - 1
have rw₁ : n - 1 = n - 1
Tactic: rw [card_erase_of_mem ha, hs.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ G.IsNClique n (insert a (s.erase b))
have zero : ∀ (hs : G.IsNClique 0 s), G.IsNClique 0 (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
Cleared hypotheses: n, hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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))
⊢ G.IsNClique n (insert a (s.erase b))
have succ : ∀ (n : ℕ) (hs : G.IsNClique (n + 1) s), G.IsNClique (n + 1) (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
Cleared hypotheses: n, hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : 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
have 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
Tactic: simp only [isNClique_iff, Set.pairwise_insert_of_symmetric G.symm, coe_insert]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
⊢ (((↑{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
have 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
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ (((↑{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
have 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
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
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
have 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
Tactic: by_cases hbc : b = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ (((↑{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
have 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
Tactic: by_cases hbc : b = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
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
have 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
Tactic: by_cases hbc : b = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ (((↑{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
have 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
Tactic: by_cases hbc : b = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : a = b
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
have 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
Tactic: by_cases hac : a = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ (((↑{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
have 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
Tactic: by_cases hac : a = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : a = b
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
have 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
Tactic: by_cases hac : a = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ (((↑{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
have 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
Tactic: by_cases hac : a = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : ¬a = b
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
have 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
Tactic: by_cases hac : a = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ (((↑{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
have 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
Tactic: by_cases hac : a = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a b c : α
inst : DecidableEq α
hab : ¬a = b
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
have 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
Tactic: by_cases hac : a = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ (((↑{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
have 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
Tactic: by_cases hac : a = c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
have 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
Tactic: subst_vars
Cleared hypotheses: a, b, hab, hbc, hac
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
have 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
Tactic: subst_vars
Cleared hypotheses: a, b, hab, hbc, hac
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
have 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
Tactic: subst_vars
Cleared hypotheses: a, b, hab, hbc, hac
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
have 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
Tactic: subst_vars
Cleared hypotheses: a, hab, hac
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
have 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
Tactic: subst_vars
Cleared hypotheses: a, b, hab, hbc, hac
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
have 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
Tactic: subst_vars
Cleared hypotheses: b, hab, hbc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
have 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
Tactic: subst_vars
Cleared hypotheses: a, hab, hac
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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}
have 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}
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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}
⊢ G.IsNClique 3 s ↔ ∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
have 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
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
inst : DecidableEq α
h : G.IsNClique 3 s
⊢ ∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
have 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}
Tactic: obtain ⟨a, b, c, -, -, -, hs⟩ := card_eq_three.1 h.card_eq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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}
have refine_1 : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
Tactic: refine ⟨a, b, c, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
inst : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
have refine_1 : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, c} {a, b, c}
Tactic: rwa [hs, eq_self_iff_true, and_true, is3Clique_triple_iff.symm, ← hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
have refine_1₁ : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ True
Tactic: rwa [hs, eq_self_iff_true, and_true, is3Clique_triple_iff.symm, ← hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
have refine_1₂ : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
Tactic: rwa [hs, eq_self_iff_true, and_true, is3Clique_triple_iff.symm, ← hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
have refine_1₃ : G.IsNClique 3 {a, b, c}
Tactic: rwa [hs, eq_self_iff_true, and_true, is3Clique_triple_iff.symm, ← hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ (∃ (s : Finset α), G.IsNClique 3 s) ↔ ∃ (u : α) (w : G.Walk u u), w.IsCycle ∧ w.length = 3
have 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
Tactic: simp_rw [is3Clique_iff, isCycle_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ (∃ (s : Finset α), G.IsNClique 3 s) ↔ ∃ (u : α) (w : G.Walk u u), w.IsCycle ∧ w.length = 3
have 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
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⟩)⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ (∃ (s : Finset α), G.IsNClique 3 s) ↔ ∃ (u : α) (w : G.Walk u u), w.IsCycle ∧ w.length = 3
have 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
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⟩)⟩