awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
inl :
  ∀ (ht : #t ≤ 1),
    IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
      #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
inr :
  ∀ (ht : 1 < #t),
    IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
      #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
    #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t

Tactic:
obtain (ht | ht) := le_or_gt #t 1

Premises used: le_or_gt, Finset.card, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : #t ≤ 1
inl : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β)
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
    #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t

Tactic:
simp only [ht, true_or, iff_true]

Premises used: true_or, iff_true
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : #t ≤ 1
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β)

Tactic:
IsClique.of_subsingleton <| card_le_one.1 ht

Premises used: SimpleGraph.IsClique.of_subsingleton, Finset.card_le_one, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : #t ≤ 1
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β)

Tactic:
exact IsClique.of_subsingleton <| card_le_one.1 ht

Premises used: SimpleGraph.IsClique.of_subsingleton, Finset.card_le_one, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
inr :
  (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ↔
    ¬1 < #t ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
inr₁ : t.Nontrivial
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔
    #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t

Tactic:
rw [isClique_map_finset_iff_of_nontrivial, ← not_lt]

Premises used: SimpleGraph.isClique_map_finset_iff_of_nontrivial, not_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ↔
    ¬1 < #t ∨ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t

Tactic:
simp [ht]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ t.Nontrivial

Tactic:
Finset.one_lt_card_iff_nontrivial.mp ht

Premises used: Finset.one_lt_card_iff_nontrivial, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ t.Nontrivial

Tactic:
exact Finset.one_lt_card_iff_nontrivial.mp ht

Premises used: Finset.one_lt_card_iff_nontrivial, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
h : G.IsClique (↑s : Set α)
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑(map f s) : Set β)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set (↑F : Type u_1)
c : (S.induce F).coe.IsClique A
simp :
  ∀ ⦃x : α⦄,
    (∃ (x_1 : x ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) x ⋯ ∈ A) →
      ∀ ⦃y : α⦄, (∃ (x : y ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A) → x ≠ y → G.Adj x y
⊢ G.IsClique (Subtype.val (p := fun (x : α) ↦ x ∈ F) '' A)

Tactic:
simp only [Set.Pairwise, Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right]

Premises used: Set.mem_image, Subtype.exists, exists_eq_right, exists_and_right, Set.Pairwise
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set (↑F : Type u_1)
c : (S.induce F).coe.IsClique A
x : α
this :
  ∀ (w : x ∈ F) (ainA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) x ⋯ ∈ A) ⦃y : α⦄,
    (∃ (x : y ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A) → x ≠ y → G.Adj x y
⊢ (∃ (x_1 : x ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) x ⋯ ∈ A) →
    ∀ ⦃y : α⦄, (∃ (x : y ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A) → x ≠ y → G.Adj x y

Tactic:
⟨_, ainA⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set (↑F : Type u_1)
c : (S.induce F).coe.IsClique A
x : α
w : x ∈ F
ainA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) x ⋯ ∈ A
_ : ∀ ⦃y : α⦄, (∃ (x : y ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A) → x ≠ y → G.Adj x y
⊢ ∀ ⦃y : α⦄, (∃ (x : y ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A) → x ≠ y → G.Adj x y

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set (↑F : Type u_1)
c : (S.induce F).coe.IsClique A
x : α
w : x ∈ F
ainA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) x ⋯ ∈ A
y : α
this : ∀ (w : y ∈ F) (binA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A), x ≠ y → G.Adj x y
⊢ (∃ (x : y ∈ F), Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A) → x ≠ y → G.Adj x y

Tactic:
⟨_, binA⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set (↑F : Type u_1)
c : (S.induce F).coe.IsClique A
x : α
w : x ∈ F
ainA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) x ⋯ ∈ A
y : α
w_1 : y ∈ F
binA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A
anb : x ≠ y
⊢ G.Adj x y

Tactic:
S.adj_sub (c ainA binA (Subtype.coe_ne_coe.mp anb)).2.2

Premises used: SimpleGraph.Subgraph.adj_sub, And.right, Iff.mp, Subtype.coe_ne_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set (↑F : Type u_1)
c : (S.induce F).coe.IsClique A
x : α
w : x ∈ F
ainA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) x ⋯ ∈ A
y : α
w_1 : y ∈ F
binA : Subtype.mk (p := fun (a : α) ↦ a ∈ F) y ⋯ ∈ A
anb : x ≠ y
⊢ G.Adj x y

