awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ G.IsClique
      ((⇑{ toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ } : (a : { x : α // x ∈ F }) → α) ''
        (↑s : Set { x : α // x ∈ F })) ∧
    #s = n

Tactic:
⟨cc.left.of_induce, cc.right⟩

Premises used: And.right, And.left, And.intro, SimpleGraph.IsClique.of_induce
-- 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
⊢ G.IsClique
      ((⇑{ toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ } : (a : { x : α // x ∈ F }) → α) ''
        (↑s : Set { x : α // x ∈ F })) ∧
    #s = n

Tactic:
exact ⟨cc.left.of_induce, cc.right⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
v w : α
s : Finset α
n : ℕ
hc : (G ⊔ edge v w).IsNClique n s
hx : v ∈ s
rw : #s - 1 = n - 1
rw₁ rw₂ : n - 1 = n - 1
⊢ #(s.erase v) = n - 1

Tactic:
rw [card_erase_of_mem hx, hc.2]

Premises used: SimpleGraph.IsNClique.card_eq, Finset.card_erase_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype β
f : Copy.{u_2, u_1} (α := β) ⊤ G
rw : G.IsClique (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f.toEmbedding : (a : β) → α)) ∧ Fintype.card β = Fintype.card β
⊢ G.IsNClique (Fintype.card β) (map f.toEmbedding univ)

Tactic:
rw [isNClique_iff, card_map, card_univ, coe_map, coe_univ, Set.image_univ]

Premises used: Finset.card_univ, Set.image_univ, Finset.coe_univ, Finset.card_map, SimpleGraph.isNClique_iff, Finset.coe_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype β
f : Copy.{u_2, u_1} (α := β) ⊤ G
⊢ G.IsClique (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f.toEmbedding : (a : β) → α)) ∧ Fintype.card β = Fintype.card β

Tactic:
⟨isClique_range_copy_top f, rfl⟩

Premises used: SimpleGraph.isClique_range_copy_top, And.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype β
f : Copy.{u_2, u_1} (α := β) ⊤ G
⊢ G.IsClique (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f.toEmbedding : (a : β) → α)) ∧ Fintype.card β = Fintype.card β

Tactic:
exact ⟨isClique_range_copy_top f, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
hG : G.IsNClique n s
⊢ ¬G.CliqueFree n

Tactic:
fun h ↦ h _ hG

Premises used: Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
h : IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ G.IsNClique (Fintype.card (Fin n)) (map (Nonempty.some h).toEmbedding univ)

Tactic:
have := isNClique_map_copy_top h.some
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
h : IsContained (α := Fin n) (completeGraph (Fin n)) G
this : G.IsNClique (Fintype.card (Fin n)) (map (Nonempty.some h).toEmbedding univ)
⊢ G.IsNClique n (map (Nonempty.some h).toEmbedding univ)

Tactic:
rw [Fintype.card_fin] at this

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
h : IsContained (α := Fin n) (completeGraph (Fin n)) G
this : G.IsNClique n (map (Nonempty.some h).toEmbedding univ)
⊢ ¬G.CliqueFree n

Tactic:
(· _ this)

Premises used: Finset.univ, Finset.map, Nonempty.some, SimpleGraph.Copy.toEmbedding, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
h : IsContained (α := Fin n) (completeGraph (Fin n)) G
this : G.IsNClique n (map (Nonempty.some h).toEmbedding univ)
⊢ ¬G.CliqueFree n

Tactic:
exact (· _ this)
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n_1 : ℕ
s : Finset α
n : ℕ
h : ¬∀ (t : Finset α), ¬G.IsNClique n t
⊢ ∃ (t : Finset α), G.IsNClique n t

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n_1 : ℕ
s : Finset α
n : ℕ
h : ∃ (t : Finset α), G.IsNClique n t
apply : Embedding (V := Fin n) (completeGraph (Fin n)) (induce (↑(h.choose (p := G.IsNClique n)) : Set α) G)
⊢ Embedding (V := Fin n) (completeGraph (Fin n)) G

Tactic:
apply Embedding.induce (h.choose : Set α) |>.comp

Premises used: SetLike.coe, Exists.choose, SimpleGraph.Embedding.induce, SimpleGraph.Embedding.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n_1 : ℕ
s : Finset α
n : ℕ
h : ∃ (t : Finset α), G.IsNClique n t
rw : Embedding (V := Fin n) (W := (↑(↑(h.choose (p := G.IsNClique n)) : Set α) : Type u_1)) (completeGraph (Fin n)) ⊤
⊢ Embedding (V := Fin n) (completeGraph (Fin n)) (induce (↑(h.choose (p := G.IsNClique n)) : Set α) G)

Tactic:
rw [G.isClique_iff_induce_eq.mp h.choose_spec.isClique]

Premises used: Exists.choose_spec, SimpleGraph.isClique_iff_induce_eq, SimpleGraph.IsNClique.isClique, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n_1 : ℕ
s : Finset α
n : ℕ
h : ∃ (t : Finset α), G.IsNClique n t
⊢ Embedding (V := Fin n) (W := (↑(↑(h.choose (p := G.IsNClique n)) : Set α) : Type u_1)) (completeGraph (Fin n)) ⊤

Tactic:
exact Embedding.completeGraph <| Finset.equivFinOfCardEq h.choose_spec.card_eq |>.symm.toEmbedding

Premises used: Exists.choose_spec, SimpleGraph.Embedding.completeGraph, SimpleGraph.IsNClique.card_eq, Equiv.toEmbedding, Finset.equivFinOfCardEq, Equiv.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ ¬G.CliqueFree n ↔ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
⟨(topEmbeddingOfNotCliqueFree · |>.isContained), IsContained.not_cliqueFree⟩

Premises used: SimpleGraph.topEmbeddingOfNotCliqueFree, SimpleGraph.IsContained.not_cliqueFree, SimpleGraph.Embedding.isContained, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
contrapose! : ¬G.CliqueFree n ↔ Nonempty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)
⊢ G.CliqueFree n ↔ IsEmpty.{max (u_1 + 1) 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)

Tactic:
contrapose!
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ ¬G.CliqueFree n ↔ Nonempty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)

Tactic:
not_cliqueFree_iff_top_isContained n

Premises used: SimpleGraph.not_cliqueFree_iff_top_isContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ ¬G.CliqueFree n ↔ Nonempty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)

Tactic:
exact not_cliqueFree_iff_top_isContained n

Premises used: SimpleGraph.not_cliqueFree_iff_top_isContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
β : Type u_3
inst : Fintype β
rw : ¬G.CliqueFree (Fintype.card β) ↔ ¬Free.{u_3, u_1} (α := β) ⊤ G
rw₁ : ¬G.CliqueFree (Fintype.card β) ↔ IsContained.{u_3, u_1} (α := β) ⊤ G
rw₂ :
  IsContained (α := Fin (Fintype.card β)) (completeGraph (Fin (Fintype.card β))) G ↔ IsContained.{u_3, u_1} (α := β) ⊤ G
rw₃ rw₄ :
  IsContained (α := Fin (Fintype.card β)) (completeGraph (Fin (Fintype.card β))) G ↔
    IsContained (α := Fin (Fintype.card β)) (completeGraph (Fin (Fintype.card β))) G
⊢ G.CliqueFree (Fintype.card β) ↔ Free.{u_3, u_1} (α := β) ⊤ G

Tactic:
rw [← not_iff_not, not_free, not_cliqueFree_iff_top_isContained,
    isContained_congr (Iso.completeGraph (equivFin β)) Iso.refl]

Premises used: not_iff_not, SimpleGraph.Iso.completeGraph, SimpleGraph.Iso.refl, SimpleGraph.not_free, Fintype.equivFin, SimpleGraph.not_cliqueFree_iff_top_isContained, SimpleGraph.isContained_congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
f : completeGraph α ⊑ G
rw : IsContained (α := Fin (Fintype.card α)) (completeGraph (Fin (Fintype.card α))) G
⊢ ¬G.CliqueFree (Fintype.card α)

Tactic:
rw [not_cliqueFree_iff_top_isContained]

Premises used: SimpleGraph.not_cliqueFree_iff_top_isContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
f : completeGraph α ⊑ G
⊢ IsContained (α := Fin (Fintype.card α)) (completeGraph (Fin (Fintype.card α))) G

Tactic:
(Iso.completeGraph <| equivFin α).isContained'.trans f

Premises used: SimpleGraph.Iso.completeGraph, SimpleGraph.IsContained.trans, Fintype.equivFin, SimpleGraph.Iso.isContained'
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
f : completeGraph α ⊑ G
⊢ IsContained (α := Fin (Fintype.card α)) (completeGraph (Fin (Fintype.card α))) G

Tactic:
exact (Iso.completeGraph <| equivFin α).isContained'.trans f

Premises used: SimpleGraph.Iso.completeGraph, SimpleGraph.IsContained.trans, Fintype.equivFin, SimpleGraph.Iso.isContained'
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
⊢ ¬G.CliqueFree 0

Tactic:
fun h ↦ h ∅ <| isNClique_empty.mpr rfl

Premises used: Iff.mpr, SimpleGraph.isNClique_empty, EmptyCollection.emptyCollection, Not, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
ht : IsNClique ⊥ n t
⊢ LE.le (α := ℕ) 2 1

Tactic:
have := le_trans h (isNClique_bot_iff.1 ht).1
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
ht : IsNClique ⊥ n t
this : LE.le (α := ℕ) 2 1
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
obtain : ∀ (t : Finset α) (hts : t ⊆ s) (ht : #t = m), False
⊢ False

Tactic:
obtain ⟨t, hts, ht⟩ := exists_subset_card_eq (h.trans hs.card_eq.ge)

Premises used: Eq.ge, SimpleGraph.IsNClique.card_eq, Finset.exists_subset_card_eq, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
t : Finset α
hts : t ⊆ s
ht : #t = m
⊢ False

Tactic:
hG _ ⟨hs.isClique.subset hts, ht⟩

Premises used: SimpleGraph.IsNClique.isClique, SimpleGraph.IsNClique.mk, SimpleGraph.IsClique.subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
t : Finset α
hts : t ⊆ s
ht : #t = m
⊢ False

Tactic:
exact hG _ ⟨hs.isClique.subset hts, ht⟩

Premises used: SimpleGraph.IsNClique.isClique, SimpleGraph.IsNClique.mk, SimpleGraph.IsClique.subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G H : SimpleGraph α
n : ℕ
h : G ≤ H
⊢ H.CliqueFree n → G.CliqueFree n

Tactic:
forall_imp fun _ ↦ mt <| IsNClique.mono h

Premises used: SimpleGraph.IsNClique.mono, mt, forall_imp, SimpleGraph.CliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : G.CliqueFree n
contrapose : ∀ (h : ¬H.CliqueFree n), ¬G.CliqueFree n
⊢ H.CliqueFree n

Tactic:
contrapose h
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : ¬H.CliqueFree n
rw : ∀ (h : IsContained (α := Fin n) (completeGraph (Fin n)) H), IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ ¬G.CliqueFree n

Tactic:
rw [not_cliqueFree_iff_top_isContained] at h ⊢

Premises used: SimpleGraph.not_cliqueFree_iff_top_isContained
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : IsContained (α := Fin n) (completeGraph (Fin n)) H
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
h.trans hle

Premises used: SimpleGraph.IsContained.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : IsContained (α := Fin n) (completeGraph (Fin n)) H
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G

Tactic:
exact h.trans hle

Premises used: SimpleGraph.IsContained.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst : Nonempty α
inl : ∀ (hle : n ≤ 1), CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n
inr : ∀ (hlt : 1 < n), CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n
⊢ CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n

Tactic:
obtain (hle | hlt) := le_or_gt n 1

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst : Nonempty α
hle : n ≤ 1
inl : ∀ (hle : LE.le (α := ℕ) 0 1), CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) 0 ↔ G.CliqueFree 0
inl₁ : ∀ (hle : LE.le (α := ℕ) 1 1), CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) 1 ↔ G.CliqueFree 1
⊢ CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n

Tactic:
obtain (rfl | rfl) := Nat.le_one_iff_eq_zero_or_eq_one.1 hle

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
inst : Nonempty α
hle : LE.le (α := ℕ) 0 1
⊢ CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) 0 ↔ G.CliqueFree 0

Tactic:
simp [CliqueFree]

Premises used: SimpleGraph.CliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
inst : Nonempty α
hle : LE.le (α := ℕ) 1 1
⊢ CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) 1 ↔ G.CliqueFree 1

Tactic:
simp [CliqueFree, show ∃ (_ : β), True from ⟨f (Classical.arbitrary _), trivial⟩]

Premises used: trivial, SimpleGraph.CliqueFree, Exists.intro, Classical.arbitrary, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst : Nonempty α
hlt : 1 < n
⊢ CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n

Tactic:
simp [CliqueFree, isNClique_map_iff hlt]

Premises used: SimpleGraph.CliqueFree, SimpleGraph.isNClique_map_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : Fintype α
hc : Fintype.card α < n
rw : IsEmpty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)
⊢ G.CliqueFree n

Tactic:
rw [cliqueFree_iff]

Premises used: SimpleGraph.cliqueFree_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : Fintype α
hc : Fintype.card α < n
contrapose! : ∀ (hc : Nonempty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)), n ≤ Fintype.card α
⊢ IsEmpty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)

