awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
x x_1 : Fin (cycle n).tail.support.length
i : ℕ
hi_1 : i < (cycle n).tail.support.length
hi : i < (cycle n).support.tail.length
j : ℕ
hj_1 : j < (cycle n).tail.support.length
hj : j < (cycle n).support.tail.length
hij : (cycle n).getVert (i + 1) = (cycle n).getVert (j + 1)
⊢ (⟨i, hi_1⟩ : Fin (cycle n).tail.support.length) = ⟨j, hj_1⟩

Tactic:
grind [← Nat.mod_eq_of_lt, cycleGraph.getVert_cycle]

Premises used: SimpleGraph.cycleGraph.getVert_cycle, Nat.mod_eq_of_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
n : ℕ
⊢ 3 ≤ (cycle n).length

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.IsClique s ↔ s.Pairwise G.Adj

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ ¬G.IsClique s ↔ ∃ (v : (↑s : Type u_1)) (w : (↑s : Type u_1)), v ≠ w ∧ ¬G.Adj (↑v : α) (↑w : α)

Tactic:
aesop (add simp [isClique_iff, Set.Pairwise])

Premises used: Set.Pairwise, SimpleGraph.isClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
mp : s.Pairwise G.Adj → induce s G = ⊤
mpr : induce s G = ⊤ → s.Pairwise G.Adj
⊢ s.Pairwise G.Adj ↔ induce s G = ⊤

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
mp :
  ∀ (v : α) (hv : v ∈ s) (w : α) (hw : w ∈ s),
    (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) ↔
      Adj ⊤ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
⊢ induce s G = ⊤

Tactic:
ext ⟨v, hv⟩ ⟨w, hw⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
mp :
  G.Adj
      ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : { x : α // x ∈ s }) → α)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv))
      ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : { x : α // x ∈ s }) → α)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)) ↔
    ¬v = w
⊢ (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) ↔
    Adj ⊤ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)

Tactic:
simp only [comap_adj, top_adj, Ne, Subtype.mk_eq_mk]

Premises used: SimpleGraph.top_adj, Ne, SimpleGraph.comap_adj, Subtype.mk_eq_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ G.Adj
      ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : { x : α // x ∈ s }) → α)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv))
      ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : { x : α // x ∈ s }) → α)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)) ↔
    ¬v = w

Tactic:
⟨Adj.ne, h hv hw⟩

Premises used: SimpleGraph.Adj.ne, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ G.Adj
      ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : { x : α // x ∈ s }) → α)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv))
      ((Embedding.subtype fun (x : α) ↦ x ∈ s : (a : { x : α // x ∈ s }) → α)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)) ↔
    ¬v = w

Tactic:
exact ⟨Adj.ne, h hv hw⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
⊢ (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) =
    (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)

Tactic:
have h2 : (G.induce s).Adj ⟨v, hv⟩ ⟨w, hw⟩ = _ := rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) =
    (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
rw : Adj ⊤ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
| (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) =
    (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
⊢ Adj ⊤ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) =
    (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)

Tactic:
conv_lhs at h2 => rw [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 :
  Adj ⊤ (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw) =
    (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
⊢ ¬v = w ↔ (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)

Tactic:
simp only [top_adj, ne_eq, Subtype.mk.injEq, eq_iff_iff] at h2

Premises used: SimpleGraph.top_adj, ne_eq, Subtype.mk.injEq, eq_iff_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 : ¬v = w ↔ (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
⊢ G.Adj v w

Tactic:
h2.1 hne

Premises used: Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : induce s G = ⊤
v : α
hv : v ∈ s
w : α
hw : w ∈ s
hne : v ≠ w
h2 : ¬v = w ↔ (induce s G).Adj (Subtype.mk (p := fun (x : α) ↦ x ∈ s) v hv) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) w hw)
⊢ G.Adj v w

Tactic:
exact h2.1 hne

Premises used: Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.IsClique s ↔ IsChain G.Adj s

Tactic:
simp [IsChain, G.symm.iff]

Premises used: SimpleGraph.symm, IsChain, Symmetric.iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.IsClique ∅

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.IsClique {a}

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
s : Set α
G : SimpleGraph α
hs : s.Subsingleton
⊢ G.IsClique s

Tactic:
hs.pairwise G.Adj

Premises used: SimpleGraph.Adj, Set.Subsingleton.pairwise
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
⊢ G.IsClique {a, b} ↔ a ≠ b → G.Adj a b

Tactic:
Set.pairwise_pair_of_symmetric G.symm

Premises used: SimpleGraph.symm, Set.pairwise_pair_of_symmetric
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
⊢ G.IsClique (insert a s) ↔ G.IsClique s ∧ ∀ b ∈ s, a ≠ b → G.Adj a b

Tactic:
Set.pairwise_insert_of_symmetric G.symm

Premises used: SimpleGraph.symm, Set.pairwise_insert_of_symmetric
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
ha : a ∉ s
⊢ G.IsClique (insert a s) ↔ G.IsClique s ∧ ∀ b ∈ s, G.Adj a b

Tactic:
Set.pairwise_insert_of_symmetric_of_notMem G.symm ha

Premises used: Set.pairwise_insert_of_symmetric_of_notMem, SimpleGraph.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
hs : G.IsClique s
h : ∀ b ∈ s, a ≠ b → G.Adj a b
⊢ G.IsClique (Insert.insert a s)

Tactic:
hs.insert_of_symmetric G.symm h

Premises used: SimpleGraph.symm, Set.Pairwise.insert_of_symmetric
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G H : SimpleGraph α
s : Set α
h : G ≤ H
⊢ G.IsClique s → H.IsClique s

Tactic:
Set.Pairwise.mono' h

Premises used: Set.Pairwise.mono'
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s t : Set α
h : t ⊆ s
⊢ G.IsClique s → G.IsClique t

Tactic:
Set.Pairwise.mono h

Premises used: Set.Pairwise.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
s : Set α
⊢ IsClique ⊥ s ↔ s.Subsingleton

Tactic:
Set.pairwise_bot_iff

Premises used: Set.pairwise_bot_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
h : G.IsClique s
f : α ↪ β
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
⊢ Adj.{u_2} (V := β) (SimpleGraph.map (⇑f : (a : α) → β) G : SimpleGraph β) ((f : (a : α) → β) a : β)
    ((f : (a : α) → β) b : β)

Tactic:
⟨hab, a, b, h ha hb <| ne_of_apply_ne _ hab, rfl, rfl⟩

Premises used: ne_of_apply_ne, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
h : G.IsClique s
f : α ↪ β
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
⊢ Adj.{u_2} (V := β) (SimpleGraph.map (⇑f : (a : α) → β) G : SimpleGraph β) ((f : (a : α) → β) a : β)
    ((f : (a : α) → β) b : β)

Tactic:
exact ⟨hab, a, b, h ha hb <| ne_of_apply_ne _ hab, rfl, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
x : Set α
hs : G.IsClique x
ht : Set.Nontrivial.{u_2} (α := β) ((⇑f : (a : α) → β) '' x)
⊢ IsClique.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) ((⇑f : (a : α) → β) '' x)

Tactic:
hs.map

Premises used: SimpleGraph.IsClique.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
x : Set α
hs : G.IsClique x
ht : Set.Nontrivial.{u_2} (α := β) ((⇑f : (a : α) → β) '' x)
⊢ IsClique.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) ((⇑f : (a : α) → β) '' x)

Tactic:
exact hs.map

Premises used: SimpleGraph.IsClique.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
refine_1 : ∀ (h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t), G.IsClique ((⇑f : (a : α) → β) ⁻¹' t)
refine_2 :
  ∀ (h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t),
    Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' t) = t
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t

Tactic:
refine ⟨fun h ↦ ⟨f ⁻¹' t, ?_, ?_⟩, by rintro ⟨x, hs, rfl⟩; exact hs.map⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : α
hx : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
y : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
hne : x ≠ y
⊢ Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : α
hx : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
y : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
hne : x ≠ y
refine_1 :
  ∀ (u v : α) (huv : G.Adj u v) (hux : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) u : β) ((f : (a : α) → β) x : β))
    (hvy : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) v : β) ((f : (a : α) → β) y : β)), G.Adj x y
⊢ G.Adj x y

Tactic:
obtain ⟨-, u, v, huv, hux, hvy⟩ := h hx hy (by simpa)
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : α
hx : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
y : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) u : β) ((f : (a : α) → β) x : β)
hvy : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) v : β) ((f : (a : α) → β) y : β)
⊢ u = x

Tactic:
rw [EmbeddingLike.apply_eq_iff_eq] at hux hvy

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : α
hx : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
y : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) u : β) ((f : (a : α) → β) x : β)
hvy : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) v : β) ((f : (a : α) → β) y : β)
hux₁ : u = x
⊢ v = y

Tactic:
rw [EmbeddingLike.apply_eq_iff_eq] at hux hvy

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : α
hx : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
y : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) y : β)
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : u = x
hvy : v = y
refine_1 : G.Adj u y
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : G.Adj u v
⊢ G.Adj x y

Tactic:
rwa [← hux, ← hvy]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
refine_2 : t ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' t) = t

Tactic:
rw [Set.image_preimage_eq_iff]

Premises used: Set.image_preimage_eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : β
hxt : x ∈ t
refine_2 :
  ∀ (y : β) (hyt : y ∈ t) (hyne : y ≠ x),
    Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x

Tactic:
obtain ⟨y, hyt, hyne⟩ := ht.exists_ne x

Premises used: Set.Nontrivial.exists_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
x : β
hxt : x ∈ t
y : β
hyt : y ∈ t
hyne : y ≠ x
refine_2 :
  ∀ (u v : α) (hyt : Membership.mem (α := β) t ((f : (a : α) → β) u : β))
    (hxt : Membership.mem (α := β) t ((f : (a : α) → β) v : β))
    (hyne : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) u : β) ((f : (a : α) → β) v : β)),
    Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      ((f : (a : α) → β) v : β)
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x

Tactic:
obtain ⟨-, u, v, -, rfl, rfl⟩ := h hyt hxt hyne

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
u v : α
hyt : Membership.mem (α := β) t ((f : (a : α) → β) u : β)
hxt : Membership.mem (α := β) t ((f : (a : α) → β) v : β)
hyne : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) u : β) ((f : (a : α) → β) v : β)
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) v : β)

Tactic:
Set.mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t
u v : α
hyt : Membership.mem (α := β) t ((f : (a : α) → β) u : β)
hxt : Membership.mem (α := β) t ((f : (a : α) → β) v : β)
hyne : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) u : β) ((f : (a : α) → β) v : β)
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    ((f : (a : α) → β) v : β)

Tactic:
exact Set.mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
inl :
  ∀ (ht : t.Subsingleton),
    IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔
      t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t
inr :
  ∀ (ht : t.Nontrivial),
    IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔
      t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔
    t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t

Tactic:
obtain (ht | ht) := t.subsingleton_or_nontrivial

Premises used: Set.subsingleton_or_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Subsingleton
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔
    t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t

Tactic:
simp [IsClique.of_subsingleton, ht]

Premises used: SimpleGraph.IsClique.of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) t ↔
    t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = t

Tactic:
simp [isClique_map_iff_of_nontrivial ht, ht.not_subsingleton]

Premises used: Set.Nontrivial.not_subsingleton, SimpleGraph.isClique_map_iff_of_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
rw :
  (s.Subsingleton ∨
      ∃ (s_1 : Set α),
        G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
    G.IsClique s
⊢ IsClique.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) ((⇑f : (a : α) → β) '' s) ↔ G.IsClique s

Tactic:
rw [isClique_map_iff, f.injective.subsingleton_image_iff]

Premises used: Function.Injective.subsingleton_image_iff, Function.Embedding.injective, SimpleGraph.isClique_map_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
inl :
  ∀ (hs : s.Subsingleton),
    (s.Subsingleton ∨
        ∃ (s_1 : Set α),
          G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
      G.IsClique s
inr :
  ∀ (hs : s.Nontrivial),
    (s.Subsingleton ∨
        ∃ (s_1 : Set α),
          G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
      G.IsClique s
⊢ (s.Subsingleton ∨
      ∃ (s_1 : Set α),
        G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
    G.IsClique s

Tactic:
obtain (hs | hs) := s.subsingleton_or_nontrivial

Premises used: Set.subsingleton_or_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Subsingleton
⊢ (s.Subsingleton ∨
      ∃ (s_1 : Set α),
        G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
    G.IsClique s

Tactic:
simp [hs, IsClique.of_subsingleton]

Premises used: SimpleGraph.IsClique.of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Nontrivial
⊢ (s.Subsingleton ∨
      ∃ (s_1 : Set α),
        G.IsClique s_1 ∧ Eq.{u_2 + 1} (α := Set β) ((⇑f : (a : α) → β) '' s_1) ((⇑f : (a : α) → β) '' s)) ↔
    G.IsClique s

Tactic:
simp [or_iff_right hs.not_subsingleton, Set.image_eq_image f.injective]

Premises used: Set.image_eq_image, Set.Nontrivial.not_subsingleton, Function.Embedding.injective, or_iff_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
mp :
  IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) → ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
mpr :
  (∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t) →
    IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β)
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) ↔ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (↑t : Set β).Nontrivial

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
mp :
  (∃ (s : Set α), G.IsClique s ∧ (⇑f : (a : α) → β) '' s = (↑t : Set β)) →
    ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑t : Set β) → ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t

Tactic:
rw [isClique_map_iff_of_nontrivial (by simpa)]

Premises used: SimpleGraph.isClique_map_iff_of_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Set α
hs : G.IsClique s
hst : (⇑f : (a : α) → β) '' s = (↑t : Set β)
⊢ Set.Finite.{u_2} (α := β) ((⇑f : (a : α) → β) '' s)

Tactic:
simp [hst]
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Set α
hs : G.IsClique s
hst : (⇑f : (a : α) → β) '' s = (↑t : Set β)
mp :
  ∀ (s : Finset α) (hs : G.IsClique (↑s : Set α)) (hst : (⇑f : (a : α) → β) '' (↑s : Set α) = (↑t : Set β)),
    ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t
⊢ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t

Tactic:
obtain ⟨s, rfl⟩ := Set.Finite.exists_finset_coe <|
      (show s.Finite from Set.Finite.of_finite_image (by simp [hst]) f.injective.injOn)

Premises used: Function.Injective.injOn, Set.Finite.of_finite_image, Function.Embedding.injective, Set.Finite.exists_finset_coe, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Finset α
hs : G.IsClique (↑s : Set α)
hst : (⇑f : (a : α) → β) '' (↑s : Set α) = (↑t : Set β)
⊢ (↑(map f s) : Set β) = (↑t : Set β)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Finset α
hs : G.IsClique (↑s : Set α)
hst : (⇑f : (a : α) → β) '' (↑s : Set α) = (↑t : Set β)
⊢ ∃ (s : Finset α), G.IsClique (↑s : Set α) ∧ map f s = t

Tactic:
exact ⟨s,hs, Finset.coe_inj.1 (by simpa)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : G.IsClique (↑s : Set α)
ht : (map f s).Nontrivial
⊢ IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑(map f s) : Set β)

Tactic:
simpa using hs.map (f := f)

Premises used: SimpleGraph.IsClique.map