awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Fintype β
inst_4 : DecidableEq β
e : α ≃ β
n : ℕ
push_cast :
  Eq.{u_2 + 1} (α := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) n)
    ((⇑{ toFun := map e.toEmbedding, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) } :
        (a : Finset α) → Finset β) ''
      G.cliqueSet n)
⊢ (↑(cliqueFinset (SimpleGraph.map (⇑e : (a : α) → β) G) n) : Set (Finset β)) =
    (↑(map { toFun := map e.toEmbedding, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Fintype β
inst_4 : DecidableEq β
e : α ≃ β
n : ℕ
⊢ Eq.{u_2 + 1} (α := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) n)
    ((⇑{ toFun := map e.toEmbedding, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) } :
        (a : Finset α) → Finset β) ''
      G.cliqueSet n)

Tactic:
cliqueSet_map_of_equiv _ _ _

Premises used: SimpleGraph.cliqueSet_map_of_equiv, Finset.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
inst_3 : Fintype β
inst_4 : DecidableEq β
e : α ≃ β
n : ℕ
⊢ Eq.{u_2 + 1} (α := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) n)
    ((⇑{ toFun := map e.toEmbedding, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) } :
        (a : Finset α) → Finset β) ''
      G.cliqueSet n)

Tactic:
exact cliqueSet_map_of_equiv _ _ _

Premises used: SimpleGraph.cliqueSet_map_of_equiv
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.IsIndepSet s ↔ s.Pairwise fun (v w : α) ↦ ¬G.Adj v w

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.IsIndepSet s ↔ IsAntichain G.Adj s

Tactic:
.rfl

Premises used: Iff.rfl, IsAntichain
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬G.Adj x y

Tactic:
simp_all [compl_adj]

Premises used: SimpleGraph.compl_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → G.Adj x y

Tactic:
simp_all [compl_adj]

Premises used: SimpleGraph.compl_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
he : e ∈ G.edgeSet
mk :
  ∀ (v w : α) (he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet),
    Set.Nonempty.{u_1} (α := α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)}
⊢ Set.Nonempty.{u_1} (α := α) {b : α | b ∈ sᶜ ∧ b ∈ e}

Tactic:
obtain ⟨v, w⟩ := e
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
mk : ∀ (c : Eq.{u_1 + 1} (α := Set α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} ∅), False
⊢ Set.Nonempty.{u_1} (α := α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)}

Tactic:
by_contra! c
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : Eq.{u_1 + 1} (α := Set α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} ∅
⊢ False

Tactic:
indA ?_ ?_ he.ne he

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : Eq.{u_1 + 1} (α := Set α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} ∅
mk : (v, w).1 ∈ s
mk₁ : (v, w).2 ∈ s
⊢ False

Tactic:
refine indA ?_ ?_ he.ne he

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : Eq.{u_1 + 1} (α := Set α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} ∅
⊢ (v, w).1 ∈ s

Tactic:
Set.not_notMem.mp <| not_and'.mp (c ▸ Set.notMem_empty v) <| Sym2.mem_mk_left ..

Premises used: Sym2.mem_mk_left, Set.not_notMem, Iff.mp, not_and'
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : Eq.{u_1 + 1} (α := Set α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} ∅
⊢ (v, w).1 ∈ s

Tactic:
exact Set.not_notMem.mp <| not_and'.mp (c ▸ Set.notMem_empty v) <| Sym2.mem_mk_left ..

Premises used: Sym2.mem_mk_left, Set.not_notMem, Iff.mp, not_and'
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : Eq.{u_1 + 1} (α := Set α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} ∅
⊢ (v, w).2 ∈ s

Tactic:
Set.not_notMem.mp <| not_and'.mp (c ▸ Set.notMem_empty w) <| Sym2.mem_mk_right ..

Premises used: Sym2.mem_mk_right, Set.not_notMem, Iff.mp, not_and'
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
indA : G.IsIndepSet s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : Eq.{u_1 + 1} (α := Set α) {b : α | b ∈ sᶜ ∧ b ∈ Quot.mk (Sym2.Rel α) (v, w)} ∅
⊢ (v, w).2 ∈ s

