mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
h : completeGraph (Fin n) ⊑ G
this : G.IsNClique n (map (Nonempty.some h).toEmbedding univ)
⊢ ¬G.CliqueFree n

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
h : completeGraph (Fin n) ⊑ G
this : G.IsNClique n (map (Nonempty.some h).toEmbedding univ)
⊢ ¬G.CliqueFree n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ t, G.IsNClique n t
⊢ completeGraph (Fin n) ↪g ⊤

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n✝ : ℕ
s : Finset α
n : ℕ
h : ∃ t, G.IsNClique n t
⊢ completeGraph (Fin n) ↪g ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ p.getVert (p.length - 1) = u

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ p.getVert (p.length - 1) = u
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ p.length = 1

Tactic:
by
  suffices p.length - 1 = 0 by grind [length_edges]
  rw [← hp.getVert_eq_start_iff <| p.length.sub_le 1]
  exact (hp.eq_penultimate_of_mem_edges <| Sym2.eq_swap ▸ h).symm

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
β : Type u_3
inst✝ : Fintype β
⊢ completeGraph (Fin (Fintype.card β)) ⊑ G ↔ completeGraph (Fin (Fintype.card β)) ⊑ G

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Fintype α
f : completeGraph α ⊑ G
⊢ completeGraph (Fin (Fintype.card α)) ⊑ G

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Fintype α
f : completeGraph α ⊑ G
⊢ completeGraph (Fin (Fintype.card α)) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
k✝ : ℕ
hl✝ : k✝ ≤ p.length
hl : k✝ = 1
⊢ v = v

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : completeGraph (Fin n) ⊑ H
⊢ completeGraph (Fin n) ⊑ G

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
hle : H ⊑ G
h : completeGraph (Fin n) ⊑ H
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
⊢ IsEmpty ((completeGraph (Fin n)).Copy G)

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
⊢ IsEmpty ((completeGraph (Fin n)).Copy G)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
⊢ ∀ (a : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)), False

Tactic:
]

Goal state after:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
⊢ ∀ (a : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)), False
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
v w : Fin n
hn : (f.topEmbedding v).fst ≠ (f.topEmbedding w).fst
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False

Tactic:
]

Goal state after:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
v w : Fin n
hn : (f.topEmbedding v).fst ≠ (f.topEmbedding w).fst
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(A.sup id)) * ↑(#(B.sup id)) ≤ ↑(#A) * ↑(#x) * ((↑m + 1) / ↑m) * (↑(#B) * ↑(#y) * ((↑m + 1) / ↑m))

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(A.sup id)) * ↑(#(B.sup id)) ≤ ↑(#A) * ↑(#x) * ((↑m + 1) / ↑m) * (↑(#B) * ↑(#y) * ((↑m + 1) / ↑m))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ (p.IsTrail ∧ q.IsTrail ∧ p.edges.Disjoint q.edges) ∧ p.append q ≠ Walk.nil ∧ (p.append q).support.tail.Nodup

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ (p.IsTrail ∧ q.IsTrail ∧ p.edges.Disjoint q.edges) ∧ p.append q ≠ Walk.nil ∧ (p.append q).support.tail.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case neg
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
h : ¬Infinite ι
this : Fintype ι
hc : n ≤ Fintype.card ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n

Tactic:
]

Goal state after:
case neg
n : ℕ
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
h : ¬Infinite ι
this : Fintype ι
hc : n ≤ Fintype.card ι
⊢ ¬(completeMultipartiteGraph V).CliqueFree n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : 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) (φ b) ↔ (completeGraph (Fin n)).Adj a b
⊢ completeGraph (Fin n) ⊑ G

Tactic:
]

Goal state after:
α : 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) (φ b) ↔ (completeGraph (Fin n)).Adj a b
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case refine_3
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail

Tactic:
]

Goal state after:
case refine_3
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
h : completeGraph (Fin n) ⊑ G
hy : φ y = s
e : x = y
⊢ completeGraph (Fin n) ⊑ G

Tactic:
]

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
h : completeGraph (Fin n) ⊑ G
hy : φ y = s
e : x = y
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(A.sup id)) * ↑(#(B.sup id)) ≤ (1 + ε ^ 5 / 49) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y)))

Tactic:
refine le_trans ?_ (mul_le_mul_of_nonneg_right (m_add_one_div_m_le_one_add hPα hPε hε₁) ?_)
      · rw [sq, mul_mul_mul_comm, mul_comm (_ / (m : ℝ)), mul_comm (_ / (m : ℝ))]
        gcongr
        exacts [sum_card_subset_chunk_parts_le (by sz_positivity) hA hx,
          sum_card_subset_chunk_parts_le (by sz_positivity) hB hy]
      · exact_mod_cast _root_.zero_le

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ (if a = x then if b = x then G.Adj s s else G.Adj s (φ b) else if b = x then G.Adj (φ a) s else G.Adj (φ a) (φ b)) ↔
    (completeGraph (Fin n)).Adj a b

Tactic:
]

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ :
  ∀ {a b : Fin n},
    { Adj := fun v w ↦ if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w,
            symm := ⋯, loopless := ⋯ }.Adj
        (φ a) (φ b) ↔
      (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
ms : s ∉ Set.range ⇑φ
a b : Fin n
⊢ (if a = x then if b = x then G.Adj s s else G.Adj s (φ b) else if b = x then G.Adj (φ a) s else G.Adj (φ a) (φ b)) ↔
    (completeGraph (Fin n)).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < #(A.sup id) * #(B.sup id)

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < #(A.sup id) * #(B.sup id)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case ha
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ∃ x ∈ A, (id x).Nonempty

Tactic:
]

