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

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

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.support = u :: nil.support.tail

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✝).support = u :: (cons h✝ p✝).support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ p.support

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ u ∈ nil.support

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ u ∈ (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u w : V
⊢ w ∈ nil.support ↔ w = u ∨ w ∈ nil.support.tail

case cons
V : Type u
G : SimpleGraph V
u v w v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ w ∈ (cons h✝ p✝).support ↔ w = u ∨ w ∈ (cons h✝ p✝).support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ ↑p.support = {u} + ↑p.support.tail

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ ↑nil.support = {u} + ↑nil.support.tail

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✝).support = {u} + ↑(cons h✝ p✝).support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support[0] = u

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.support[0] = u

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✝).support[0] = u
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).Nil ↔ p.Nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
⊢ (Walk.map f nil).Nil ↔ nil.Nil

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (Walk.map f (cons h✝ p✝)).Nil ↔ (cons h✝ p✝).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
⊢ Walk.map f p = nil ↔ p = nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
⊢ Walk.map f nil = nil ↔ nil = nil

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ u
⊢ Walk.map f (cons h✝ p✝) = nil ↔ cons h✝ p✝ = nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.Nil ↔ p.support = [v]

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
⊢ nil.Nil ↔ nil.support = [v]

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✝).Nil ↔ (cons h✝ p✝).support = [v]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.darts = [] ↔ p.Nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
⊢ nil.darts = [] ↔ nil.Nil

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✝).darts = [] ↔ (cons h✝ p✝).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.edges = [] ↔ p.Nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
⊢ nil.edges = [] ↔ nil.Nil

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✝).edges = [] ↔ (cons h✝ p✝).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.length = 0 ↔ p.Nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.length = 0 ↔ nil.Nil

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✝).length = 0 ↔ (cons h✝ p✝).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ ¬p.Nil ↔ 0 < p.length

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
⊢ ¬nil.Nil ↔ 0 < nil.length

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✝).Nil ↔ 0 < (cons h✝ p✝).length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ ¬p.Nil ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, p = cons h q

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
⊢ ¬nil.Nil ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, nil = cons h q

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✝).Nil ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, cons h✝ p✝ = cons h q
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ ¬p.Nil ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, p = cons h q

Tactic:
cases p <;> simp [*]

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

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

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
⊢ nil = nil ↔ nil.Nil

case cons
V : Type u
G : SimpleGraph V
v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
⊢ cons h✝ p✝ = nil ↔ (cons h✝ p✝).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ¬p.Nil → (w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e)
hnil : ¬(cons h p).Nil
⊢ w ∈ (cons h p).support ↔ ∃ e ∈ (cons h p).edges, w ∈ e

Tactic:
cases p

Goal state after:
case cons.nil
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h : G.Adj u✝ v✝
ih : ¬nil.Nil → (w ∈ nil.support ↔ ∃ e ∈ nil.edges, w ∈ e)
hnil : ¬(cons h nil).Nil
⊢ w ∈ (cons h nil).support ↔ ∃ e ∈ (cons h nil).edges, w ∈ e

case cons.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝¹ w✝ : V
h : G.Adj u✝ v✝¹
v✝ : V
h✝ : G.Adj v✝¹ v✝
p✝ : G.Walk v✝ w✝
ih : ¬(cons h✝ p✝).Nil → (w ∈ (cons h✝ p✝).support ↔ ∃ e ∈ (cons h✝ p✝).edges, w ∈ e)
hnil : ¬(cons h (cons h✝ p✝)).Nil
⊢ w ∈ (cons h (cons h✝ p✝)).support ↔ ∃ e ∈ (cons h (cons h✝ p✝)).edges, w ∈ e
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∀ e ∈ p.reverse.edges, e ∈ H.edgeSet

Tactic:
by simp only [edges_reverse, List.mem_reverse]; exact hp

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
p : G.Walk u v
⊢ p.takeUntil u ⋯ = nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
⊢ nil.takeUntil v ⋯ = nil

case cons
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).takeUntil u ⋯ = nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
⊢ p.concat h ≠ nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
h : G.Adj u u
⊢ nil.concat h ≠ nil

case cons
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj v u
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).concat h ≠ nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case succ
V : Type u_1
G : SimpleGraph V
u v : V
n k✝ : ℕ
p : G.Walk u v
k : ℕ
h : n ≤ k
ih : (p.take n).IsSubwalk (p.take k)
⊢ (p.take k).IsSubwalk (p.take (k + 1))

Tactic:
cases p

Goal state after:
case succ.nil
V : Type u_1
G : SimpleGraph V
u : V
n k✝ k : ℕ
h : n ≤ k
ih : (nil.take n).IsSubwalk (nil.take k)
⊢ (nil.take k).IsSubwalk (nil.take (k + 1))

