awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hba : b ≠ a
c w : α
left : G.Adj c w
hc : (f : (a : α) → β) c = a
right : (f : (a : α) → β) w = b
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a

Tactic:
⟨c, hc⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hba : b ≠ a
c w : α
left : G.Adj c w
hc : (f : (a : α) → β) c = a
right : (f : (a : α) → β) w = b
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a

Tactic:
exact ⟨c, hc⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
rw : image (⇑f : (a : α) → β) (s.preimage (⇑f : (a : α) → β) ⋯) = s
rw₁ : {x ∈ s | Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x} = s
rw₂ : s = s
rw₃ : ∀ x ∈ s, Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
rw₄ : s = s
rw₅ rw₆ rw₇ :
  ∀ (a : β) (ha : a ∈ s), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
rw₈ :
  ∀ (a : β) (ha : a ∈ s) (b : β) (hb : b ∈ s) (hba : b ≠ a),
    Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
rw₉ :
  ∀ (a : β) (ha : a ∈ s) (b : β) (hb : b ∈ s) (hba : b ≠ a) (c w : α),
    G.Adj c w →
      ∀ (hc : (f : (a : α) → β) c = a),
        (f : (a : α) → β) w = b → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
⊢ map f (s.preimage (⇑f : (a : α) → β) ⋯) = s

Tactic:
classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩

Premises used: Finset.filter_true_of_mem, Finset.image_preimage, Finset.map_eq_image
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
⊢ map f (s.preimage (⇑f : (a : α) → β) ⋯) = s

Tactic:
have hs' : (s.preimage f f.injective.injOn).map f = s := by
      classical
      rw [map_eq_image, image_preimage, filter_true_of_mem]
      rintro a ha
      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
      exact ⟨c, hc⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
hs' : map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
rw : #(map f (s.preimage (⇑f : (a : α) → β) ⋯)) = #s
rw₁ rw₂ : #s = #s
⊢ #(s.preimage (⇑f : (a : α) → β) ⋯) = #s

Tactic:
rw [← card_map f, hs']

Premises used: Finset.card_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
hs' : map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
h : G.IsClique (↑(s.preimage (⇑f : (a : α) → β) ⋯) : Set α)
⊢ s ∈ map f '' G.cliqueSet #s

Tactic:
refine ⟨s.preimage f f.injective.injOn, ⟨?_, by rw [← card_map f, hs']⟩, hs'⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
hs' : map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
h : G.IsClique ((⇑f : (a : α) → β) ⁻¹' (↑s : Set β))
⊢ G.IsClique (↑(s.preimage (⇑f : (a : α) → β) ⋯) : Set α)

Tactic:
rw [coe_preimage]

Premises used: Finset.coe_preimage
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
hs' : map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
⊢ G.IsClique ((⇑f : (a : α) → β) ⁻¹' (↑s : Set β))

Tactic:
fun a ha b hb hab => map_adj_apply.1 (hs ha hb <| f.injective.ne hab)

Premises used: Function.Injective.ne, SimpleGraph.map_adj_apply, Set.Pairwise, Iff.mp, Function.Embedding.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
hs' : map f (s.preimage (⇑f : (a : α) → β) ⋯) = s
⊢ G.IsClique ((⇑f : (a : α) → β) ⁻¹' (↑s : Set β))

Tactic:
exact fun a ha b hb hab => map_adj_apply.1 (hs ha hb <| f.injective.ne hab)

Premises used: Function.Injective.ne, SimpleGraph.map_adj_apply, Iff.mp, Function.Embedding.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : s ∈ G.cliqueSet n
⊢ Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) (map f s)

Tactic:
hs.map

Premises used: Set.Mem, setOf, SimpleGraph.IsNClique.map, SimpleGraph.cliqueSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : s ∈ G.cliqueSet n
⊢ Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) (map f s)

Tactic:
exact hs.map

Premises used: SimpleGraph.IsNClique.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
inl : cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) 1 = map e.toEmbedding '' G.cliqueSet 1
inr : ∀ (hn : n ≠ 1), cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) n = map e.toEmbedding '' G.cliqueSet n
⊢ cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) n = map e.toEmbedding '' G.cliqueSet n

Tactic:
obtain rfl | hn := eq_or_ne n 1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
inl :
  ∀ (x : Finset β),
    Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) 1) x ↔
      x ∈ map e.toEmbedding '' G.cliqueSet 1
⊢ cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) 1 = map e.toEmbedding '' G.cliqueSet 1

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
x : Finset β
⊢ Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) 1) x ↔
    x ∈ map e.toEmbedding '' G.cliqueSet 1

Tactic:
simp [e.exists_congr_left]

Premises used: Equiv.exists_congr_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
e : α ≃ β
n : ℕ
hn : n ≠ 1
⊢ cliqueSet (SimpleGraph.map (⇑e : (a : α) → β) G) n = map e.toEmbedding '' G.cliqueSet n

Tactic:
simpa using cliqueSet_map hn G e.toEmbedding

Premises used: SimpleGraph.cliqueSet_map, Equiv.toEmbedding
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
have : ∀ (this : Fintype α), BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}
⊢ BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}

Tactic:
have := ofFinite α
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
this : Fintype α
h : Membership.mem (γ := Set ℕ) (upperBounds {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}) (Fintype.card α)
⊢ BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}

Tactic:
use card α

Premises used: Fintype.card
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
this : Fintype α
y : ℕ
s : Finset α
syc : G.IsNClique y s
⊢ G.IsClique (↑s : Set α) ∧ #s = y

Tactic:
rw [isNClique_iff] at syc

Premises used: SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
this : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique (↑s : Set α) ∧ #s = y
h : #s ≤ Fintype.card α
⊢ y ≤ Fintype.card α

Tactic:
rw [← syc.right]

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
this : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique (↑s : Set α) ∧ #s = y
⊢ #s ≤ Fintype.card α

Tactic:
Finset.card_le_card (Finset.subset_univ s)

Premises used: Finset.card_le_card, Fintype.card, Finset.subset_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
this : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique (↑s : Set α) ∧ #s = y
⊢ #s ≤ Fintype.card α

Tactic:
exact Finset.card_le_card (Finset.subset_univ s)

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

Tactic:
le_csSup G.finite_cliqueNum_bddAbove (Exists.intro t ⟨tc, rfl⟩)

Premises used: SimpleGraph.IsNClique.mk, _private.0.SimpleGraph.finite_cliqueNum_bddAbove, Exists.intro, le_csSup, SimpleGraph.cliqueNum, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Finset α
tc : G.IsClique (↑t : Set α)
⊢ #t ≤ G.cliqueNum

Tactic:
exact le_csSup G.finite_cliqueNum_bddAbove (Exists.intro t ⟨tc, rfl⟩)

Premises used: SimpleGraph.IsNClique.mk, _private.0.SimpleGraph.finite_cliqueNum_bddAbove, Exists.intro, le_csSup, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
pos : ∀ (h : BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}), ∃ (s : Finset α), G.IsNClique G.cliqueNum s
neg :
  ∀ (h : ¬BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}), ∃ (s : Finset α), G.IsNClique G.cliqueNum s
⊢ ∃ (s : Finset α), G.IsNClique G.cliqueNum s

Tactic:
by_cases h : BddAbove {n | ∃ s, G.IsNClique n s}

Premises used: SimpleGraph.IsNClique, setOf, Exists, BddAbove
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
h : BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s} 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
h : BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}
⊢ ∃ (s : Finset α), G.IsNClique G.cliqueNum s

Tactic:
exact Nat.sSup_mem ⟨0, by simp⟩ h

Premises used: Nat.sSup_mem, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
h : ¬BddAbove (α := ℕ) {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}
⊢ ∃ (s : Finset α), G.IsNClique G.cliqueNum s

Tactic:
simp [cliqueNum, h]

Premises used: SimpleGraph.cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
⊢ G.IsMaximumClique s ↔ G.IsClique (↑s : Set α) ∧ ∀ (t : Finset α), G.IsClique (↑t : Set α) → #t ≤ #s

Tactic:
⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

Premises used: SimpleGraph.IsMaximumClique.isClique, And.right, And.left, And.intro, Iff.intro, SimpleGraph.IsMaximumClique.mk, SimpleGraph.IsMaximumClique.maximum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
s : Set α
⊢ Maximal G.IsClique s ↔ G.IsClique s ∧ ∀ (t : Set α), G.IsClique t → s ⊆ t → t ⊆ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Maximal
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
by_contra : ∀ (hc : ¬t ≤ (↑s : Set α)), False
⊢ t ≤ (↑s : Set α)

Tactic:
by_contra hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
have : ∀ (fint : Fintype (↑t : Type u_3)), False
⊢ False

Tactic:
have fint := ofFinite t
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
a : s = t.toFinset
⊢ G.IsMaximumClique t.toFinset

Tactic:
subst a
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
a : s = t.toFinset
M₁ : G.IsMaximumClique t.toFinset
⊢ (↑t.toFinset : Set α) ≤ t