Tactic:
contrapose! hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : Fintype α
hc : Nonempty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)
⊢ n ≤ Fintype.card α

Tactic:
simpa only [Fintype.card_fin] using card_le_of_embedding hc.some.toEmbedding

Premises used: Fintype.card_fin, Nonempty.some, SimpleGraph.Copy.toEmbedding, Fintype.card_le_of_embedding
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
inst : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
rw : ∀ (a : Copy (α := Fin n) (completeGraph (Fin n)) (completeMultipartiteGraph V)), False
⊢ (completeMultipartiteGraph V).CliqueFree n

Tactic:
rw [cliqueFree_iff, isEmpty_iff]

Premises used: isEmpty_iff, SimpleGraph.cliqueFree_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
inst : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : Copy (α := Fin n) (completeGraph (Fin n)) (completeMultipartiteGraph V)
⊢ Fintype.card ι < Fintype.card (Fin n)

Tactic:
simp [hc]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
inst : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : Copy (α := Fin n) (completeGraph (Fin n)) (completeMultipartiteGraph V)
obtain :
  ∀ (v w : Fin n) (hn : v ≠ w)
    (he :
      Eq.{u_3 + 1} (α := ι)
        (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) v)
        (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) w)),
    False
⊢ False

Tactic:
obtain ⟨v, w, hn, he⟩ := exists_ne_map_eq_of_card_lt (Sigma.fst ∘ f) (by simp [hc])