case succ.cons
V : Type u_1
G : SimpleGraph V
u v : V
n k✝ k : ℕ
h : n ≤ k
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
ih : ((cons h✝ p✝).take n).IsSubwalk ((cons h✝ p✝).take k)
⊢ ((cons h✝ p✝).take k).IsSubwalk ((cons h✝ p✝).take (k + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case succ
V : Type u_1
G : SimpleGraph V
v : V
n k n✝ : ℕ
ih : ∀ {u : V} (p : G.Walk u v), (p.drop (n✝ + 1)).IsSubwalk (p.drop n✝)
u : V
p : G.Walk u v
⊢ (p.drop (n✝ + 1 + 1)).IsSubwalk (p.drop (n✝ + 1))

Tactic:
cases p

Goal state after:
case succ.nil
V : Type u_1
G : SimpleGraph V
v : V
n k n✝ : ℕ
ih : ∀ {u : V} (p : G.Walk u v), (p.drop (n✝ + 1)).IsSubwalk (p.drop n✝)
⊢ (nil.drop (n✝ + 1 + 1)).IsSubwalk (nil.drop (n✝ + 1))

case succ.cons
V : Type u_1
G : SimpleGraph V
v : V
n k n✝ : ℕ
ih : ∀ {u : V} (p : G.Walk u v), (p.drop (n✝ + 1)).IsSubwalk (p.drop n✝)
u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).drop (n✝ + 1 + 1)).IsSubwalk ((cons h✝ p✝).drop (n✝ + 1))
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
⊢ (p.append q).Nil ↔ p.Nil ∧ q.Nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u w : V
q : G.Walk u w
⊢ (nil.append q).Nil ↔ nil.Nil ∧ q.Nil

case cons
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk v w
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).append q).Nil ↔ (cons h✝ p✝).Nil ∧ q.Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.reverse.Nil ↔ p.Nil

Tactic:
cases p

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

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
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.take 0 = nil.copy ⋯ ⋯

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.take 0 = nil.copy ⋯ ⋯

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✝).take 0 = nil.copy ⋯ ⋯
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:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.IsPath ↔ nil.Nil

case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ u
⊢ (cons h✝ p✝).IsPath ↔ (cons h✝ p✝).Nil
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 : ℕ
⊢ (p.take n).Nil ↔ p.Nil ∨ n = 0

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ (nil.take n).Nil ↔ nil.Nil ∨ n = 0

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✝).take n).Nil ↔ (cons h✝ p✝).Nil ∨ n = 0
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case zero
V : Type u
G : SimpleGraph V
v u : V
p : G.Walk u v
h : p.length ≤ 0
⊢ p.take 0 = p.copy ⋯ ⋯

Tactic:
cases p

Goal state after:
case zero.nil
V : Type u
G : SimpleGraph V
v : V
h : nil.length ≤ 0
⊢ nil.take 0 = nil.copy ⋯ ⋯

case zero.cons
V : Type u
G : SimpleGraph V
v u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : (cons h✝ p✝).length ≤ 0
⊢ (cons h✝ p✝).take 0 = (cons h✝ p✝).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case succ
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
p : G.Walk u v
h : p.length ≤ n + 1
⊢ p.take (n + 1) = p.copy ⋯ ⋯

Tactic:
cases p

Goal state after:
case succ.nil
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 ⋯ ⋯
h : nil.length ≤ n + 1
⊢ nil.take (n + 1) = nil.copy ⋯ ⋯

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 ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.reverse.penultimate = nil.snd

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✝).reverse.penultimate = (cons h✝ p✝).snd
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.drop 0 = p.copy ⋯ ⋯

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.drop 0 = nil.copy ⋯ ⋯

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✝).drop 0 = (cons h✝ p✝).copy ⋯ ⋯
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
⊢ 0 < ↑(#A)

Tactic:
cast_pos,

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
⊢ 0 < #A
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
⊢ 0 < ↑(#x)

Tactic:
cast_pos,

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
⊢ 0 < #x
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
⊢ 0 < ↑(#B)

Tactic:
cast_pos,

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
⊢ 0 < #B
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
⊢ (cons h p).tail = p.copy ⋯ ⋯

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).tail = nil.copy ⋯ ⋯

case cons
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ (cons h (cons h✝ p✝)).tail = (cons h✝ p✝).copy ⋯ ⋯
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
⊢ 0 < ↑(#y)

Tactic:
cast_pos,

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
⊢ 0 < #y
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
⊢ cons ⋯ p.tail = p

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
hp : ¬nil.Nil
⊢ cons ⋯ nil.tail = nil

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
hp : ¬(cons h✝ p✝).Nil
⊢ cons ⋯ (cons h✝ p✝).tail = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.tail.length = p.length - 1

Tactic:
cases p

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

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
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.dropLast.length = p.length - 1

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.dropLast.length = nil.length - 1

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✝).dropLast.length = (cons h✝ p✝).length - 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
⊢ p.tail.Nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
hp : Walk.nil.Nil
⊢ Walk.nil.tail.Nil

case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).Nil
⊢ (cons h✝ p✝).tail.Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.Nil
⊢ p.dropLast.Nil

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
hp : Walk.nil.Nil
⊢ Walk.nil.dropLast.Nil

case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).Nil
⊢ (cons h✝ p✝).dropLast.Nil
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
⊢ p.getVert i = u ↔ i = 0

Tactic:
cases p

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
i : ℕ
hp : Walk.nil.IsPath
hi : i ≤ Walk.nil.length
⊢ Walk.nil.getVert i = u ↔ i = 0

case cons
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).IsPath
hi : i ≤ (cons h✝ p✝).length
⊢ (cons h✝ p✝).getVert i = u ↔ i = 0
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
⊢ p.tail.getVert n = p.getVert (n + 1)

Tactic:
cases p

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

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)
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
⊢ 0 < ↑(#A)

Tactic:
cast_pos,

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
⊢ 0 < #A