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

Goal state before:
pp: case injective'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ Injective (⇑g.toHom ∘ ⇑f.toHom)

Tactic:
exact g.injective.comp f.injective

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

Goal state before:
pp: V : Type u_1
s t v w : V
⊢ (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w

Tactic:
edge,

Goal state after:
V : Type u_1
s t v w : V
⊢ (fromEdgeSet {s(s, t)}).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
s t : V
⊢ edge s t = edge t s

Tactic:
edge,

Goal state after:
V : Type u_1
s t : V
⊢ fromEdgeSet {s(s, t)} = edge t s
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
s t : V
⊢ fromEdgeSet {s(s, t)} = edge t s

Tactic:
edge,

Goal state after:
V : Type u_1
s t : V
⊢ fromEdgeSet {s(s, t)} = fromEdgeSet {s(t, s)}
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), edge u v = x} = ⨆ e ∈ G.edgeSet, fromEdgeSet {e}

Tactic:
edge,

Goal state after:
V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), fromEdgeSet {s(u, v)} = x} = ⨆ e ∈ G.edgeSet, fromEdgeSet {e}
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
⊢ { fst := u, snd := v✝, adj := h }.toProd.1 = u ∨ { fst := u, snd := v✝, adj := h }.toProd.1 ∈ p'.support

Tactic:
exact .inl rfl

Goal state after:
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
n : ℕ
⊢ (Walk.map f p).getVert n = f (p.getVert n)

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).getVert 0 = f (nil.getVert 0)

case nil.succ
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ : V
n✝ : ℕ
⊢ (Walk.map f nil).getVert (n✝ + 1) = f (nil.getVert (n✝ + 1))

case cons.zero
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (Walk.map f p✝).getVert n = f (p✝.getVert n)
⊢ (Walk.map f (cons h✝ p✝)).getVert 0 = f ((cons h✝ p✝).getVert 0)

case cons.succ
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (Walk.map f p✝).getVert n = f (p✝.getVert n)
n✝ : ℕ
⊢ (Walk.map f (cons h✝ p✝)).getVert (n✝ + 1) = f ((cons h✝ p✝).getVert (n✝ + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q, ∃ (h' : G.Adj x w✝), cons h p = q.concat h'
u : V
h : G.Adj u u✝
y : V
q : G.Walk u✝ y
h'' : G.Adj y w✝
hc : cons h' p = q.concat h''
⊢ ∃ x q, ∃ (h'_1 : G.Adj x w✝), cons h (cons h' p) = q.concat h'_1

Tactic:
exact ⟨y, cons h q, h'', hc ▸ concat_cons _ _ _ ▸ rfl⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
l✝ : List G.Dart
d₁ d₂ : G.Dart
l : List G.Dart
hne : d₁ :: d₂ :: l ≠ []
hchain : List.IsChain G.DartAdj (d₁ :: d₂ :: l)
⊢ (ofDarts (d₁ :: d₂ :: l) hne hchain).darts = d₁ :: d₂ :: l

Tactic:
simpa [hchain.rel.symm] using darts_ofDarts (l.cons_ne_nil d₂) hchain.of_cons

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.dropUntil u h).support.tail ++ (c.takeUntil u h).support.tail ~r c.support.tail

Tactic:
apply List.IsRotated.trans List.isRotated_append

Goal state after:
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.takeUntil u h).support.tail ++ (c.dropUntil u h).support.tail ~r c.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.dropUntil u h).darts ++ (c.takeUntil u h).darts ~r c.darts

Tactic:
apply List.IsRotated.trans List.isRotated_append

Goal state after:
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.takeUntil u h).darts ++ (c.dropUntil u h).darts ~r c.darts
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.drop n).length = p.length - n

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).length = nil.length - 0

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).length = nil.length - (n✝ + 1)

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).length = p✝.length - n
⊢ ((cons h✝ p✝).drop 0).length = (cons h✝ p✝).length - 0

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).length = p✝.length - n
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).length = (cons h✝ p✝).length - (n✝ + 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
n m : ℕ
⊢ (p.drop n).getVert m = p.getVert (n + m)

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
⊢ (nil.drop 0).getVert m = nil.getVert (0 + m)

case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).getVert m = nil.getVert (n✝ + 1 + m)

case cons.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).getVert m = p✝.getVert (n + m)
⊢ ((cons h✝ p✝).drop 0).getVert m = (cons h✝ p✝).getVert (0 + m)