Tactic:
subst a
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
a : s = t.toFinset
M₁ : G.IsMaximumClique t.toFinset
hsub₁ : (↑t.toFinset : Set α) ≤ t
⊢ ¬t ≤ (↑t.toFinset : Set α)

Tactic:
subst a
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
t : Set α
ht : G.IsClique t
fint : Fintype (↑t : Type u_3)
M : G.IsMaximumClique t.toFinset
hsub : (↑t.toFinset : Set α) ≤ t
hc : ¬t ≤ (↑t.toFinset : Set α)
⊢ False

Tactic:
simp_all[Set.coe_toFinset, not_true_eq_false]

Premises used: not_true_eq_false, Set.coe_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
⊢ s ≠ t.toFinset

Tactic:
have ne : s ≠ t.toFinset := fun a ↦ by subst a; simp_all[Set.coe_toFinset, not_true_eq_false]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
ne : s ≠ t.toFinset
⊢ G.IsClique (↑t.toFinset : Set α)

Tactic:
simp [Set.coe_toFinset, ht]

Premises used: Set.coe_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
ne : s ≠ t.toFinset
⊢ #t.toFinset ≤ #s

Tactic:
have hle : #t.toFinset ≤ #s := M.maximum t.toFinset (by simp [Set.coe_toFinset, ht])
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
ne : s ≠ t.toFinset
hle : #t.toFinset ≤ #s
⊢ #s < #t.toFinset

Tactic:
have hlt : #s < #t.toFinset :=
        card_lt_card (ssubset_of_ne_of_subset ne (Set.subset_toFinset.mpr hsub))
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
ne : s ≠ t.toFinset
hle : #t.toFinset ≤ #s
hlt : #s < #t.toFinset
⊢ False

Tactic:
lt_irrefl _ (lt_of_lt_of_le hlt hle)

Premises used: lt_irrefl, lt_of_lt_of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
M : G.IsMaximumClique s
t : Set α
ht : G.IsClique t
hsub : (↑s : Set α) ≤ t
hc : ¬t ≤ (↑s : Set α)
fint : Fintype (↑t : Type u_3)
ne : s ≠ t.toFinset
hle : #t.toFinset ≤ #s
hlt : #s < #t.toFinset
⊢ False

Tactic:
exact lt_irrefl _ (lt_of_lt_of_le hlt hle)

Premises used: lt_irrefl, lt_of_lt_of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
sm : G.IsMaximumClique s
⊢ G.IsClique (↑s : Set α)

Tactic:
obtain ⟨sc, sm⟩ := sm
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
sm : G.IsMaximumClique s
sc : G.IsClique (↑s : Set α)
⊢ ∀ (t : Finset α), G.IsClique (↑t : Set α) → #t ≤ #s