Tactic:
exact Set.not_notMem.mp <| not_and'.mp (c ▸ Set.notMem_empty w) <| Sym2.mem_mk_right ..

Premises used: Sym2.mem_mk_right, Set.not_notMem, Iff.mp, not_and'
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
by_contra : ∀ (nind : ¬G.IsIndepSet (G.neighborSet v)), False
⊢ G.IsIndepSet (G.neighborSet v)

Tactic:
by_contra nind
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ¬G.IsIndepSet (G.neighborSet v)
⊢ ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y

Tactic:
rw [IsIndepSet, Set.Pairwise] at nind

Premises used: SimpleGraph.IsIndepSet, Set.Pairwise
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y
⊢ ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y

Tactic:
push Not at nind

Premises used: Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y
⊢ ∃ (x : α), G.Adj v x ∧ ∃ (y : α), G.Adj v y ∧ x ≠ y ∧ G.Adj x y

Tactic:
simp_rw [mem_neighborSet] at nind

Premises used: SimpleGraph.mem_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ∃ (x : α), G.Adj v x ∧ ∃ (y : α), G.Adj v y ∧ x ≠ y ∧ G.Adj x y
obtain : ∀ (j : α) (avj : G.Adj v j) (k : α) (avk : G.Adj v k), j ≠ k → ∀ (ajk : G.Adj j k), False
⊢ False

Tactic:
obtain ⟨j, avj, k, avk, _, ajk⟩ := nind
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v j : α
avj : G.Adj v j
k : α
avk : G.Adj v k
left : j ≠ k
ajk : G.Adj j k
⊢ G.Adj v j ∧ G.Adj v k ∧ G.Adj j k

Tactic:
simp [avj, avk, ajk]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v j : α
avj : G.Adj v j
k : α
avk : G.Adj v k
left : j ≠ k
ajk : G.Adj j k
⊢ False

Tactic:
exact h {v, j, k} (is3Clique_triple_iff.mpr (by simp [avj, avk, ajk]))

Premises used: Iff.mpr, Insert.insert, SimpleGraph.is3Clique_triple_iff, Singleton.singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
by_contra by_contra₁ by_contra₂ : ∀ (nind : ¬G.IsIndepSet (G.neighborSet v)), False
by_contra₃ : ∀ (nind : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y), False
by_contra₄ : ∀ (nind : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y), False
by_contra₅ : ∀ (nind : ∃ (x : α), G.Adj v x ∧ ∃ (y : α), G.Adj v y ∧ x ≠ y ∧ G.Adj x y), False
by_contra₆ : ∀ (j : α) (avj : G.Adj v j) (k : α) (avk : G.Adj v k), j ≠ k → ∀ (ajk : G.Adj j k), False
⊢ G.IsIndepSet (G.neighborSet v)

Tactic:
classical
  by_contra nind
  rw [IsIndepSet, Set.Pairwise] at nind
  push Not at nind
  simp_rw [mem_neighborSet] at nind
  obtain ⟨j, avj, k, avk, _, ajk⟩ := nind
  exact h {v, j, k} (is3Clique_triple_iff.mpr (by simp [avj, avk, ajk]))

Premises used: SimpleGraph.IsIndepSet, SimpleGraph.mem_neighborSet, Set.Pairwise, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
F : Set α
s : Set (↑F : Type u_1)
⊢ IsIndepSet (Subgraph.coe (Subgraph.induce ⊤ F)) s ↔ G.IsIndepSet (Subtype.val (p := fun (x : α) ↦ x ∈ F) '' s)

Tactic:
simp [Set.Pairwise]

Premises used: Set.Pairwise
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
rw : Gᶜ.IsNClique n s ↔ G.IsIndepSet (↑s : Set α) ∧ #s = n
⊢ Gᶜ.IsNClique n s ↔ G.IsNIndepSet n s

Tactic:
rw [isNIndepSet_iff]

Premises used: SimpleGraph.isNIndepSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNClique n s ↔ G.IsIndepSet (↑s : Set α) ∧ #s = n

Tactic:
simp [isNClique_iff]

Premises used: SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
rw : Gᶜ.IsNIndepSet n s ↔ G.IsClique (↑s : Set α) ∧ #s = n
⊢ Gᶜ.IsNIndepSet n s ↔ G.IsNClique n s

Tactic:
rw [isNClique_iff]

Premises used: SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNIndepSet n s ↔ G.IsClique (↑s : Set α) ∧ #s = n

Tactic:
simp [isNIndepSet_iff]

Premises used: SimpleGraph.isNIndepSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
F : Set α
s : Finset { x : α // x ∈ F }
n : ℕ
⊢ IsNIndepSet (Subgraph.coe (Subgraph.induce ⊤ F)) n s ↔
    G.IsNIndepSet n (map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ } s)

Tactic:
simp [isNIndepSet_iff, (isIndepSet_induce)]

Premises used: SimpleGraph.isNIndepSet_iff, SimpleGraph.isIndepSet_induce
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ Gᶜ.CliqueFree n ↔ G.IndepSetFree n

Tactic:
simp [IndepSetFree, CliqueFree]

Premises used: SimpleGraph.IndepSetFree, SimpleGraph.CliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ Gᶜ.IndepSetFree n ↔ G.CliqueFree n

Tactic:
simp [IndepSetFree, CliqueFree]

Premises used: SimpleGraph.IndepSetFree, SimpleGraph.CliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ s ∈ G.indepSetSet n ↔ G.IsNIndepSet n s

Tactic:
Iff.rfl

Premises used: SimpleGraph.indepSetSet, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
⊢ Gᶜ.cliqueNum = G.indepNum

Tactic:
simp [indepNum, cliqueNum]

Premises used: SimpleGraph.indepNum, SimpleGraph.cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
⊢ Gᶜ.indepNum = G.cliqueNum

Tactic:
simp [indepNum, cliqueNum]

Premises used: SimpleGraph.indepNum, SimpleGraph.cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tc : G.IsIndepSet (↑t : Set α)
⊢ Gᶜ.IsClique (↑t : Set α)

Tactic:
rw [← isClique_compl] at tc

Premises used: SimpleGraph.isClique_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tc : Gᶜ.IsClique (↑t : Set α)
simp_rw : #t ≤ sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}
⊢ #t ≤ G.indepNum

Tactic:
simp_rw [indepNum, ← isNClique_compl]

Premises used: SimpleGraph.isNClique_compl, SimpleGraph.indepNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tc : Gᶜ.IsClique (↑t : Set α)
⊢ #t ≤ sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}

Tactic:
tc.card_le_cliqueNum

Premises used: SimpleGraph.cliqueNum, SimpleGraph.IsClique.card_le_cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tc : Gᶜ.IsClique (↑t : Set α)
⊢ #t ≤ sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}

Tactic:
exact tc.card_le_cliqueNum

Premises used: SimpleGraph.IsClique.card_le_cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
simp_rw : ∃ (s : Finset α), Gᶜ.IsNClique (sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}) s
⊢ ∃ (s : Finset α), G.IsNIndepSet G.indepNum s

Tactic:
simp_rw [indepNum, ← isNClique_compl]

Premises used: SimpleGraph.isNClique_compl, SimpleGraph.indepNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
⊢ ∃ (s : Finset α), Gᶜ.IsNClique (sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}) s

Tactic:
exists_isNClique_cliqueNum

Premises used: SimpleGraph.exists_isNClique_cliqueNum, SimpleGraph.cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
⊢ ∃ (s : Finset α), Gᶜ.IsNClique (sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}) s

Tactic:
exact exists_isNClique_cliqueNum

Premises used: SimpleGraph.exists_isNClique_cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
⊢ Gᶜ.IsMaximumClique s ↔ G.IsMaximumIndepSet s

Tactic:
simp [isMaximumIndepSet_iff, isMaximumClique_iff]

Premises used: SimpleGraph.isMaximumClique_iff, SimpleGraph.isMaximumIndepSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
⊢ Gᶜ.IsMaximumIndepSet s ↔ G.IsMaximumClique s

Tactic:
simp [isMaximumIndepSet_iff, isMaximumClique_iff]