Goal state after:
case ha
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ∃ x ∈ A, (id x).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset * 1

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
⊢ #(G.cliqueFinset 3) * 3 ≤ #G.edgeFinset * 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case right
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
⊢ G.IsNClique n (t.erase y) ∧ G.IsNClique n (t.erase x)

Tactic:
]

Goal state after:
case right
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
⊢ G.IsNClique n (t.erase y) ∧ G.IsNClique n (t.erase x)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
this : #{s(a, b), s(a, c), s(b, c)} = 3
⊢ #{s(a, b), s(a, c), s(b, c)} ≤ #(bipartiteAbove (fun s e ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.EdgeDisjointTriangles
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
this : #{s(a, b), s(a, c), s(b, c)} = 3
⊢ #{s(a, b), s(a, c), s(b, c)} ≤ #(bipartiteAbove (fun s e ↦ ∀ a ∈ e, a ∈ s) G.edgeFinset {a, b, c})
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
n : ℕ
h : ∀ (t : Finset ↑s), ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) t)
t : Finset α
ht : ↑t ⊆ s
this : ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) (Finset.subtype (fun x ↦ x ∈ s) t))
⊢ ¬G.IsNClique n (map (Embedding.subtype (Membership.mem s)) (Finset.subtype (Membership.mem s) t))

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
n : ℕ
h : ∀ (t : Finset ↑s), ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) t)
t : Finset α
ht : ↑t ⊆ s
this : ¬G.IsNClique n (map (Embedding.subtype fun x ↦ x ∈ s) (Finset.subtype (fun x ↦ x ∈ s) t))
⊢ ¬G.IsNClique n (map (Embedding.subtype (Membership.mem s)) (Finset.subtype (Membership.mem s) t))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
⊢ s = s

pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
⊢ ∀ x ∈ s, x ∈ Set.range ⇑f

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
⊢ ∀ x ∈ s, x ∈ Set.range ⇑f
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ #s = #s

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ G.IsClique (⇑f ⁻¹' ↑s)

Tactic:
]

Goal state after:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : (SimpleGraph.map (⇑f) G).IsClique ↑s
hn : #s ≠ 1
hs' : map f (s.preimage ⇑f ⋯) = s
⊢ G.IsClique (⇑f ⁻¹' ↑s)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #G.edgeFinset * 1 ≤ #(G.cliqueFinset 3) * 3

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #G.edgeFinset * 1 ≤ #(G.cliqueFinset 3) * 3
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case hb
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ∃ x ∈ B, (id x).Nonempty

Tactic:
]

Goal state after:
case hb
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ∃ x ∈ B, (id x).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ p'.support ++ q'.support.reverse.tail <+ p.support ++ q.support.reverse.tail

Tactic:
]

Goal state after:
case right
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ p'.support ++ q'.support.reverse.tail <+ p.support ++ q.support.reverse.tail
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ 1 + 1 = 2

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case h
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
this : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique ↑s ∧ #s = y
⊢ y ≤ Fintype.card α

Tactic:
]

Goal state after:
case h
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
this : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique ↑s ∧ #s = y
⊢ y ≤ Fintype.card α
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case h
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
this : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique ↑s ∧ #s = y
⊢ #s ≤ Fintype.card α

Tactic:
]

Goal state after:
case h
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
this : Fintype α
y : ℕ
s : Finset α
syc : G.IsClique ↑s ∧ #s = y
⊢ #s ≤ Fintype.card α
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Set α
t' : Finset ↑s
tc : G.IsNClique (induce s G).cliqueNum (map (Embedding.subtype fun x ↦ x ∈ s) t')
⊢ (induce s G).cliqueNum ≤ G.cliqueNum

Tactic:
]

Goal state after:
α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Set α
t' : Finset ↑s
tc : G.IsNClique (induce s G).cliqueNum (map (Embedding.subtype fun x ↦ x ∈ s) t')
⊢ (induce s G).cliqueNum ≤ G.cliqueNum
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
⊢ #(G.cliqueFinset n) ≤ #(powersetCard n univ)

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
⊢ #(G.cliqueFinset n) ≤ #(powersetCard n univ)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise Gᶜ.Adj ↔ s.Pairwise fun v w ↦ ¬G.Adj v w

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise Gᶜ.Adj ↔ s.Pairwise fun v w ↦ ¬G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ s.Pairwise fun v w ↦ ¬G.Adj v w

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ s.Pairwise fun v w ↦ ¬G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬G.Adj x y

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (s.Pairwise fun v w ↦ ¬Gᶜ.Adj v w) ↔ s.Pairwise G.Adj

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (s.Pairwise fun v w ↦ ¬Gᶜ.Adj v w) ↔ s.Pairwise G.Adj
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ s.Pairwise G.Adj

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ s.Pairwise G.Adj