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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).reverse.IsPath
⊢ q.reverse.IsPath

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).reverse.IsPath
⊢ q.reverse.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (q.reverse.append p.reverse).IsPath
⊢ q.reverse.IsPath

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (q.reverse.append p.reverse).IsPath
⊢ q.reverse.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
w✝¹ : G.Walk v' v
w✝ : G.Walk w w'
h₂ : ((w✝¹.append p₁).append w✝).IsTrail
h : p₂ = (w✝¹.append p₁).append w✝
⊢ p₁.IsTrail

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
w✝¹ : G.Walk v' v
w✝ : G.Walk w w'
h₂ : ((w✝¹.append p₁).append w✝).IsTrail
h : p₂ = (w✝¹.append p₁).append w✝
⊢ p₁.IsTrail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
w✝¹ : G.Walk v' v
w✝ : G.Walk w w'
h₂ : ((w✝¹.append p₁).append w✝).IsPath
h : p₂ = (w✝¹.append p₁).append w✝
⊢ p₁.IsPath

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
w✝¹ : G.Walk v' v
w✝ : G.Walk w w'
h₂ : ((w✝¹.append p₁).append w✝).IsPath
h : p₂ = (w✝¹.append p₁).append w✝
⊢ p₁.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (cons ⋯ p.reverse).IsPath ↔ p.reverse.IsPath ∧ w ∉ p.reverse.support

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (cons ⋯ p.reverse).IsPath ↔ p.reverse.IsPath ∧ w ∉ p.reverse.support
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_2
α : 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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#A) * ↑(#x) * (↑m / (↑m + 1)) * (↑(#B) * ↑(#y) * (↑m / (↑m + 1))) ≤ ↑(#(A.sup id)) * ↑(#(B.sup id))

Tactic:
]

Goal state after:
case refine_2
α : 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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#A) * ↑(#x) * (↑m / (↑m + 1)) * (↑(#B) * ↑(#y) * (↑m / (↑m + 1))) ≤ ↑(#(A.sup id)) * ↑(#(B.sup id))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.tail.support

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.tail.support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.support.tail

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
hpq' : (p.support ++ q.support.tail).Nodup
⊢ p.support.Disjoint q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.support.tail

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x = v ∨ x ∈ q.support.tail
hq : ¬q.Nil
⊢ x ∈ q.support.tail

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x = v ∨ x ∈ q.support.tail
hq : ¬q.Nil
⊢ x ∈ q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ (p.take n).append ((p.drop n).take m) ≍ ((p.take n).append ((p.drop n).take m)).copy ⋯ ⋯

Tactic:
by simp [Walk.copy]

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
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ q.IsPath

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ q.IsPath
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
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ v ∉ q.support.tail ∧ 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
h : ¬p.Nil
hcyc : (p.append q).IsCycle
this : p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
⊢ v ∉ q.support.tail ∧ q.support.tail.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : 0 < n
h : (p.drop 1).IsPath
⊢ (((p.drop (Nat.succ 0)).drop (n - Nat.succ 0)).copy ⋯ ⋯).IsPath

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : 0 < n
h : (p.drop 1).IsPath
⊢ (((p.drop (Nat.succ 0)).drop (n - Nat.succ 0)).copy ⋯ ⋯).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : n < p.length
h : (p.take (p.length - 1)).IsPath
this : (p.take n).IsPath
⊢ (p.take n).IsPath

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : n < p.length
h : (p.take (p.length - 1)).IsPath
this : (p.take n).IsPath
⊢ (p.take n).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case succ.cons
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v✝ : V
h✝¹ : G.Adj u v✝
p✝ : G.Walk v✝ v
h✝ : (cons h✝¹ p✝).length ≤ n + 1
h : p✝.length ≤ n
⊢ (cons h✝¹ p✝).take (n + 1) = (cons h✝¹ p✝).copy ⋯ ⋯

Tactic:
]

Goal state after:
case succ.cons
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v✝ : V
h✝¹ : G.Adj u v✝
p✝ : G.Walk v✝ v
h✝ : (cons h✝¹ p✝).length ≤ n + 1
h : p✝.length ≤ n
⊢ (cons h✝¹ p✝).take (n + 1) = (cons h✝¹ p✝).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case succ.cons
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : (cons h✝ p✝).length ≤ n + 1
⊢ (cons h✝ p✝).take (n + 1) = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
rw [length_cons, Nat.add_le_add_iff_right] at h