Premises used: SimpleGraph.isMaximumClique_iff, SimpleGraph.isMaximumIndepSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
s : Set α
⊢ Maximal G.IsIndepSet s ↔ G.IsIndepSet s ∧ ∀ (t : Set α), G.IsIndepSet t → s ⊆ t → t ⊆ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Maximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
s : Finset α
⊢ Maximal Gᶜ.IsClique (↑s : Set α) ↔ Maximal G.IsIndepSet (↑s : Set α)

Tactic:
simp [isMaximalIndepSet_iff, isMaximalClique_iff]

Premises used: SimpleGraph.isMaximalClique_iff, SimpleGraph.isMaximalIndepSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
s : Finset α
⊢ Maximal Gᶜ.IsIndepSet (↑s : Set α) ↔ Maximal G.IsClique (↑s : Set α)

Tactic:
simp [isMaximalIndepSet_iff, isMaximalClique_iff]

Premises used: SimpleGraph.isMaximalClique_iff, SimpleGraph.isMaximalIndepSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumIndepSet s
rw : Maximal Gᶜ.IsClique (↑s : Set α)
⊢ Maximal G.IsIndepSet (↑s : Set α)

Tactic:
rw [← isMaximalClique_compl]

Premises used: SimpleGraph.isMaximalClique_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumIndepSet s
⊢ Gᶜ.IsMaximumClique s

Tactic:
rw [← isMaximumClique_compl] at M

Premises used: SimpleGraph.isMaximumClique_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : Gᶜ.IsMaximumClique s
⊢ Maximal Gᶜ.IsClique (↑s : Set α)

Tactic:
IsMaximumClique.isMaximalClique s M

Premises used: SimpleGraph.IsMaximumClique.isMaximalClique
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : Gᶜ.IsMaximumClique s
⊢ Maximal Gᶜ.IsClique (↑s : Set α)

Tactic:
exact IsMaximumClique.isMaximalClique s M

Premises used: SimpleGraph.IsMaximumClique.isMaximalClique
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tmc : G.IsMaximumIndepSet t
⊢ Gᶜ.IsMaximumClique t

Tactic:
rw [← isMaximumClique_compl] at tmc

Premises used: SimpleGraph.isMaximumClique_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
simp_rw : #t = sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}
⊢ #t = G.indepNum

Tactic:
simp_rw [indepNum, ← isNClique_compl]

Premises used: SimpleGraph.isNClique_compl, SimpleGraph.indepNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}

Tactic:
Gᶜ.maximumClique_card_eq_cliqueNum t tmc

Premises used: SimpleGraph.maximumClique_card_eq_cliqueNum, SimpleGraph.cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tmc : Gᶜ.IsMaximumClique t
⊢ #t = sSup {n : ℕ | ∃ (s : Finset α), Gᶜ.IsNClique n s}

Tactic:
exact Gᶜ.maximumClique_card_eq_cliqueNum t tmc

Premises used: SimpleGraph.maximumClique_card_eq_cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
⊢ ∃ (s : Finset α), G.IsMaximumIndepSet s

Tactic:
simp [← isMaximumClique_compl, maximumClique_exists]

Premises used: SimpleGraph.maximumClique_exists, SimpleGraph.isMaximumClique_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
s : Finset α
⊢ s ∈ G.indepSetFinset n ↔ G.IsNIndepSet n s

Tactic:
mem_filter.trans <| and_iff_right <| mem_univ _

Premises used: Finset.mem_univ, Set.Mem, setOf, and_iff_right, Iff.trans, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
u v : Fin n
rw :
  (↑u : ℕ) + 1 = (↑v : ℕ) ∨ (↑v : ℕ) + 1 = (↑u : ℕ) →
    Ne (α := Bool) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) u) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) v)
⊢ (pathGraph n).Adj u v →
    Ne (α := Bool) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) u) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) v)

Tactic:
rw [pathGraph_adj]

Premises used: SimpleGraph.pathGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
u v : Fin n
h : (↑u : ℕ) + 1 = (↑v : ℕ)
⊢ Ne (α := Bool) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) u) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) v)

Tactic:
simp [← h, not_iff, Nat.succ_mod_two_eq_zero_iff]

Premises used: Nat.succ_mod_two_eq_zero_iff, not_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
u v : Fin n
h : (↑v : ℕ) + 1 = (↑u : ℕ)
⊢ Ne (α := Bool) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) u) ((fun (u : Fin n) ↦ decide ((↑u : ℕ) % 2 = 0)) v)

