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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ some (p.getVert 0) = some (p.getVert (p.support.length - 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x✝ : Sym2 V
⊢ x✝ ∈ p.reverse.edgeSet ↔ x✝ ∈ p.edgeSet

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
x✝ : Sym2 V
⊢ x✝ ∈ (p.append q).edgeSet ↔ x✝ ∈ p.edgeSet ∪ q.edgeSet

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ c.rotate u h = nil ↔ c = nil

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
x✝ : Sym2 V
⊢ x✝ ∈ (p.copy hu hv).edgeSet ↔ x✝ ∈ p.edgeSet

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.nil
V : Type u
G : SimpleGraph V
u : V
⊢ (nil.append nil).Nil ↔ nil.Nil ∧ nil.Nil

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.cons
V : Type u
G : SimpleGraph V
u w v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ w
⊢ (nil.append (cons h✝ p✝)).Nil ↔ nil.Nil ∧ (cons h✝ p✝).Nil

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).append nil).Nil ↔ (cons h✝ p✝).Nil ∧ nil.Nil

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons.cons
V : Type u
G : SimpleGraph V
u v w v✝¹ : V
h✝¹ : G.Adj u v✝¹
p✝¹ : G.Walk v✝¹ v
v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ ((cons h✝¹ p✝¹).append (cons h✝ p✝)).Nil ↔ (cons h✝¹ p✝¹).Nil ∧ (cons h✝ p✝).Nil

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
⊢ nil.reverse.Nil ↔ nil.Nil

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ (cons h✝ p✝).reverse.Nil ↔ (cons h✝ p✝).Nil

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
w✝ : ℕ
hn : w✝ + 1 ≠ 0
⊢ (p.drop w✝).support = ((p.drop (w✝ + 1 - 1)).copy ⋯ ⋯).support

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ edges ⊆ G.edgeFinset

Tactic:
intro e h

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h✝ : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case isTrail
V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.IsTrail

Tactic:
simp

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

Goal state before:
pp: case support_nodup
V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.support.Nodup

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.IsPath

Tactic:
constructor <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.IsPath ↔ p = nil

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p = p.reverse.reverse

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
hp : Walk.nil.IsPath
⊢ Walk.nil.tail.IsPath

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
⊢ ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
have := Fintype.ofFinite G.edgeSet