case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).getVert m = p✝.getVert (n + m)
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).getVert m = (cons h✝ p✝).getVert (n✝ + 1 + m)
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.drop (m + n) ≍ (p.drop n).drop m

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
⊢ nil.drop (m + 0) ≍ (nil.drop 0).drop m

case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ nil.drop (m + (n✝ + 1)) ≍ (nil.drop (n✝ + 1)).drop m

case cons.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.drop (m + n) ≍ (p✝.drop n).drop m
⊢ (cons h✝ p✝).drop (m + 0) ≍ ((cons h✝ p✝).drop 0).drop m

case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.drop (m + n) ≍ (p✝.drop n).drop m
n✝ : ℕ
⊢ (cons h✝ p✝).drop (m + (n✝ + 1)) ≍ ((cons h✝ p✝).drop (n✝ + 1)).drop m
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.drop n).Nil ↔ p.length ≤ n

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).Nil ↔ nil.length ≤ 0

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).Nil ↔ nil.length ≤ n✝ + 1

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).Nil ↔ p✝.length ≤ n
⊢ ((cons h✝ p✝).drop 0).Nil ↔ (cons h✝ p✝).length ≤ 0

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).Nil ↔ p✝.length ≤ n
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).Nil ↔ (cons h✝ p✝).length ≤ n✝ + 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
n : ℕ
⊢ (p.drop n).darts = List.drop n p.darts

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).darts = List.drop 0 nil.darts

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).darts = List.drop (n✝ + 1) nil.darts

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).darts = List.drop n p✝.darts
⊢ ((cons h✝ p✝).drop 0).darts = List.drop 0 (cons h✝ p✝).darts

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).darts = List.drop n p✝.darts
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).darts = List.drop (n✝ + 1) (cons h✝ p✝).darts
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.drop n).edges = List.drop n p.edges

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).edges = List.drop 0 nil.edges

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).edges = List.drop (n✝ + 1) nil.edges

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).edges = List.drop n p✝.edges
⊢ ((cons h✝ p✝).drop 0).edges = List.drop 0 (cons h✝ p✝).edges

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).edges = List.drop n p✝.edges
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).edges = List.drop (n✝ + 1) (cons h✝ p✝).edges
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).length = min n p.length

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.take 0).length = min 0 nil.length

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).length = min (n✝ + 1) nil.length

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.take n).length = min n p✝.length
⊢ ((cons h✝ p✝).take 0).length = min 0 (cons h✝ p✝).length

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.take n).length = min n p✝.length
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).length = min (n✝ + 1) (cons h✝ p✝).length
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
⊢ w.length ≤ G.edgeFinset.card

Tactic:
rw [← this]

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
⊢ edges.card ≤ G.edgeFinset.card
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 (m + n) ≍ (p.take n).append ((p.drop n).take m)

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
⊢ nil.take (m + 0) ≍ (nil.take 0).append ((nil.drop 0).take m)

case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ nil.take (m + (n✝ + 1)) ≍ (nil.take (n✝ + 1)).append ((nil.drop (n✝ + 1)).take m)

case cons.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
⊢ (cons h✝ p✝).take (m + 0) ≍ ((cons h✝ p✝).take 0).append (((cons h✝ p✝).drop 0).take m)

case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
n✝ : ℕ
⊢ (cons h✝ p✝).take (m + (n✝ + 1)) ≍ ((cons h✝ p✝).take (n✝ + 1)).append (((cons h✝ p✝).drop (n✝ + 1)).take m)
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).support = List.take (n + 1) p.support

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.take 0).support = List.take (0 + 1) nil.support

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).support = List.take (n✝ + 1 + 1) nil.support

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.take n).support = List.take (n + 1) p✝.support
⊢ ((cons h✝ p✝).take 0).support = List.take (0 + 1) (cons h✝ p✝).support

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.take n).support = List.take (n + 1) p✝.support
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).support = List.take (n✝ + 1 + 1) (cons h✝ p✝).support
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).darts = List.take n p.darts

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.take 0).darts = List.take 0 nil.darts

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).darts = List.take (n✝ + 1) nil.darts

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.take n).darts = List.take n p✝.darts
⊢ ((cons h✝ p✝).take 0).darts = List.take 0 (cons h✝ p✝).darts

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.take n).darts = List.take n p✝.darts
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).darts = List.take (n✝ + 1) (cons h✝ p✝).darts
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).edges = List.take n p.edges

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.take 0).edges = List.take 0 nil.edges

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).edges = List.take (n✝ + 1) nil.edges

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.take n).edges = List.take n p✝.edges
⊢ ((cons h✝ p✝).take 0).edges = List.take 0 (cons h✝ p✝).edges

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.take n).edges = List.take n p✝.edges
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).edges = List.take (n✝ + 1) (cons h✝ p✝).edges
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.drop n).support = List.drop (min n p.length) p.support