Tactic:
obtain ⟨sc, sm⟩ := sm
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
sc : G.IsClique (↑s : Set α)
sm : ∀ (t : Finset α), G.IsClique (↑t : Set α) → #t ≤ #s
obtain : ∀ (t : Finset α) (tc : G.IsClique (↑t : Set α)) (tcard : #t = G.cliqueNum), #s = G.cliqueNum
⊢ #s = G.cliqueNum

Tactic:
obtain ⟨t, tc, tcard⟩ := G.exists_isNClique_cliqueNum

Premises used: SimpleGraph.exists_isNClique_cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
sc : G.IsClique (↑s : Set α)
sm : ∀ (t : Finset α), G.IsClique (↑t : Set α) → #t ≤ #s
t : Finset α
tc : G.IsClique (↑t : Set α)
tcard : #t = G.cliqueNum
⊢ ¬#s < G.cliqueNum

Tactic:
simp [← tcard, sm t tc]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
sc : G.IsClique (↑s : Set α)
sm : ∀ (t : Finset α), G.IsClique (↑t : Set α) → #t ≤ #s
t : Finset α
tc : G.IsClique (↑t : Set α)
tcard : #t = G.cliqueNum
⊢ #s = G.cliqueNum

Tactic:
exact eq_of_le_of_not_lt sc.card_le_cliqueNum (by simp [← tcard, sm t tc])

Premises used: eq_of_le_of_not_lt, SimpleGraph.IsClique.card_le_cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
obtain : ∀ (s : Finset α) (snc : G.IsNClique G.cliqueNum s), ∃ (s : Finset α), G.IsMaximumClique s
⊢ ∃ (s : Finset α), G.IsMaximumClique s

Tactic:
obtain ⟨s, snc⟩ := G.exists_isNClique_cliqueNum

Premises used: SimpleGraph.exists_isNClique_cliqueNum
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
snc : G.IsNClique G.cliqueNum s
⊢ ∃ (s : Finset α), G.IsMaximumClique s

Tactic:
⟨s, ⟨snc.isClique, fun t ht => snc.card_eq.symm ▸ ht.card_le_cliqueNum⟩⟩

Premises used: SimpleGraph.IsNClique.card_eq, Eq.rec, SimpleGraph.IsNClique.isClique, Exists.intro, Eq.symm, SimpleGraph.IsClique.card_le_cliqueNum, SimpleGraph.IsMaximumClique.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_3
G : SimpleGraph α
inst : Finite α
s : Finset α
snc : G.IsNClique G.cliqueNum s
⊢ ∃ (s : Finset α), G.IsMaximumClique s

Tactic:
exact ⟨s, ⟨snc.isClique, fun t ht => snc.card_eq.symm ▸ ht.card_le_cliqueNum⟩⟩
-- 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.cliqueFinset n ↔ G.IsNClique 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.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
⊢ (↑(G.cliqueFinset n) : Set (Finset α)) = G.cliqueSet n

Tactic:
Set.ext fun _ ↦ mem_cliqueFinset_iff

Premises used: Set.ext, SimpleGraph.mem_cliqueFinset_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
simp_rw : G.cliqueFinset n = ∅ ↔ ∀ (t : Finset α), ¬G.IsNClique n t
simp_rw₁ : (∀ (x : Finset α), x ∉ G.cliqueFinset n) ↔ ∀ (t : Finset α), ¬G.IsNClique n t
⊢ G.cliqueFinset n = ∅ ↔ G.CliqueFree n

Tactic:
simp_rw [CliqueFree, eq_empty_iff_forall_notMem, mem_cliqueFinset_iff]

Premises used: Finset.eq_empty_iff_forall_notMem, SimpleGraph.mem_cliqueFinset_iff, SimpleGraph.CliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
rw : #(G.cliqueFinset n) ≤ Finset.card.{u_1} (α := Finset α) (powersetCard n univ)
⊢ #(G.cliqueFinset n) ≤ (Fintype.card α).choose n

Tactic:
rw [← card_univ, ← card_powersetCard]

Premises used: Finset.card_univ, Finset.card_powersetCard
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
⊢ #(G.cliqueFinset n) ≤ Finset.card.{u_1} (α := Finset α) (powersetCard n univ)

Tactic:
card_mono fun s => ?_

Premises used: Finset.card_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
refine : ∀ s ∈ G.cliqueFinset n, Membership.mem (γ := Finset (Finset α)) (powersetCard n univ) s
⊢ #(G.cliqueFinset n) ≤ Finset.card.{u_1} (α := Finset α) (powersetCard n univ)

Tactic:
refine card_mono fun s => ?_

Premises used: Finset.card_mono
-- 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.cliqueFinset n → Membership.mem (γ := Finset (Finset α)) (powersetCard n univ) s

Tactic:
simpa [mem_powersetCard_univ] using IsNClique.card_eq

Premises used: SimpleGraph.IsNClique.card_eq, Finset.mem_powersetCard_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
inst_3 : DecidableRel H.Adj
h : G ≤ H
⊢ G.cliqueFinset n ⊆ H.cliqueFinset n

Tactic:
monotone_filter_right _ fun _ _ ↦ IsNClique.mono h

Premises used: SimpleGraph.IsNClique.mono, Set.Mem, setOf, Finset.monotone_filter_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
n : ℕ
inst_3 : Fintype β
inst_4 : DecidableEq β
f : α ↪ β
hn : n ≠ 1
simp_rw :
  cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
simp_rw₁ :
  map f '' G.cliqueSet n =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))
simp_rw₂ :
  map f '' G.cliqueSet n =
    (⇑{ toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) } :
        (a : Finset α) → Finset β) ''
      (↑(G.cliqueFinset n) : Set (Finset α))
simp_rw₃ :
  map f '' G.cliqueSet n =
    (⇑{ toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) } :
        (a : Finset α) → Finset β) ''
      G.cliqueSet n
⊢ (↑(cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) n) : Set (Finset β)) =
    (↑(map { toFun := map f, inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Finset α) (Finset β) }
          (G.cliqueFinset n)) :
      Set (Finset β))

Tactic:
simp_rw [coe_cliqueFinset, cliqueSet_map hn, coe_map, coe_cliqueFinset, Embedding.coeFn_mk]

Premises used: SimpleGraph.coe_cliqueFinset, SimpleGraph.cliqueSet_map, Function.Embedding.coeFn_mk, Finset.coe_map