Goal state after:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
this : Fintype ↑G.edgeSet
⊢ ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
⊢ nil.IsTrail ∧ nil.length = 0

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
⊢ ∃ u v p, ∃ (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length

Tactic:
have := Fintype.ofFinite G.edgeSet

Goal state after:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
this : Fintype ↑G.edgeSet
⊢ ∃ u v p, ∃ (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsPath ∧ p.length = n}
this : s.Finite
x : V
⊢ nil.IsPath ∧ nil.length = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
hp : ¬p.Nil
⊢ ∀ {u_1 v w : V} (h : G.Adj u_1 v) (q : G.Walk v w) (x : G.Adj u u_1),
    (cons x (cons h q)).dropLast = cons x ((cons h q).dropLast.copy ⋯ ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ w t u v : V
p : G.Walk u v
h : G.Adj v t
⊢ v = (p.concat h).penultimate

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.tail.length = nil.length - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).tail.length = (cons h✝ p✝).length - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ nil.tail.reverse = nil.reverse.dropLast.copy ⋯ ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ nil.dropLast.reverse = nil.reverse.tail.copy ⋯ ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ nil.tail.getVert n = nil.getVert (n + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).tail.getVert n = (cons h✝ p✝).getVert (n + 1)

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Set.InjOn Walk.nil.getVert {i | i ≤ Walk.nil.length} → Walk.nil.IsPath

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.IsClique ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
⊢ G.IsClique {a}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ 3 ≠ 1

Tactic:
simp

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : V
hu : u ∈ {w | w ∈ p.support}
v : V
hv : v ∈ {w | w ∈ p.support}
⊢ f u = f v → u = v

Tactic:
hf

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : V
hu : u ∈ {w | w ∈ p.support}
v : V
hv : v ∈ {w | w ∈ p.support}
hf : f u = f v
⊢ u = v
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.IsClique ↑∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
⊢ G.IsClique ↑{a}

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
simp

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ p.length - 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
simp

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
h : p.snd = p.penultimate
this : 3 ≤ p.length
⊢ 1 ≤ p.length - 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
⊢ ↑(s.erase a) ⊆ ↑s

Tactic:
simp

Goal state after:
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
⊢ ↑(#(interedges G.Adj x y)) / (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))) ≤
    ↑(#(interedges G.Adj x y)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))

Tactic:
div_le_iff₀,

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
⊢ ↑(#(interedges G.Adj x y)) ≤
    ↑(#(interedges G.Adj x y)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id)))) *
      (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y)))

α : 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) * ↑(#x) * (↑(#B) * ↑(#y))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : v ∈ c.support
⊢ (c.takeUntil v h).IsPath

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
hp : p.IsPath
hw : w ∈ p.support
h : v ≠ w
n : ℕ
hn : p.getVert n = v
hnl : n ≤ (p.takeUntil w hw).length
this : (p.takeUntil w hw).length < p.length
⊢ p.length ∈ {i | i ≤ p.length}

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : Walk.nil.IsTrail
h : ∀ (v : V) (w : G.Walk v v), w.IsSubwalk Walk.nil → ¬w.IsCycle
⊢ Walk.nil.IsPath

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : SimpleGraph α
m n : ℕ
s : Finset α
ι : Type u_3
V : ι → Type u_4
f : (i : ι) → V i
⊢ ∀ {a b : ι},
    (completeMultipartiteGraph V).Adj ({ toFun := fun i ↦ ⟨i, f i⟩, inj' := ⋯ } a)
        ({ toFun := fun i ↦ ⟨i, f i⟩, inj' := ⋯ } b) ↔
      ⊤.Adj a b

Tactic:
simp

Goal state after:
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
⊢ 3 * #(G.cliqueFinset 3) ≤ #G.edgeFinset

Tactic:
rw [mul_comm, ← mul_one #G.edgeFinset]

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 refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ False

Tactic:
refine h hst.1 hst.2 hab (ht ?_ ?_ hab)

Goal state after:
case refine_2.refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ a ∈ ↑{a, b}

case refine_2.refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ b ∈ ↑{a, b}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ a ∈ ↑{a, b}

Tactic:
simp

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

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique ↑{a, b}
hst : a ∈ s ∧ b ∈ s
⊢ b ∈ ↑{a, b}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s ∈ G.cliqueSet 0 ↔ s ∈ {∅}

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
h : BddAbove {n | ∃ s, G.IsNClique n s}
⊢ 0 ∈ {n | ∃ s, G.IsNClique n s}

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
⊢ ∃ s, G.IsMaximumClique s

Tactic:
by
  obtain ⟨s, snc⟩ := G.exists_isNClique_cliqueNum
  exact ⟨s, ⟨snc.isClique, fun t ht => snc.card_eq.symm ▸ ht.card_le_cliqueNum⟩⟩

Goal state after:
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:
· exact ⟨_, hy, nonempty_of_mem_parts _ (hB hy)⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
v' : V
hvv' : G.Adj v v'
w : G.Walk v' v
hw : (cons hvv' w).IsCircuit
⊢ cons hvv' w.bypass ≠ nil

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNClique n s ↔ G.IsIndepSet ↑s ∧ #s = n

Tactic:
simp [isNClique_iff]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_1
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h : ∀ (x_1 y_1 : α), x_1 ∈ {x, y, z} → y_1 ∈ {x, y, z} → x_1 ≠ y_1 → G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ x ∈ {x, y, z}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h : ∀ (x_1 y_1 : α), x_1 ∈ {x, y, z} → y_1 ∈ {x, y, z} → x_1 ≠ y_1 → G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ y ∈ {x, y, z}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_3
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h : ∀ (x_1 y_1 : α), x_1 ∈ {x, y, z} → y_1 ∈ {x, y, z} → x_1 ≠ y_1 → G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ x ∈ {x, y, z}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_4
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h : ∀ (x_1 y_1 : α), x_1 ∈ {x, y, z} → y_1 ∈ {x, y, z} → x_1 ≠ y_1 → G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ z ∈ {x, y, z}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_5
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h : ∀ (x_1 y_1 : α), x_1 ∈ {x, y, z} → y_1 ∈ {x, y, z} → x_1 ≠ y_1 → G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ y ∈ {x, y, z}

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_6
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h : ∀ (x_1 y_1 : α), x_1 ∈ {x, y, z} → y_1 ∈ {x, y, z} → x_1 ≠ y_1 → G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ z ∈ {x, y, z}

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u✝ : V
hp : ∀ e ∈ Walk.nil.edges, e ∈ H.edgeSet
pp : Walk.nil.IsPath
⊢ (Walk.nil.transfer H hp).IsPath

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
⊢ 1 ≤ 2

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: ε : ℝ
hε : ε ≤ 0
⊢ min (2 * ↑0 ^ 3)⁻¹ ((1 - min 1 ε / 4) * (ε / (16 * ↑(bound (ε / 8) 0))) ^ 3) ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: ε : ℝ
hε : ε ≤ 0
⊢ 0 ≤ 4

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hε : G.FarFromTriangleFree ε
⊢ ⊥.CliqueFree 3

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case right
α : 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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) ≤
    ε ^ 5 / 49

Tactic:
suffices (G.edgeDensity (A.biUnion id) (B.biUnion id) : ℝ) -
      (∑ ab ∈ A.product B, (G.edgeDensity ab.1 ab.2 : ℝ)) / (#A * #B) ≤ ε ^ 5 / 50 by
    apply this.trans
    gcongr <;> [sz_positivity; norm_num]

Goal state after:
case right
α : 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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) ≤
    ε ^ 5 / 50