Premises used: Fintype.exists_ne_map_eq_of_card_lt, Function.comp, Sigma.fst, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
inst : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : Copy (α := Fin n) (completeGraph (Fin n)) (completeMultipartiteGraph V)
v w : Fin n
hn : v ≠ w
he :
  Eq.{u_3 + 1} (α := ι)
    (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) v)
    (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) w)
⊢ Ne.{u_3 + 1} (α := ι) (Sigma.fst (β := fun (i : ι) ↦ V i) ((f.topEmbedding : (a : Fin n) → (i : ι) × V i) v))
    (Sigma.fst (β := fun (i : ι) ↦ V i) ((f.topEmbedding : (a : Fin n) → (i : ι) × V i) w))

Tactic:
rw [← top_adj, ← f.topEmbedding.map_adj_iff, comap_adj, top_adj] at hn

Premises used: SimpleGraph.Copy.topEmbedding, SimpleGraph.Embedding.map_adj_iff, SimpleGraph.top_adj, SimpleGraph.comap_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
inst : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : Copy (α := Fin n) (completeGraph (Fin n)) (completeMultipartiteGraph V)
v w : Fin n
hn : v ≠ w
he :
  Eq.{u_3 + 1} (α := ι)
    (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) v)
    (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) w)
hn₁ :
  Ne.{u_3 + 1} (α := ι) (Sigma.fst (β := fun (i : ι) ↦ V i) ((f.topEmbedding : (a : Fin n) → (i : ι) × V i) v))
    (Sigma.fst (β := fun (i : ι) ↦ V i) ((f.topEmbedding : (a : Fin n) → (i : ι) × V i) w))