Tactic:
simp [← h, not_iff, Nat.succ_mod_two_eq_zero_iff]

Premises used: Nat.succ_mod_two_eq_zero_iff, not_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
v w : Fin 2
rw : (↑v : ℕ) = (↑w : ℕ) → v = w
⊢ Eq (α := Fin n) ((fun (v : Fin 2) ↦ (⟨(↑v : ℕ), ⋯⟩ : Fin n)) v) ((fun (v : Fin 2) ↦ (⟨(↑v : ℕ), ⋯⟩ : Fin n)) w) →
    v = w

Tactic:
rw [Fin.mk.injEq]

Premises used: Fin.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
v w : Fin 2
⊢ (↑v : ℕ) = (↑w : ℕ) → v = w

Tactic:
Fin.ext

Premises used: Fin.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
v w : Fin 2
⊢ (↑v : ℕ) = (↑w : ℕ) → v = w

Tactic:
exact Fin.ext

Premises used: Fin.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
⊢ ∀ {a b : Fin 2},
    (pathGraph n).Adj
        (({ toFun := fun (v : Fin 2) ↦ (⟨(↑v : ℕ), ⋯⟩ : Fin n), inj' := ⋯ : Fin 2 ↪ Fin n } : (a : Fin 2) → Fin n) a)
        (({ toFun := fun (v : Fin 2) ↦ (⟨(↑v : ℕ), ⋯⟩ : Fin n), inj' := ⋯ : Fin 2 ↪ Fin n } : (a : Fin 2) → Fin n) b) ↔
      Adj (pathGraph 2) a b

Tactic:
simp [pathGraph]

Premises used: SimpleGraph.pathGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
⊢ (pathGraph n).Colorable (Fintype.card Bool)

Tactic:
have hc := (pathGraph.bicoloring n).colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
a : (pathGraph n).chromaticNumber ≤ 2
a₁ : 2 ≤ (pathGraph n).chromaticNumber
⊢ (pathGraph n).chromaticNumber = 2

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).chromaticNumber ≤ 2

Tactic:
hc.chromaticNumber_le

Premises used: Fintype.card, SimpleGraph.Colorable.chromaticNumber_le, Finset.card, Multiset.card
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).chromaticNumber ≤ 2

Tactic:
exact hc.chromaticNumber_le

Premises used: SimpleGraph.Colorable.chromaticNumber_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩

Tactic:
simp [pathGraph_adj]

Premises used: SimpleGraph.pathGraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
⊢ (pathGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩

Tactic:
have hadj : (pathGraph n).Adj ⟨0, Nat.zero_lt_of_lt h⟩ ⟨1, h⟩ := by simp [pathGraph_adj]
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
hadj : (pathGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩
⊢ 2 ≤ (pathGraph n).chromaticNumber

Tactic:
two_le_chromaticNumber_of_adj hadj

Premises used: SimpleGraph.two_le_chromaticNumber_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
n : ℕ
h : 2 ≤ n
hc : (pathGraph n).Colorable (Fintype.card Bool)
hadj : (pathGraph n).Adj ⟨0, ⋯⟩ ⟨1, h⟩
⊢ 2 ≤ (pathGraph n).chromaticNumber

Tactic:
exact two_le_chromaticNumber_of_adj hadj

Premises used: SimpleGraph.two_le_chromaticNumber_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v u_1 : α
⊢ Even (Walk.length.{u_1} (V := α) (G := G) (u := u_1) Walk.nil) ↔
    ((c : (a : α) → Bool) u_1 = true ↔ (c : (a : α) → Bool) u_1 = true)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
Goal:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u_1 v_1 u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ ((c : (a : α) → Bool) v = true ↔ (c : (a : α) → Bool) w = true)
cons : ¬Even p.length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)
⊢ Even (Walk.cons h p).length ↔ ((c : (a : α) → Bool) u = true ↔ (c : (a : α) → Bool) w = true)

Tactic:
simp only [Walk.length_cons, Nat.even_add_one]

Premises used: Nat.even_add_one, SimpleGraph.Walk.length_cons