Tactic:
exact S.adj_sub (c ainA binA (Subtype.coe_ne_coe.mp anb)).2.2

Premises used: SimpleGraph.Subgraph.adj_sub, And.right, Iff.mp, Subtype.coe_ne_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
hc : (G ⊔ edge v w).IsClique s
x : α
hx : x ∈ s \ {v}
_ : ∀ ⦃y : α⦄, y ∈ s \ {v} → x ≠ y → G.Adj x y
⊢ ∀ ⦃y : α⦄, y ∈ s \ {v} → x ≠ y → G.Adj x y

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
hc : (G ⊔ edge v w).IsClique s
x : α
hx : x ∈ s \ {v}
y : α
hy : y ∈ s \ {v}
hxy : x ≠ y
⊢ (G ⊔ edge v w).Adj x y

Tactic:
have := hc hx.1 hy.1 hxy
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
hc : (G ⊔ edge v w).IsClique s
x : α
hx : x ∈ s \ {v}
y : α
hy : y ∈ s \ {v}
hxy : x ≠ y
this : (G ⊔ edge v w).Adj x y
⊢ G.Adj x y

Tactic:
simp_all [sup_adj, edge_adj]

Premises used: SimpleGraph.sup_adj, SimpleGraph.edge_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
pos : ∀ (h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}), (G ⊔ edge v w).Adj x y
neg : ∀ (h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})), (G ⊔ edge v w).Adj x y
⊢ (G ⊔ edge v w).Adj x y

Tactic:
by_cases h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w}
pos : ∀ (hx : x ∈ s \ {v}) (hy : y ∈ s \ {v}), (G ⊔ edge v w).Adj x y
pos₁ : ∀ (hx : x ∈ s \ {w}) (hy : y ∈ s \ {w}), (G ⊔ edge v w).Adj x y
⊢ (G ⊔ edge v w).Adj x y

Tactic:
obtain (⟨hx, hy⟩ | ⟨hx, hy⟩) := h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx_1 : x ∈ s
y : α
hy_1 : y ∈ s
hxy : x ≠ y
hx : x ∈ s \ {v}
hy : y ∈ s \ {v}
⊢ (G ⊔ edge v w).Adj x y

Tactic:
hv.mono le_sup_left hx hy hxy

Premises used: le_sup_left, SimpleGraph.IsClique.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx_1 : x ∈ s
y : α
hy_1 : y ∈ s
hxy : x ≠ y
hx : x ∈ s \ {v}
hy : y ∈ s \ {v}
⊢ (G ⊔ edge v w).Adj x y

Tactic:
exact hv.mono le_sup_left hx hy hxy

Premises used: le_sup_left, SimpleGraph.IsClique.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx_1 : x ∈ s
y : α
hy_1 : y ∈ s
hxy : x ≠ y
hx : x ∈ s \ {w}
hy : y ∈ s \ {w}
⊢ (G ⊔ edge v w).Adj x y

Tactic:
hw.mono le_sup_left hx hy hxy

Premises used: le_sup_left, SimpleGraph.IsClique.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx_1 : x ∈ s
y : α
hy_1 : y ∈ s
hxy : x ≠ y
hx : x ∈ s \ {w}
hy : y ∈ s \ {w}
⊢ (G ⊔ edge v w).Adj x y

Tactic:
exact hw.mono le_sup_left hx hy hxy

Premises used: le_sup_left, SimpleGraph.IsClique.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
pos : x = v → Sym2.ToRel {s(v, w)} x y
neg : ¬x = v → Sym2.ToRel {s(v, w)} x y
⊢ Sym2.ToRel {s(v, w)} x y