⊢ Eq.{u_3 + 1} (α := ι)
    (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) v)
    (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) w)

Tactic:
rw [← top_adj, ← f.topEmbedding.map_adj_iff, comap_adj, top_adj] at hn

Premises used: SimpleGraph.Copy.topEmbedding, SimpleGraph.Embedding.map_adj_iff, SimpleGraph.top_adj, SimpleGraph.comap_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
inst : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : Copy (α := Fin n) (completeGraph (Fin n)) (completeMultipartiteGraph V)
v w : Fin n
hn :
  Ne.{u_3 + 1} (α := ι) (Sigma.fst (β := fun (i : ι) ↦ V i) ((f.topEmbedding : (a : Fin n) → (i : ι) × V i) v))
    (Sigma.fst (β := fun (i : ι) ↦ V i) ((f.topEmbedding : (a : Fin n) → (i : ι) × V i) w))
he :
  Eq.{u_3 + 1} (α := ι)
    (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) v)
    (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) w)
⊢ False

Tactic:
absurd he hn

Premises used: absurd
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
inst : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : Copy (α := Fin n) (completeGraph (Fin n)) (completeMultipartiteGraph V)
v w : Fin n
hn :
  Ne.{u_3 + 1} (α := ι) (Sigma.fst (β := fun (i : ι) ↦ V i) ((f.topEmbedding : (a : Fin n) → (i : ι) × V i) v))
    (Sigma.fst (β := fun (i : ι) ↦ V i) ((f.topEmbedding : (a : Fin n) → (i : ι) × V i) w))
