mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ log 2 * 2 ≤ √(log 8)

Tactic:
by
  rw [show (8 : ℝ) = 2 ^ 3 by norm_num1, Real.log_pow, Nat.cast_ofNat]
  apply le_sqrt_of_sq_le
  rw [mul_pow, sq (log 2), mul_assoc, mul_comm]
  gcongr
  linarith only [log_two_lt_d9.le]

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑N ^ (1 - 2 / ↑n) / rexp (↑n - 2) / ↑n

Tactic:
div_div,

Goal state after:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑N ^ (1 - 2 / ↑n) / (rexp (↑n - 2) * ↑n)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑N / ↑N ^ (2 / ↑n) / (rexp (↑n - 2) * ↑n)

Tactic:
div_div,

Goal state after:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑N / (↑N ^ (2 / ↑n) * (rexp (↑n - 2) * ↑n))
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : Mul α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #(s * {t.min' ht} ∪ {s.max' hs} * t) ≤ #(s * t)

Tactic:
exact card_mono (union_subset (mul_subset_mul_left <| singleton_subset_iff.2 <| min'_mem _ _) <|
      mul_subset_mul_right <| singleton_subset_iff.2 <| max'_mem _ _)

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

Goal state before:
pp: case mk
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ #{d | d.edge = Quot.mk (Sym2.Rel V) (v, w)} = 2

Tactic:
convert! congr_arg card d.edge_fiber

Goal state after:
case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ 2 = #{d, d.symm}
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ 2 * #G.edgeFinset =
    #{x |
        match x with
        | (x, y) => G.Adj x y}

Tactic:
by
  rw [← dart_card_eq_twice_card_edges, ← card_univ]
  refine card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_
    <;> simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v✝ : V
f : G ≃g G'
v : V
w : ↑(G'.neighborSet (f v))
⊢ f.symm ↑w ∈ G.neighborSet v

Tactic:
by
      simpa [RelIso.symm_apply_apply] using f.symm.apply_mem_neighborSet_iff.mpr w.2

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G.degree v = 1 ↔ ∃! w, G.Adj v w

Tactic:
rw [degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]
  simp only [mem_neighborFinset]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
⊢ ∃ c ∈ P.parts, c ≤ b

Tactic:
by_contra H

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a b : α
P Q : Finpartition a
h : P ≤ Q
hb : b ∈ Q.parts
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
| 4 ^ #P.parts

Tactic:
rw [← Nat.sub_add_cancel h]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
| 4 ^ #P.parts - 1 + 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#A) * ((↑(#A) + ↑(#P.parts)) / ↑(#P.parts)) = ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

Tactic:
mul_div_assoc

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#A) * ((↑(#A) + ↑(#P.parts)) / ↑(#P.parts)) = ↑(#A) * ((↑(#A) + ↑(#P.parts)) / ↑(#P.parts))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#A) * (↑(#A) / ↑(#P.parts) + 1) = ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

Tactic:
by rw [← div_add_same (mod_cast h.card_pos.ne'), mul_div_assoc]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ stepBound^[⌊4 / ε ^ 5⌋₊] t * 4 ^ stepBound^[⌊4 / ε ^ 5⌋₊] t ≤ bound ε l

Tactic:
bound

Goal state after:
case refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ stepBound^[⌊4 / ε ^ 5⌋₊] t * 4 ^ stepBound^[⌊4 / ε ^ 5⌋₊] t ≤
    stepBound^[⌊4 / ε ^ 5⌋₊] (initialBound ε l) * 16 ^ stepBound^[⌊4 / ε ^ 5⌋₊] (initialBound ε l)
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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 2 ^ #P.parts * (ε * ε / 10) = 2 ^ #P.parts * (ε * (ε / 10))

Tactic:
mul_div_assoc

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 2 ^ #P.parts * (ε * (ε / 10)) = 2 ^ #P.parts * (ε * (ε / 10))
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ (∃ w, u = x✝ ∧ v = w ∨ u = w ∧ v = x✝) → x✝ ∈ {u, v}

Tactic:
rintro ⟨_, hw⟩

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ w✝ : V
hw : u = x✝ ∧ v = w✝ ∨ u = w✝ ∧ v = x✝
⊢ x✝ ∈ {u, v}
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: case nil
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 = f (nil.getVert n)

Tactic:
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))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: case cons
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 = f ((cons h✝ p✝).getVert n)

Tactic:
cases n

Goal state after:
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.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u v✝ v u' : V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ Walk.map (Embedding.induce s).toHom (Walk.induce s (cons huu' w) hw) = cons huu' w

