awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
y : Fin n
hy : (φ : (a : Fin n) → α) y = s
e : x = y
pos :
  ∀ (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) x)).CliqueFree n) (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
pos₁ :
  ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) y)).CliqueFree n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
pos₂ :
  ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬(G.replaceVertex s s).CliqueFree n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have pos₃ : ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬G.CliqueFree n) (hy : (φ : (a : Fin n) → α) y = s) (e : x = y),
  IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff_top_isContained] at h
Cleared hypotheses: h, hx, y, hy, e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
y : Fin n
hy : (φ : (a : Fin n) → α) y = s
e : x = y
pos :
  ∀ (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) x)).CliqueFree n) (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
pos₁ :
  ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) y)).CliqueFree n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
pos₂ :
  ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬(G.replaceVertex s s).CliqueFree n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
pos₃ :
  ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬G.CliqueFree n) (hy : (φ : (a : Fin n) → α) y = s) (e : x = y),
    IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have pos₄ : ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : IsContained (α := Fin n) (completeGraph (Fin n)) G)
  (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff_top_isContained] at h
Cleared hypotheses: h, hx, y, hy, e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    {
            Adj := fun (v w : α) ↦
              if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have neg : ∀ {a b : Fin n},
  G.Adj ((φ.setValue x s : (a : Fin n) → α) a) ((φ.setValue x s : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
Tactic: refine Embedding.isContained ⟨φ.setValue x s, fun {a b} ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    {
            Adj := fun (v w : α) ↦
              if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
⊢ G.Adj ((φ.setValue x s : (a : Fin n) → α) a) ((φ.setValue x s : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
have neg : G.Adj (if a = x then s else (φ : (a : Fin n) → α) a) (if b = x then s else (φ : (a : Fin n) → α) b) ↔
  Adj (completeGraph (Fin n)) a b
Tactic: simp only [Embedding.coeFn_mk, Embedding.setValue, not_exists.mp ms, ite_false]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    {
            Adj := fun (v w : α) ↦
              if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
⊢ G.Adj (if a = x then s else (φ : (a : Fin n) → α) a) (if b = x then s else (φ : (a : Fin n) → α) b) ↔
    Adj (completeGraph (Fin n)) a b
have neg : (if a = x then if b = x then G.Adj s s else G.Adj s ((φ : (a : Fin n) → α) b)
  else if b = x then G.Adj ((φ : (a : Fin n) → α) a) s else G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b)) ↔
  Adj (completeGraph (Fin n)) a b
Tactic: rw [apply_ite (G.Adj · _), apply_ite (G.Adj _ ·), apply_ite (G.Adj _ ·)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    {
            Adj := fun (v w : α) ↦
              if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
⊢ (if a = x then if b = x then G.Adj s s else G.Adj s ((φ : (a : Fin n) → α) b)
    else
      if b = x then G.Adj ((φ : (a : Fin n) → α) a) s else G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b)) ↔
    Adj (completeGraph (Fin n)) a b
have h₁ : a = x ↔ (φ : (a : Fin n) → α) a = t
Tactic: convert! @hφ a b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    {
            Adj := fun (v w : α) ↦
              if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
h₁ : a = x ↔ (φ : (a : Fin n) → α) a = t
⊢ (if a = x then if b = x then G.Adj s s else G.Adj s ((φ : (a : Fin n) → α) b)
    else
      if b = x then G.Adj ((φ : (a : Fin n) → α) a) s else G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b)) ↔
    Adj (completeGraph (Fin n)) a b
have h₂ : (φ : (a : Fin n) → α) a = t → (b = x ↔ (φ : (a : Fin n) → α) b = t)
Tactic: convert! @hφ a b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    {
            Adj := fun (v w : α) ↦
              if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
h₁ : a = x ↔ (φ : (a : Fin n) → α) a = t
h₂ : (φ : (a : Fin n) → α) a = t → (b = x ↔ (φ : (a : Fin n) → α) b = t)
⊢ (if a = x then if b = x then G.Adj s s else G.Adj s ((φ : (a : Fin n) → α) b)
    else
      if b = x then G.Adj ((φ : (a : Fin n) → α) a) s else G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b)) ↔
    Adj (completeGraph (Fin n)) a b
have h₃ : (φ : (a : Fin n) → α) a = t → (φ : (a : Fin n) → α) b = t → (G.Adj s s ↔ False)
Tactic: convert! @hφ a b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    {
            Adj := fun (v w : α) ↦
              if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ : SimpleGraph α }.Adj
        ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔
      Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
a b : Fin n
h₁ : a = x ↔ (φ : (a : Fin n) → α) a = t
h₂ : (φ : (a : Fin n) → α) a = t → (b = x ↔ (φ : (a : Fin n) → α) b = t)
h₃ : (φ : (a : Fin n) → α) a = t → (φ : (a : Fin n) → α) b = t → (G.Adj s s ↔ False)
⊢ (if a = x then if b = x then G.Adj s s else G.Adj s ((φ : (a : Fin n) → α) b)
    else
      if b = x then G.Adj ((φ : (a : Fin n) → α) a) s else G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b)) ↔
    Adj (completeGraph (Fin n)) a b
have h₄ : ¬(φ : (a : Fin n) → α) a = t → (b = x ↔ (φ : (a : Fin n) → α) b = t)
Tactic: convert! @hφ a b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : t ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have neg : ∀ {a b : Fin n}, G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
Tactic: refine Embedding.isContained ⟨φ, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : t ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)
⊢ ∀ {a b : Fin n}, G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
have mt₁ : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
Tactic: simp_rw [Set.mem_range, not_exists, ← ne_eq] at mt
Cleared hypotheses: mt
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
| ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
have enter : ∀ {a b : Fin n},
  (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
Tactic: enter [a, b]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
a b : Fin n
| (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
have rw : G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
Tactic: rw [G.adj_replaceVertex_iff_of_ne _ (mt a) (mt b)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : 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 : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : ∀ (x : Fin n), (φ : (a : Fin n) → α) x ≠ t
| ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
have enter : ∀ {a b : Fin n}, G.Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
Tactic: enter [a, b]; rw [G.adj_replaceVertex_iff_of_ne _ (mt a) (mt b)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 ↔ G = ⊥
have mp : G.CliqueFree 2 → G = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
mp : G.CliqueFree 2 → G = ⊥
⊢ G.CliqueFree 2 ↔ G = ⊥
have mpr : G = ⊥ → G.CliqueFree 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → G = ⊥
have mp : G.CliqueFree 2 → ∀ (x y : α), ¬G.Adj x y
Tactic: simp_rw [← edgeSet_eq_empty, Set.eq_empty_iff_forall_notMem, Sym2.forall, mem_edgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 ↔ G = ⊥
have mp : G.CliqueFree 2 → G = ⊥
Tactic: classical
  constructor
  · simp_rw [← edgeSet_eq_empty, Set.eq_empty_iff_forall_notMem, Sym2.forall, mem_edgeSet]
    exact fun h a b hab => h _ ⟨by simpa [hab.ne], card_pair hab.ne⟩
  · rintro rfl
    exact cliqueFree_bot le_rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
mp : G.CliqueFree 2 → G = ⊥
⊢ G.CliqueFree 2 ↔ G = ⊥
have mpr : G = ⊥ → G.CliqueFree 2
Tactic: classical
  constructor
  · simp_rw [← edgeSet_eq_empty, Set.eq_empty_iff_forall_notMem, Sym2.forall, mem_edgeSet]
    exact fun h a b hab => h _ ⟨by simpa [hab.ne], card_pair hab.ne⟩
  · rintro rfl
    exact cliqueFree_bot le_rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
x y : α
t : Finset α
n : ℕ
h : G.CliqueFree n
hc : (G ⊔ edge x y).IsNClique n t
⊢ x ∈ t
have by_contra : ∀ (hf : x ∉ t), False
Tactic: by_contra hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
x y : α
t : Finset α
n : ℕ
h : G.CliqueFree n
hc : (G ⊔ edge x y).IsNClique n t
hf : x ∉ t
⊢ False
have ht : (↑t : Set α) \ {x} = (↑t : Set α)
Tactic: have ht : (t : Set α) \ {x} = t := sdiff_eq_left.mpr <| Set.disjoint_singleton_right.mpr hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
hc : G.IsNClique n s
h : G.CliqueFree (n + 1)
x : α
⊢ ∃ y ∈ s, ¬G.Adj x y
have by_contra! : ∀ (hf : ∀ (y : α) (_ : y ∈ s), G.Adj x y), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
hc : G.IsNClique n s
h : G.CliqueFree (n + 1)
x : α
⊢ ∃ y ∈ s, ¬G.Adj x y
have by_contra! : (¬∃ y ∈ s, ¬G.Adj x y) → False
Tactic: classical
  by_contra! hf
  exact (hc.insert hf).not_cliqueFree h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
hc : G.IsNClique n s
h : G.CliqueFree (n + 1)
x : α
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∃ y ∈ s, ¬G.Adj x y) → False
⊢ ∃ y ∈ s, ¬G.Adj x y
have by_contra!₄ : (∀ (y : α) (_ : y ∈ s), G.Adj x y) → False
Tactic: classical
  by_contra! hf
  exact (hc.insert hf).not_cliqueFree h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
⊢ ∃ (s : Finset α), x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)
have obtain : ∀ (t : Finset α) (hc : (G ⊔ edge x y).IsNClique (n + 1) t),
  ∃ (s : Finset α), x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)
Tactic: obtain ⟨t, hc⟩ := not_forall_not.1 <| h.not_prop_of_gt <| G.lt_sup_edge _ _ hne hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
⊢ ∃ (s : Finset α), x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)
have right : G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (insert y ((t.erase x).erase y))
Tactic: use (t.erase x).erase y, erase_right_comm (a := x) ▸ (notMem_erase _ _), notMem_erase _ _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
⊢ G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (insert y ((t.erase x).erase y))
have h1 : x ∈ t
Tactic: have h1 := h.1.mem_of_sup_edge_isNClique hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
⊢ G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (insert y ((t.erase x).erase y))
have h2 : y ∈ t
Tactic: have h2 := h.1.mem_of_sup_edge_isNClique (edge_comm .. ▸ hc)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
⊢ G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (insert y ((t.erase x).erase y))
have right : G.IsNClique n (t.erase y) ∧ G.IsNClique n (t.erase x)
Tactic: rw [insert_erase <| mem_erase_of_ne_of_mem hne.symm h2, erase_right_comm,
      insert_erase <| mem_erase_of_ne_of_mem hne h1]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
t : Finset α
hts : (↑t : Set α) ⊆ s
ht : G.IsNClique n t
⊢ False
have obtain : ∀ (u : Finset α) (hut : u ⊆ t) (hu : #u = m), False
Tactic: obtain ⟨u, hut, hu⟩ := exists_subset_card_eq (hmn.trans ht.card_eq.ge)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
⊢ G.CliqueFreeOn {a} n ↔ 1 < n
have zero : G.CliqueFreeOn {a} 0 ↔ LT.lt (α := ℕ) 1 0
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
zero : G.CliqueFreeOn {a} 0 ↔ LT.lt (α := ℕ) 1 0
⊢ G.CliqueFreeOn {a} n ↔ 1 < n
have succ : G.CliqueFreeOn {a} (HAdd.hAdd (α := ℕ) 0 1) ↔ 1 < HAdd.hAdd (α := ℕ) 0 1
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
zero : G.CliqueFreeOn {a} 0 ↔ LT.lt (α := ℕ) 1 0
succ : G.CliqueFreeOn {a} (HAdd.hAdd (α := ℕ) 0 1) ↔ 1 < HAdd.hAdd (α := ℕ) 0 1
⊢ G.CliqueFreeOn {a} n ↔ 1 < n
have succ₁ : ∀ (n : ℕ), G.CliqueFreeOn {a} (n + 1 + 1) ↔ 1 < n + 1 + 1
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ
have refine_1 : ∀ (h : G.CliqueFreeOn s 2) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s), a ≠ b → ∀ (hab : G.Adj a b), (↑{a, b} : Set α) ⊆ s
Tactic: refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
refine_1 :
  ∀ (h : G.CliqueFreeOn s 2) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s),
    a ≠ b → ∀ (hab : G.Adj a b), (↑{a, b} : Set α) ⊆ s
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ
have refine_2 : s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2
Tactic: refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h_1 : a ≠ b
hab : G.Adj a b
⊢ (↑{a, b} : Set α) ⊆ s
have refine_1 : {a, b} ⊆ s
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2
have refine_2 : s.Pairwise G.Adjᶜ →
  ∀ ⦃t : Finset α⦄, (↑t : Set α) ⊆ s → G.IsClique (↑t : Set α) → ∀ (x x_1 : α), x ≠ x_1 → ¬t = {x, x_1}
Tactic: simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
hst : (↑{a, b} : Set α) ⊆ s
ht : G.IsClique (↑{a, b} : Set α)
⊢ False
have hst₁ : a ∈ s ∧ b ∈ s
Tactic: simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique (↑{a, b} : Set α)
hst : a ∈ s ∧ b ∈ s
⊢ False
have refine_2 : a ∈ (↑{a, b} : Set α)
Tactic: refine h hst.1 hst.2 hab (ht ?_ ?_ hab)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique (↑{a, b} : Set α)
hst : a ∈ s ∧ b ∈ s
refine_2 : a ∈ (↑{a, b} : Set α)
⊢ False
have refine_2₁ : b ∈ (↑{a, b} : Set α)
Tactic: refine h hst.1 hst.2 hab (ht ?_ ?_ hab)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ
have refine_1 : ∀ (h : G.CliqueFreeOn s 2) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s), a ≠ b → ∀ (hab : G.Adj a b), (↑{a, b} : Set α) ⊆ s
Tactic: classical
  refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
  · push_cast
    exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩
  simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]
  rintro h t hst ht a b hab rfl
  simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst
  refine h hst.1 hst.2 hab (ht ?_ ?_ hab) <;> simp