he :
  Eq.{u_3 + 1} (α := ι)
    (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) v)
    (comp (β := (i : ι) × V i) (Sigma.fst (β := fun (i : ι) ↦ V i)) (⇑f : (a : Fin n) → (i : ι) × V i) w)
⊢ False

Tactic:
exact absurd he hn

Premises used: absurd
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n : ℕ
s : Finset α
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
⊢ ∀ {a b : ι},
    (completeMultipartiteGraph V).Adj
        (({ toFun := fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ V i) i (f i), inj' := ⋯ } : (a : ι) → (i : ι) × V i) a)
        (({ toFun := fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ V i) i (f i), inj' := ⋯ } : (a : ι) → (i : ι) × V i)
          b) ↔
      Adj ⊤ a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
inst : Fintype ι
f : (i : ι) → V i
hc : n ≤ Fintype.card ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
fun hf ↦ (cliqueFree_iff.1 <| hf.mono hc).elim' <|
    topEmbedding V f |>.toCopy.comp (Iso.completeGraph (equivFin ι).symm).toCopy

Premises used: SimpleGraph.Iso.completeGraph, SimpleGraph.cliqueFree_iff, SimpleGraph.completeMultipartiteGraph.topEmbedding, Fintype.equivFin, IsEmpty.elim', SimpleGraph.Iso.toCopy, Iff.mp, Equiv.symm, SimpleGraph.Copy.comp, SimpleGraph.CliqueFree.mono, Not, SimpleGraph.Embedding.toCopy
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
inst : Infinite ι
f : (i : ι) → V i
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
(topEmbedding V f |>.comp <| .completeGraph <| Fin.valEmbedding.trans <| Infinite.natEmbedding ι)
    |>.isContained.not_cliqueFree

Premises used: SimpleGraph.Embedding.completeGraph, Fin.valEmbedding, SimpleGraph.completeMultipartiteGraph.topEmbedding, SimpleGraph.IsContained.not_cliqueFree, Function.Embedding.trans, SimpleGraph.Embedding.isContained, SimpleGraph.Embedding.comp, Infinite.natEmbedding
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
hc : (↑n : ℕ∞) ≤ ENat.card ι
pos : ∀ (h : Infinite ι), ¬(completeMultipartiteGraph V).CliqueFree n
neg : ∀ (h : ¬Infinite ι), ¬(completeMultipartiteGraph V).CliqueFree n
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
by_cases h : Infinite ι

Premises used: Infinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
hc : (↑n : ℕ∞) ≤ ENat.card ι
h : Infinite ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
not_cliqueFree_of_infinite V f

Premises used: SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_infinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
hc : (↑n : ℕ∞) ≤ ENat.card ι
h : Infinite ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
exact not_cliqueFree_of_infinite V f

Premises used: SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_infinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
hc : (↑n : ℕ∞) ≤ ENat.card ι
h : ¬Infinite ι
neg : ∀ (this : Fintype ι), ¬(completeMultipartiteGraph V).CliqueFree n
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
have : Fintype ι := fintypeOfNotInfinite h
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
hc : (↑n : ℕ∞) ≤ ENat.card ι
h : ¬Infinite ι
this : Fintype ι
⊢ n ≤ Fintype.card ι

Tactic:
rw [ENat.card_eq_coe_fintype_card, Nat.cast_le] at hc

Premises used: ENat.card_eq_coe_fintype_card, Nat.cast_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
h : ¬Infinite ι
this : Fintype ι
hc : n ≤ Fintype.card ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
not_cliqueFree_of_le_card V f hc

Premises used: SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_card