Tactic:
simp [map_induce]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 1 / (↑m + 1) ≤ ε ^ 5 / 50 / 2

Tactic:
div_div,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 1 / (↑m + 1) ≤ ε ^ 5 / (50 * 2)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' : V
p : G.Walk u v
⊢ p.IsSubwalk nil ↔ ∃ (hu : u' = u) (hv : u' = v), p = nil.copy hu hv

Tactic:
by
  cases p with
  | nil =>
    constructor
    · rintro ⟨_ | _, _, ⟨⟩⟩
      simp
    · rintro ⟨rfl, _, _⟩
      simp
  | cons h p =>
    constructor
    · rintro ⟨_ | _, _, h⟩ <;> simp at h
    · rintro ⟨rfl, rfl, ⟨⟩⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ {u} + ↑p.support.tail + ↑p'.support.tail = {u} + ↑p.support.tail + ({v} + ↑p'.support.tail) - {v}

Tactic:
add_comm ({v} : Multiset V),

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ {u} + ↑p.support.tail + ↑p'.support.tail = {u} + ↑p.support.tail + (↑p'.support.tail + {v}) - {v}
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).length = nil.length - n

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

Goal state before:
pp: case cons
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).length = (cons h✝ p✝).length - n

Tactic:
cases n

Goal state after:
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: case nil
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n : ℕ
⊢ (nil.drop n).getVert m = nil.getVert (n + m)

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

Goal state before:
pp: case cons
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).getVert m = (cons h✝ p✝).getVert (n + m)

Tactic:
cases n

Goal state after:
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: case nil
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n : ℕ
⊢ nil.drop (m + n) ≍ (nil.drop n).drop m

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

Goal state before:
pp: case cons
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) ≍ ((cons h✝ p✝).drop n).drop m

Tactic:
cases n

Goal state after:
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: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).Nil ↔ nil.length ≤ n

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

Goal state before:
pp: case cons
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).Nil ↔ (cons h✝ p✝).length ≤ n

Tactic:
cases n

Goal state after:
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: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).darts = List.drop n nil.darts

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

Goal state before:
pp: case cons
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).darts = List.drop n (cons h✝ p✝).darts

Tactic:
cases n

Goal state after:
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: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).edges = List.drop n nil.edges

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

Goal state before:
pp: case cons
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).edges = List.drop n (cons h✝ p✝).edges

Tactic:
cases n

Goal state after:
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: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.take n).length = min n nil.length

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

Goal state before:
pp: case cons
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).length = min n (cons h✝ p✝).length

Tactic:
cases n

Goal state after:
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.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n m : ℕ
⊢ (nil.take n).getVert m = nil.getVert (min n m)

Tactic:
cases n

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

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
m n✝ : ℕ
⊢ (nil.take (n✝ + 1)).getVert m = nil.getVert (min (n✝ + 1) m)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
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 m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n m : ℕ
⊢ ((cons h✝ p✝).take n).getVert m = (cons h✝ p✝).getVert (min n m)

Tactic:
cases n

Goal state after:
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 m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
m : ℕ
⊢ ((cons h✝ p✝).take 0).getVert m = (cons h✝ p✝).getVert (min 0 m)

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 m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
m n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).getVert m = (cons h✝ p✝).getVert (min (n✝ + 1) m)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n : ℕ
⊢ nil.take (m + n) ≍ (nil.take n).append ((nil.drop n).take m)

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

Goal state before:
pp: case cons
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) ≍ ((cons h✝ p✝).take n).append (((cons h✝ p✝).drop n).take m)

Tactic:
cases n

Goal state after:
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: case nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ (nil.take n).Nil ↔ nil.Nil ∨ n = 0

Tactic:
cases n

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

case nil.succ
V : Type u
G : SimpleGraph V
u : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).Nil ↔ nil.Nil ∨ n✝ + 1 = 0
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).take n).Nil ↔ (cons h✝ p✝).Nil ∨ n = 0

Tactic:
cases n

Goal state after:
case cons.zero
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 ↔ (cons h✝ p✝).Nil ∨ 0 = 0

case cons.succ
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).Nil ↔ (cons h✝ p✝).Nil ∨ n✝ + 1 = 0