Tactic:
induction p generalizing n <;> cases n

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).support = List.drop (min 0 nil.length) nil.support

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).support = List.drop (min (n✝ + 1) nil.length) nil.support

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).support = List.drop (min n p✝.length) p✝.support
⊢ ((cons h✝ p✝).drop 0).support = List.drop (min 0 (cons h✝ p✝).length) (cons h✝ p✝).support

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).support = List.drop (min n p✝.length) p✝.support
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).support = List.drop (min (n✝ + 1) (cons h✝ p✝).length) (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ G.IsClique s ↔ IsChain G.Adj s

Tactic:
simp [IsChain, G.symm.iff]

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
h : p.getVert i = u
hi : ¬i = 0
⊢ i ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
simp only [Set.mem_ofPred_eq]

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

Tactic:
simp only [Set.mem_ofPred_eq]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
h : p.getVert i = u
hi : ¬i = 0
⊢ 1 ≤ p.length ∧ p.length ≤ p.length
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
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ i + 1 ∈ {i | i ≤ p.length - 1}

Tactic:
simp only [Set.mem_ofPred_eq]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ i + 1 ≤ p.length - 1
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

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

Tactic:
rw [← this]

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

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

Tactic:
exact Nat.sSup_mem ⟨0, by simp⟩ h

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
s : Finset α
⊢ Maximal Gᶜ.IsClique ↑s ↔ Maximal G.IsIndepSet ↑s

Tactic:
simp [isMaximalIndepSet_iff, isMaximalClique_iff]

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
s : Finset α
⊢ Maximal Gᶜ.IsIndepSet ↑s ↔ Maximal G.IsClique ↑s

Tactic:
simp [isMaximalIndepSet_iff, isMaximalClique_iff]

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

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n < k * (n / k) + k * (n / k)

Tactic:
← add_lt_add_iff_right (n % k),

Goal state after:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n + n % k < k * (n / k) + k * (n / k) + n % k
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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ 3 / 4 * ε ≤
    |(∑ i ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity i.1 i.2)) /
          ↑(#((star hP G ε hU V).product (star hP G ε hV U))) -
        (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) /
          ↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts))|

Tactic:
simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow]
        simpa using edgeDensity_star_not_uniform hPα hPε hε₁ hUVne hUV

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: n : ℕ
⊢ (2 * n + 1).bitIndices = 0 :: map (fun x ↦ x + 1) n.bitIndices

Tactic:
by
  rw [← bitIndices_bit_true, bit_true]

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case refine_1
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ (map (fun x ↦ x - (a + 1)) L).SortedLT

Tactic:
rwa [sortedLT_iff_pairwise, pairwise_map, Pairwise.and_mem,
        Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y), ← Pairwise.and_mem]

Goal state after:
case refine_1.H
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ ∀ (a_1 b : ℕ), a_1 ∈ L ∧ b ∈ L ∧ a_1 - (a + 1) < b - (a + 1) ↔ a_1 ∈ L ∧ b ∈ L ∧ a_1 < b
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun a ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology (β a)
e : Finset α → Set ((a : α) → β a) := fun s ↦ {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this : ∀ (s : Finset α), s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ (x : ↥s), f x = g t ↑x} = e s
s : Finset α
⊢ IsClosed (e s)

Tactic:
rw [← this]

Goal state after:
α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun a ↦ ⊥
instDiscr : ∀ (a : α), DiscreteTopology (β a)
e : Finset α → Set ((a : α) → β a) := fun s ↦ {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
this : ∀ (s : Finset α), s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ (x : ↥s), f x = g t ↑x} = e s
s : Finset α
⊢ IsClosed (s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ (x : ↥s), f x = g t ↑x})
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ toColex (cons a s ha) ≤ toColex (cons b s hb) ↔ a ≤ b

Tactic:
classical
  rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
⊢ (∃ (_ : ∀ (a : α), ¬p a → a ∈ fixedPoints ⇑f), ∀ a ∈ fixedPoints ⇑f, ¬p a) ↔ ∀ (a : α), ¬p a ↔ a ∈ fixedPoints ⇑f

Tactic:
simp_rw [exists_prop, ← forall_and, ← iff_iff_implies_and_implies]

Goal state after: