awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x : α // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsNClique n s
⊢ G.IsNClique n (map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ } s)
have rw : ∀ (cc : (S.induce F).coe.IsClique (↑s : Set (↑(S.induce F).verts : Type u_1)) ∧ #s = n),
  G.IsClique
      (↑(map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := sorry : { x : α // x ∈ F } ↪ α } s) : Set α) ∧
    #(map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := sorry : { x : α // x ∈ F } ↪ α } s) = n
Tactic: rw [isNClique_iff] at cc ⊢
Cleared hypotheses: cc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
      (↑(map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ : { x : α // x ∈ F } ↪ α } s) : Set α) ∧
    #(map { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := ⋯ : { x : α // x ∈ F } ↪ α } s) = n
have simp : G.IsClique
    ((⇑{ toFun := Subtype.val (p := fun (x : α) ↦ x ∈ F), inj' := sorry } : (a : { x : α // x ∈ F }) → α) ''
      (↑s : Set { x : α // x ∈ F })) ∧
  #s = n
Tactic: simp only [coe_map, card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
v w : α
s : Finset α
n : ℕ
hc : (G ⊔ edge v w).IsNClique n s
hx : v ∈ s
⊢ #(s.erase v) = n - 1
have rw : #s - 1 = n - 1
Tactic: rw [card_erase_of_mem hx, hc.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ #(s.erase v) = n - 1
have rw₁ : n - 1 = n - 1
Tactic: rw [card_erase_of_mem hx, hc.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst : Fintype β
f : Copy.{u_2, u_1} (α := β) ⊤ G
⊢ G.IsNClique (Fintype.card β) (map f.toEmbedding univ)
have rw : G.IsClique (Set.range.{u_1, u_2 + 1} (ι := β) (⇑f.toEmbedding : (a : β) → α)) ∧ Fintype.card β = Fintype.card β
Tactic: rw [isNClique_iff, card_map, card_univ, coe_map, coe_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
h : IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ ¬G.CliqueFree n
have this : G.IsNClique (Fintype.card (Fin n)) (map (Nonempty.some h).toEmbedding univ)
Tactic: have := isNClique_map_copy_top h.some
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
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.CliqueFree n
have this₁ : G.IsNClique n (map (Nonempty.some h).toEmbedding univ)
Tactic: rw [Fintype.card_fin] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
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) (completeGraph (Fin n)) G
have h₁ : ∃ (t : Finset α), G.IsNClique n t
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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) (completeGraph (Fin n)) G
have apply : Embedding (V := Fin n) (completeGraph (Fin n)) (induce (↑(h.choose (p := G.IsNClique n)) : Set α) G)
Tactic: apply Embedding.induce (h.choose : Set α) |>.comp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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) (completeGraph (Fin n)) (induce (↑(h.choose (p := G.IsNClique n)) : Set α) G)
have rw : Embedding (V := Fin n) (W := (↑(↑(h.choose (p := G.IsNClique n)) : Set α) : Type u_1)) (completeGraph (Fin n)) ⊤
Tactic: rw [G.isClique_iff_induce_eq.mp h.choose_spec.isClique]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.CliqueFree n ↔ IsEmpty.{max (u_1 + 1) 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)
have contrapose! : ¬G.CliqueFree n ↔ Nonempty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
β : Type u_3
inst : Fintype β
⊢ G.CliqueFree (Fintype.card β) ↔ Free.{u_3, u_1} (α := β) ⊤ G
have rw : ¬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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
β : Type u_3
inst : Fintype β
rw : ¬G.CliqueFree (Fintype.card β) ↔ ¬Free.{u_3, u_1} (α := β) ⊤ G
⊢ G.CliqueFree (Fintype.card β) ↔ Free.{u_3, u_1} (α := β) ⊤ G
have rw₁ : ¬G.CliqueFree (Fintype.card β) ↔ IsContained.{u_3, u_1} (α := β) ⊤ G
Tactic: rw [← not_iff_not, not_free, not_cliqueFree_iff_top_isContained,
    isContained_congr (Iso.completeGraph (equivFin β)) Iso.refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ G.CliqueFree (Fintype.card β) ↔ Free.{u_3, u_1} (α := β) ⊤ G
have rw₂ : IsContained (α := Fin (Fintype.card β)) (completeGraph (Fin (Fintype.card β))) G ↔ IsContained.{u_3, u_1} (α := β) ⊤ G
Tactic: rw [← not_iff_not, not_free, not_cliqueFree_iff_top_isContained,
    isContained_congr (Iso.completeGraph (equivFin β)) Iso.refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ G.CliqueFree (Fintype.card β) ↔ Free.{u_3, u_1} (α := β) ⊤ G
have rw₃ : IsContained (α := Fin (Fintype.card β)) (completeGraph (Fin (Fintype.card β))) G ↔
  IsContained (α := Fin (Fintype.card β)) (completeGraph (Fin (Fintype.card β))) G
Tactic: rw [← not_iff_not, not_free, not_cliqueFree_iff_top_isContained,
    isContained_congr (Iso.completeGraph (equivFin β)) Iso.refl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : Fintype α
f : completeGraph α ⊑ G
⊢ ¬G.CliqueFree (Fintype.card α)
have rw : IsContained (α := Fin (Fintype.card α)) (completeGraph (Fin (Fintype.card α))) G
Tactic: rw [not_cliqueFree_iff_top_isContained]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
ht : IsNClique ⊥ n t
⊢ False
have this : LE.le (α := ℕ) 2 1
Tactic: have := le_trans h (isNClique_bot_iff.1 ht).1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
⊢ False
have obtain : ∀ (t : Finset α) (hts : t ⊆ s) (ht : #t = m), False
Tactic: obtain ⟨t, hts, ht⟩ := exists_subset_card_eq (h.trans hs.card_eq.ge)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : G.CliqueFree n
⊢ H.CliqueFree n
have contrapose : ∀ (h : ¬H.CliqueFree n), ¬G.CliqueFree n
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : ¬H.CliqueFree n
⊢ ¬G.CliqueFree n
have rw : ∀ (h : IsContained (α := Fin n) (completeGraph (Fin n)) H), IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: rw [not_cliqueFree_iff_top_isContained] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst : Nonempty α
⊢ CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n
have inl : ∀ (hle : n ≤ 1), CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n
Tactic: obtain (hle | hlt) := le_or_gt n 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n
have inr : ∀ (hlt : 1 < n), CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n
Tactic: obtain (hle | hlt) := le_or_gt n 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
f : α ↪ β
inst : Nonempty α
hle : n ≤ 1
⊢ CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n
have inl : ∀ (hle : LE.le (α := ℕ) 0 1), CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) 0 ↔ G.CliqueFree 0
Tactic: obtain (rfl | rfl) := Nat.le_one_iff_eq_zero_or_eq_one.1 hle
Cleared hypotheses: n, hle
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
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
⊢ CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) n ↔ G.CliqueFree n
have inl₁ : ∀ (hle : LE.le (α := ℕ) 1 1), CliqueFree.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G) 1 ↔ G.CliqueFree 1
Tactic: obtain (rfl | rfl) := Nat.le_one_iff_eq_zero_or_eq_one.1 hle
Cleared hypotheses: n, hle
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : Fintype α
hc : Fintype.card α < n
⊢ G.CliqueFree n
have rw : IsEmpty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)
Tactic: rw [cliqueFree_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : Fintype α
hc : Fintype.card α < n
⊢ IsEmpty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)
have contrapose! : ∀ (hc : Nonempty.{u_1 + 1} (Copy (α := Fin n) (completeGraph (Fin n)) G)), n ≤ Fintype.card α
Tactic: contrapose! hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
n : ℕ
ι : Type u_3
inst : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
⊢ (completeMultipartiteGraph V).CliqueFree n
have rw : ∀ (a : Copy (α := Fin n) (completeGraph (Fin n)) (completeMultipartiteGraph V)), False
Tactic: rw [cliqueFree_iff, isEmpty_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
n : ℕ
ι : Type u_3
inst : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : Copy (α := Fin n) (completeGraph (Fin n)) (completeMultipartiteGraph V)
⊢ False
have 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
Tactic: obtain ⟨v, w, hn, he⟩ := exists_ne_map_eq_of_card_lt (Sigma.fst ∘ f) (by simp [hc])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
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)
⊢ False
have 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))
Tactic: rw [← top_adj, ← f.topEmbedding.map_adj_iff, comap_adj, top_adj] at hn
Cleared hypotheses: hn, he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
hc : (↑n : ℕ∞) ≤ ENat.card ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n
have pos : ∀ (h : Infinite ι), ¬(completeMultipartiteGraph V).CliqueFree n
Tactic: by_cases h : Infinite ι
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
hc : (↑n : ℕ∞) ≤ ENat.card ι
pos : ∀ (h : Infinite ι), ¬(completeMultipartiteGraph V).CliqueFree n
⊢ ¬(completeMultipartiteGraph V).CliqueFree n
have neg : ∀ (h : ¬Infinite ι), ¬(completeMultipartiteGraph V).CliqueFree n
Tactic: by_cases h : Infinite ι
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
hc : (↑n : ℕ∞) ≤ ENat.card ι
h : ¬Infinite ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n
have neg : ∀ (this : Fintype ι), ¬(completeMultipartiteGraph V).CliqueFree n
Tactic: have : Fintype ι := fintypeOfNotInfinite h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
hc : (↑n : ℕ∞) ≤ ENat.card ι
h : ¬Infinite ι
this : Fintype ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n
have hc₁ : n ≤ Fintype.card ι
Tactic: rw [ENat.card_eq_coe_fintype_card, Nat.cast_le] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : G.CliqueFree n
s t : α
⊢ (G.replaceVertex s t).CliqueFree n
have contrapose : ∀ (h : ¬(G.replaceVertex s t).CliqueFree n), ¬G.CliqueFree n
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
⊢ ¬G.CliqueFree n
have have : ∀ (φ : Fin n ↪ α)
  (hφ :
    ∀ {a b : Fin n},
      (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b),
  ¬G.CliqueFree n
Tactic: have ⟨φ, hφ⟩ := topEmbeddingOfNotCliqueFree h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
⊢ ¬G.CliqueFree n
have rw : IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: rw [not_cliqueFree_iff_top_isContained]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have pos : ∀ (mt : Membership.mem (γ := Set α) (Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)) t),
  IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: by_cases mt : t ∈ Set.range φ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
pos :
  ∀ (mt : Membership.mem (γ := Set α) (Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)) t),
    IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have neg : ∀ (mt : t ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)), IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: by_cases mt : t ∈ Set.range φ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
mt : Membership.mem (γ := Set α) (Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)) t
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have pos : ∀ (x : Fin n) (hx : (φ : (a : Fin n) → α) x = t), IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: obtain ⟨x, hx⟩ := mt
Cleared hypotheses: mt
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have pos : ∀ (ms : Membership.mem (γ := Set α) (Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)) s),
  IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: by_cases ms : s ∈ Set.range φ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
pos :
  ∀ (ms : Membership.mem (γ := Set α) (Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)) s),
    IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have neg : ∀ (ms : s ∉ Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)), IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: by_cases ms : s ∈ Set.range φ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
ms : Membership.mem (γ := Set α) (Set.range (ι := Fin n) (⇑φ : (a : Fin n) → α)) s
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have pos : ∀ (y : Fin n) (hy : (φ : (a : Fin n) → α) y = s), IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: obtain ⟨y, hy⟩ := ms
Cleared hypotheses: ms
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
y : Fin n
hy : (φ : (a : Fin n) → α) y = s
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have e : (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) x) ((φ : (a : Fin n) → α) y) ↔ Adj (completeGraph (Fin n)) x y
Tactic: have e := @hφ x y
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
y : Fin n
hy : (φ : (a : Fin n) → α) y = s
e : (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) x) ((φ : (a : Fin n) → α) y) ↔ Adj (completeGraph (Fin n)) x y
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have e₁ : x = y
Tactic: simp_rw [hx, hy, adj_comm, not_adj_replaceVertex_same, top_adj, false_iff, not_ne_iff] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
y : Fin n
hy : (φ : (a : Fin n) → α) y = s
e : x = y
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have pos : ∀ (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) x)).CliqueFree n) (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n)
  (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff_top_isContained] at h
Cleared hypotheses: h, hx, y, hy, e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
y : Fin n
hy : (φ : (a : Fin n) → α) y = s
e : x = y
pos :
  ∀ (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) x)).CliqueFree n) (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have pos₁ : ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) y)).CliqueFree n)
  (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff_top_isContained] at h
Cleared hypotheses: h, hx, y, hy, e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Clique (goal)
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    (G.replaceVertex s t).Adj ((φ : (a : Fin n) → α) a) ((φ : (a : Fin n) → α) b) ↔ Adj (completeGraph (Fin n)) a b
x : Fin n
hx : (φ : (a : Fin n) → α) x = t
y : Fin n
hy : (φ : (a : Fin n) → α) y = s
e : x = y
pos :
  ∀ (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) x)).CliqueFree n) (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
pos₁ :
  ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬(G.replaceVertex s ((φ : (a : Fin n) → α) y)).CliqueFree n)
    (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
⊢ IsContained (α := Fin n) (completeGraph (Fin n)) G
have pos₂ : ∀ (hx : (φ : (a : Fin n) → α) x = t) (y : Fin n) (h : ¬(G.replaceVertex s s).CliqueFree n)
  (hy : (φ : (a : Fin n) → α) y = s) (e : x = y), IsContained (α := Fin n) (completeGraph (Fin n)) G
Tactic: rwa [← hx, e, hy, replaceVertex_self, not_cliqueFree_iff_top_isContained] at h
Cleared hypotheses: h, hx, y, hy, e