Tactic:
by_cases x = v
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
h_1 : x = v
⊢ Sym2.ToRel {s(v, w)} x y

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
h_1 : ¬x = v
⊢ Sym2.ToRel {s(v, w)} x y

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
h' : ¬(x ∈ s \ {v} ∧ y ∈ s \ {v} ∨ x ∈ s \ {w} ∧ y ∈ s \ {w})
⊢ (G ⊔ edge v w).Adj x y

Tactic:
exact Or.inr ⟨by by_cases x = v <;> aesop, hxy⟩

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
⊢ (G ⊔ edge v w).IsClique s ↔ G.IsClique (s \ {v}) ∧ G.IsClique (s \ {w})

Tactic:
⟨fun h' ↦ ⟨h'.sdiff_of_sup_edge, (edge_comm .. ▸ h').sdiff_of_sup_edge⟩,
    fun h' ↦ isClique_sup_edge_of_ne_sdiff h h'.1 h'.2⟩

Premises used: SimpleGraph.isClique_sup_edge_of_ne_sdiff, SimpleGraph.IsClique.sdiff_of_sup_edge, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
this :
  ∀ (w : β) (h : (f : (a : β) → α) w = x) ⦃y : α⦄,
    Membership.mem (γ := Set α) (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f : (a : β) → α)) y → x ≠ y → G.Adj x y
⊢ Membership.mem (γ := Set α) (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f : (a : β) → α)) x →
    ∀ ⦃y : α⦄, Membership.mem (γ := Set α) (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f : (a : β) → α)) y → x ≠ y → G.Adj x y

Tactic:
⟨_, h⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
w : β
h : (f : (a : β) → α) w = x
_ : ∀ ⦃y : α⦄, Membership.mem (γ := Set α) (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f : (a : β) → α)) y → x ≠ y → G.Adj x y
⊢ ∀ ⦃y : α⦄, Membership.mem (γ := Set α) (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f : (a : β) → α)) y → x ≠ y → G.Adj x y

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
w : β
h : (f : (a : β) → α) w = x
y : α
this : ∀ (w : β) (h' : (f : (a : β) → α) w = y), x ≠ y → G.Adj x y
⊢ Membership.mem (γ := Set α) (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f : (a : β) → α)) y → x ≠ y → G.Adj x y

Tactic:
⟨_, h'⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
w : β
h : (f : (a : β) → α) w = x
y : α
w_1 : β
h' : (f : (a : β) → α) w_1 = y
nh : x ≠ y
rw :
  ∀ (nh : Ne.{u_1 + 1} (α := α) ((f.topEmbedding : (a : β) → α) w : α) ((f.topEmbedding : (a : β) → α) w_1 : α)),
    G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
⊢ G.Adj x y

Tactic:
rw [← h, ← Copy.topEmbedding_apply, ← h', ← Copy.topEmbedding_apply] at nh ⊢

Premises used: SimpleGraph.Copy.topEmbedding_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : Copy.{u_2, u_1} (α := β) ⊤ G
x : α
w : β
h : (f : (a : β) → α) w = x
y : α
w_1 : β
h' : (f : (a : β) → α) w_1 = y
nh : Ne.{u_1 + 1} (α := α) ((f.topEmbedding : (a : β) → α) w : α) ((f.topEmbedding : (a : β) → α) w_1 : α)
rwa :
  ∀
    (nh :
      Ne.{u_1 + 1} (α := α) ((f.topEmbedding.toEmbedding (r := Adj ⊤) (s := G.Adj) : (a : β) → α) w : α)
        ((f.topEmbedding.toEmbedding (r := Adj ⊤) (s := G.Adj) : (a : β) → α) w_1 : α)),
    G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
rwa₁ : ∀ (nh : w ≠ w_1), G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
rwa₂ : ∀ (nh : Adj ⊤ w w_1), G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (nh : G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)),
    G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)
⊢ G.Adj ((f.topEmbedding : (a : β) → α) w) ((f.topEmbedding : (a : β) → α) w_1)

Tactic:
rwa [← f.topEmbedding.coe_toEmbedding, (f.topEmbedding.apply_eq_iff_eq _ _).ne,
    ← top_adj, ← f.topEmbedding.map_adj_iff] at nh

Premises used: SimpleGraph.Copy.topEmbedding, SimpleGraph.Embedding.map_adj_iff, RelEmbedding.coe_toEmbedding, SimpleGraph.top_adj, RelEmbedding.toEmbedding, Iff.ne, Function.Embedding.apply_eq_iff_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ G.IsNClique n s ↔ G.IsClique (↑s : Set α) ∧ #s = n

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

Premises used: SimpleGraph.IsNClique.card_eq, SimpleGraph.IsNClique.isClique, And.right, And.left, SimpleGraph.IsNClique.mk, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.IsNClique n ∅ ↔ n = 0

Tactic:
simp [isNClique_iff, eq_comm]

Premises used: eq_comm, SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
a : α
⊢ G.IsNClique n {a} ↔ n = 1

Tactic:
simp [isNClique_iff, eq_comm]

Premises used: eq_comm, SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
simp_rw : G.IsClique (↑s : Set α) ∧ #s = n → H.IsClique (↑s : Set α) ∧ #s = n
⊢ G.IsNClique n s → H.IsNClique n s

Tactic:
simp_rw [isNClique_iff]

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

Tactic:
And.imp_left (IsClique.mono h)

Premises used: And.imp_left, SimpleGraph.IsClique.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ G.IsClique (↑s : Set α) ∧ #s = n → H.IsClique (↑s : Set α) ∧ #s = n

Tactic:
exact And.imp_left (IsClique.mono h)

Premises used: And.imp_left, SimpleGraph.IsClique.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
rw : IsClique.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) ((⇑f : (a : α) → β) '' (↑s : Set α))
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑(map f s) : Set β)

Tactic:
rw [coe_map]

Premises used: Finset.coe_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
⊢ IsClique.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) ((⇑f : (a : α) → β) '' (↑s : Set α))

Tactic:
h.1.map

Premises used: SimpleGraph.IsNClique.isClique, SimpleGraph.IsClique.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
⊢ IsClique.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) ((⇑f : (a : α) → β) '' (↑s : Set α))

Tactic:
exact h.1.map

Premises used: SimpleGraph.IsNClique.isClique, SimpleGraph.IsClique.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
t : Finset β
f : α ↪ β
h' : #t ≤ 1
hn : 1 < #t
⊢ False

Tactic:
h'.not_gt hn

Premises used: LE.le.not_gt
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
t : Finset β
f : α ↪ β
h' : #t ≤ 1
hn : 1 < #t
⊢ False

Tactic:
exact h'.not_gt hn