Goal state after:
case succ.cons
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v✝ : V
h✝¹ : G.Adj u v✝
p✝ : G.Walk v✝ v
h✝ : (cons h✝¹ p✝).length ≤ n + 1
h : p✝.length ≤ n
⊢ (cons h✝¹ p✝).take (n + 1) = (cons h✝¹ p✝).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ u' v✝ w : V
p✝ : G.Walk u✝ v✝
f : G →g G'
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ Decidable p.support.Nodup

Tactic:
]

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ u' v✝ w : V
p✝ : G.Walk u✝ v✝
f : G →g G'
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ Decidable p.support.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.support.length ≤ Fintype.card V

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.support.length ≤ Fintype.card V
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
⊢ 0 = 0

Tactic:
]

Goal state after:
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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ A.Nonempty

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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ A.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_2
α : 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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ x.Nonempty

Tactic:
]

Goal state after:
case refine_2
α : 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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ x.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : p.length ≤ n
⊢ List.take (n + 1) p.support ++ [] = p.support

Tactic:
]

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : p.length ≤ n
⊢ List.take (n + 1) p.support ++ [] = p.support
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_3
α : 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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ B.Nonempty

Tactic:
]

Goal state after:
case refine_3
α : 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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ B.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_4
α : 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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ y.Nonempty

Tactic:
]

Goal state after:
case refine_4
α : 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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ y.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ p.support = p.support

Tactic:
]

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
hp : ¬p.Nil
⊢ p.dropLast.support ++ [v] = p.support

Tactic:
by
  rw [← support_concat _ <| adj_penultimate hp, concat_dropLast]

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
hp : ¬p.Nil
⊢ p.length = p.length

Tactic:
]

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✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons hadj p).tail.reverse.support = (cons hadj p).reverse.dropLast.support

Tactic:
]

Goal state after:
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
⊢ (cons hadj p).tail.reverse.support = (cons hadj p).reverse.dropLast.support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ i ≤ p.length

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ i ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ 0 ≤ p.length

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : p.getVert i = u
h' : i ≤ p.length
⊢ 0 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : w = u
h' : ¬i ≤ p.length
⊢ i = 0

Tactic:
]

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
h✝ : ¬p.Nil
h : w = u
h' : ¬i ≤ p.length
⊢ i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
⊢ p.length - i = 0 ↔ i = p.length

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
⊢ p.length - i = 0 ↔ i = p.length
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
⊢ ε ^ 5 / 49 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ ε ^ 5 / 49

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
⊢ ε ^ 5 / 49 * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ ε ^ 5 / 49
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
i : ℕ
x✝ : i + 1 ≠ 0
⊢ p.tail.getVert i ∈ p.tail.support

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
i : ℕ
x✝ : i + 1 ≠ 0
⊢ p.tail.getVert i ∈ p.tail.support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
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}
⊢ q.IsPath ∧ u✝ ∉ q.support

Tactic:
]

Goal state after:
case cons
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}
⊢ q.IsPath ∧ u✝ ∉ q.support
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ induce s G = ⊤ ↔ s.Pairwise G.Adj

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ induce s G = ⊤ ↔ s.Pairwise G.Adj
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inl
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 : k ≤ p.length
⊢ some (p.getVert k) = some (q.getVert k)

Tactic:
]

Goal state after:
case inl
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 : k ≤ p.length
⊢ some (p.getVert k) = some (q.getVert k)
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
⊢ 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}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ n + 1 ≤ q.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : u = x
hvy : v = y
⊢ G.Adj x y

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : u = x
hvy : v = y
⊢ G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : u = x
hvy : v = y
⊢ G.Adj u v

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
x : α
hx : f x ∈ t
y : α
hy : f y ∈ t
hne : x ≠ y
u v : α
huv : G.Adj u v
hux : u = x
hvy : v = y
⊢ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
⊢ t ⊆ Set.range ⇑f

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
⊢ t ⊆ Set.range ⇑f