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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ m + 1 ≤ q.length + 1

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ m + 1 ≤ q.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.support[k]? = none
ht : q.support[k]? = none
⊢ p.support[k]? = q.support[k]?

Tactic:
]

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.support[k]? = none
ht : q.support[k]? = none
⊢ p.support[k]? = q.support[k]?
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.support[k]? = none
ht : q.support[k]? = none
⊢ none = none

Tactic:
]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique s ∧ ⇑f '' s = ↑t) → ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
]

Goal state after:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique s ∧ ⇑f '' s = ↑t) → ∃ s, G.IsClique ↑s ∧ map f s = t
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ q.length + 1

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ q.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ↔ ¬1 < #t ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ t.Nontrivial

Tactic:
]

Goal state after:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ↔ ¬1 < #t ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : 1 < #t
⊢ t.Nontrivial
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ (cons h p).support ~ (cons h p).support

Tactic:
]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ q.getVert (n + 1 - 1) = u✝

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ q.getVert (n + 1 - 1) = u✝
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (G.cliqueSet 3).Pairwise (Function.onFun (fun x y ↦ (↑x ∩ ↑y).Subsingleton) (Finset.map f))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (G.cliqueSet 3).Pairwise (Function.onFun (fun x y ↦ (↑x ∩ ↑y).Subsingleton) (Finset.map f))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (⇑f '' (↑s ∩ ↑t)).Subsingleton

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ (⇑f '' (↑s ∩ ↑t)).Subsingleton
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ (SimpleGraph.map (⇑e.toEmbedding) (SimpleGraph.comap (⇑e.toEmbedding) G)).LocallyLinear

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ (SimpleGraph.map (⇑e.toEmbedding) (SimpleGraph.comap (⇑e.toEmbedding) G)).LocallyLinear
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.map (⇑e.symm.toEmbedding) G).LocallyLinear

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.map (⇑e.symm.toEmbedding) G).LocallyLinear
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
⊢ w = p.snd

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
⊢ w = p.snd
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : f.topEmbedding w✝¹ ≠ f.topEmbedding w✝
⊢ G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : f.topEmbedding w✝¹ ≠ f.topEmbedding w✝
⊢ G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)
⊢ G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)
⊢ G.Adj (f.topEmbedding w✝¹) (f.topEmbedding w✝)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
⊢ Set.InjOn p.getVert {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
⊢ Set.InjOn p.getVert {i | 1 ≤ i ∧ i ≤ p.length}
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
⊢ (SimpleGraph.map (⇑f) G).IsClique (⇑f '' ↑s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
⊢ (SimpleGraph.map (⇑f) G).IsClique (⇑f '' ↑s)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ n = m

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : 1 ≤ n ∧ n ≤ p.tail.length + 1
m : ℕ
hm : 1 ≤ m ∧ m ≤ p.tail.length + 1
hnm : p.getVert n = p.getVert m
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n ↔ ∃ s, G.IsNClique n s ∧ map f s = t

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n ↔ ∃ s, G.IsNClique n s ∧ map f s = t
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ (↑s).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n

Tactic:
]

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
⊢ (↑s).Subsingleton ∧ #s = n ↔ n ≤ 1 ∧ #s = n
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case card_eq
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ n + 1 = n + 1

Tactic:
]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u → ¬i = 0 → i = p.length

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u → ¬i = 0 → i = p.length
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
⊢ n - 1 = n - 1

Tactic:
]

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : i - 1 = 0 ∨ i - 1 = p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ False

Tactic:
]

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : i - 1 = 0 ∨ i - 1 = p.length
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
hc : ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
hc : ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.IsNClique 3 s

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.IsNClique 3 s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
hc : ((p.takeUntil u h).append (p.dropUntil u h)).IsPath
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsPath

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
hc : ((p.takeUntil u h).append (p.dropUntil u h)).IsPath
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsPath
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)) ≤
    ↑(#(interedges G.Adj x y)) *
      ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))))

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) * ↑(#x) * (↑(#B) * ↑(#y))

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
⊢ ↑(#(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: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
⊢ c.edges.Nodup ↔ c.edges.Nodup

Tactic:
]

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
h : w ∈ c.support
hc : ((c.dropUntil w h).reverse.append (c.takeUntil w h).reverse).IsCycle
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath

Tactic:
]

Goal state after:
case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
h : w ∈ c.support
hc : ((c.dropUntil w h).reverse.append (c.takeUntil w h).reverse).IsCycle
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath
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
hv : ∃ n, (p.takeUntil w hw).getVert n = v ∧ n ≤ (p.takeUntil w hw).length
⊢ False

Tactic:
]

Goal state after:
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
hv : ∃ n, (p.takeUntil w hw).getVert n = v ∧ n ≤ (p.takeUntil w hw).length
⊢ False
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
⊢ False

Tactic:
]

Goal state after:
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
⊢ False
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
⊢ n ≤ p.length

Tactic:
]

Goal state after:
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
⊢ n ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsClique ↑s ∧ #s = n
⊢ G.IsClique ↑(map { toFun := Subtype.val, inj' := ⋯ } s) ∧ #(map { toFun := Subtype.val, inj' := ⋯ } s) = n

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsClique ↑s ∧ #s = n
⊢ G.IsClique ↑(map { toFun := Subtype.val, inj' := ⋯ } s) ∧ #(map { toFun := Subtype.val, inj' := ⋯ } s) = n
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)))

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
⊢ ↑(#(A.sup id)) * ↑(#(B.sup id)) ≤ (1 + ε ^ 5 / 49) * (↑(#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.sup id)) * ↑(#(B.sup id))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
⊢ G.EdgeDisjointTriangles → ∀ (x y : α), ¬s(x, y).IsDiag → {s | s ∈ G.cliqueSet 3 ∧ s(x, y) ∈ s.sym2}.Subsingleton

Tactic:
]

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
⊢ G.EdgeDisjointTriangles → ∀ (x y : α), ¬s(x, y).IsDiag → {s | s ∈ G.cliqueSet 3 ∧ s(x, y) ∈ s.sym2}.Subsingleton
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
v w : α
s : Finset α
n : ℕ
hc : (G ⊔ edge v w).IsNClique n s
hx : v ∈ s
⊢ n - 1 = n - 1

Tactic:
]

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ u :: (p.takeUntil u hup).support <:+: u :: p.support

Tactic:
]

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ u :: (p.takeUntil u hup).support <:+: u :: p.support
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬a = b
⊢ {s | G.Adj (a, b).1 (a, b).2 ∧ ∃ c, G.Adj (a, b).1 c ∧ G.Adj (a, b).2 c ∧ s = {(a, b).1, (a, b).2, c}}.Subsingleton

Tactic:
]

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α),
    a ≠ b → {s | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬a = b
⊢ {s | G.Adj (a, b).1 (a, b).2 ∧ ∃ c, G.Adj (a, b).1 c ∧ G.Adj (a, b).2 c ∧ s = {(a, b).1, (a, b).2, c}}.Subsingleton
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝ : Fintype β
f : ⊤.Copy G
⊢ G.IsClique (Set.range ⇑f.toEmbedding) ∧ Fintype.card β = Fintype.card β

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝ : Fintype β
f : ⊤.Copy G
⊢ G.IsClique (Set.range ⇑f.toEmbedding) ∧ Fintype.card β = Fintype.card β