Premises used: LE.le.not_gt
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
rw :
  (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ∧ #t = n ↔ ∃ (s : Finset α), G.IsNClique n s ∧ map f s = t
⊢ IsNClique (SimpleGraph.map (⇑f : (a : α) → β) G) n t ↔ ∃ (s : Finset α), G.IsNClique n s ∧ map f s = t

Tactic:
rw [isNClique_iff, isClique_map_finset_iff, or_and_right,
    or_iff_right (by rintro ⟨h', rfl⟩; exact h'.not_gt hn)]

Premises used: SimpleGraph.isClique_map_finset_iff, or_iff_right, SimpleGraph.isNClique_iff, or_and_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
mp :
  (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ∧ #t = n → ∃ (s : Finset α), G.IsNClique n s ∧ map f s = t
mpr :
  (∃ (s : Finset α), G.IsNClique n s ∧ map f s = t) → (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ∧ #t = n
⊢ (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) ∧ #t = n ↔ ∃ (s : Finset α), G.IsNClique n s ∧ map f s = t

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : G.IsClique (↑s : Set α)
hn : 1 < #(map f s)
⊢ ∃ (s_1 : Finset α), G.IsNClique (#(map f s)) s_1 ∧ map f s_1 = map f s

Tactic:
simp [isNClique_iff, hs]

Premises used: SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
f : α ↪ β
s : Finset α
hs : G.IsNClique n s
⊢ (∃ (s_1 : Finset α), G.IsClique (↑s_1 : Set α) ∧ map f s_1 = map f s) ∧ #(map f s) = n

Tactic:
simp [hs.card_eq, hs.isClique]

Premises used: SimpleGraph.IsNClique.card_eq, SimpleGraph.IsNClique.isClique
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
n : ℕ
s : Finset α
rw : (↑s : Set α).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n
⊢ IsNClique ⊥ n s ↔ n ≤ 1 ∧ #s = n

Tactic:
rw [isNClique_iff, isClique_bot_iff]

Premises used: SimpleGraph.isClique_bot_iff, SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
n : ℕ
s : Finset α
⊢ (↑s : Set α).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n

Tactic:
and_congr_left ?_

Premises used: and_congr_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
n : ℕ
s : Finset α
refine : #s = n → ((↑s : Set α).Subsingleton ↔ n ≤ 1)
⊢ (↑s : Set α).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n

Tactic:
refine and_congr_left ?_

Premises used: and_congr_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
s : Finset α
⊢ (↑s : Set α).Subsingleton ↔ #s ≤ 1

Tactic:
card_le_one.symm

Premises used: Finset.card_le_one, Set.Subsingleton, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
s : Finset α
⊢ (↑s : Set α).Subsingleton ↔ #s ≤ 1

Tactic:
exact card_le_one.symm

Premises used: Finset.card_le_one, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
simp : s = ∅ → G.IsClique (↑s : Set α)
⊢ G.IsNClique 0 s ↔ s = ∅

Tactic:
simp only [isNClique_iff, Finset.card_eq_zero, and_iff_right_iff_imp]

Premises used: and_iff_right_iff_imp, Finset.card_eq_zero, SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.IsClique (↑∅ : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
simp : (∃ (a : α), s = {a}) → G.IsClique (↑s : Set α)
⊢ G.IsNClique 1 s ↔ ∃ (a : α), s = {a}

Tactic:
simp only [isNClique_iff, card_eq_one, and_iff_right_iff_imp]

Premises used: Finset.card_eq_one, and_iff_right_iff_imp, SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.IsClique (↑{a} : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
isClique : G.IsClique (↑(insert a s) : Set α)
card_eq : #(insert a s) = n + 1
⊢ G.IsNClique (n + 1) (insert a s)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
isClique : G.IsClique (insert a (↑s : Set α))
⊢ G.IsClique (↑(insert a s) : Set α)

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique (insert a (↑s : Set α))

Tactic:
hs.1.insert fun b hb _ => h _ hb

Premises used: SimpleGraph.IsClique.insert, SimpleGraph.IsNClique.isClique
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique (insert a (↑s : Set α))

Tactic:
exact hs.1.insert fun b hb _ => h _ hb

Premises used: SimpleGraph.IsClique.insert, SimpleGraph.IsNClique.isClique
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
card_eq : #s + 1 = n + 1
card_eq₁ card_eq₂ : n + 1 = n + 1
⊢ #(insert a s) = n + 1

Tactic:
rw [card_insert_of_notMem fun ha => (h _ ha).ne rfl, hs.2]

Premises used: SimpleGraph.Adj.ne, SimpleGraph.IsNClique.card_eq, Finset.card_insert_of_notMem, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
⊢ (↑(s.erase a) : Set α) ⊆ (↑s : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
rw : #s - 1 = n - 1
rw₁ rw₂ : n - 1 = n - 1
⊢ #(s.erase a) = n - 1

Tactic:
rw [card_erase_of_mem ha, hs.2]

Premises used: SimpleGraph.IsNClique.card_eq, Finset.card_erase_of_mem