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

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

Tactic:
← le_log_iff_exp_le (rpow_pos_of_pos hN₀ _),

Goal state after:
case h₁
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
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ -2 * √(log ↑N) ≤ log (↑N ^ (-(2 / ↑n)))
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
K : Finset G
hKA : A ^ 2 ⊆ ↑K • A
hK : ∃ x, K = ∅ ∨ K = {x}
⊢ ∃ x, A * A ⊆ x • A

Tactic:
obtain ⟨x, rfl | rfl⟩ := hK

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑∅ • A
⊢ ∃ x, A * A ⊆ x • A

case inr
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑{x} • A
⊢ ∃ x, A * A ⊆ x • A
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
⊢ minOrder G = ⊤ ↔ IsMulTorsionFree G

Tactic:
simp [minOrder, isMulTorsionFree_iff_not_isOfFinOrder]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#{x | ¬↑(G.degree x) = 0}) = 0
⊢ Even #{v | Odd (G.degree v)}

Tactic:
rw [← ZMod.natCast_eq_zero_iff_even]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#{x | ¬↑(G.degree x) = 0}) = 0
⊢ ↑(#{v | Odd (G.degree v)}) = 0
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G.neighborFinset v = ∅ ↔ G.IsIsolated v

Tactic:
by
  simp [neighborFinset, IsIsolated, Set.ext_iff]

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)
⊢ 0 < G.degree v ↔ ∃ w, G.Adj v w

Tactic:
simp only [degree, card_pos, Finset.Nonempty, mem_neighborFinset]

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

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
h✝ : Nonempty V
⊢ ∀ (v : V), G.minDegree ≤ H.degree v

Tactic:
exact fun v ↦ (G.minDegree_le_degree v).trans (G.degree_le_of_le hle)

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
x✝ : α
hx : x✝ ∈ ↑P.parts
y✝ : α
hy : y✝ ∈ ↑P.parts
hxy : x✝ ≠ y✝
this : id x✝ ⊓ id y✝ = ⊥
⊢ (Disjoint on f) x✝ y✝

Tactic:
simp_all [disjoint_iff, ← hf]

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
H : ¬∃ c ∈ P.parts, c ≤ b
⊢ ∀ p ∈ P.parts, ∃ q ∈ Q.parts.erase b, p ≤ q

Tactic:
grind [h _]

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

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
a b : α
P : Finpartition a
hb : b ≤ a
M : Type u_2
inst✝ : AddCommMonoid M
f : α → M
hf : f ⊥ = 0
⊢ ∑ p ∈ (P.restrict hb).parts, f p = ∑ q ∈ P.parts, f (q ⊓ b)

Tactic:
have hinj : ∀ x ∈ P.parts.filter (· ⊓ b ≠ ⊥), ∀ y ∈ P.parts.filter (· ⊓ b ≠ ⊥),
      x ⊓ b = y ⊓ b → x = y := fun x hx y hy hxy => by
    by_contra hne
    simp only [Finset.mem_filter] at hx hy
    have : Disjoint (x ⊓ b) (y ⊓ b) := (P.disjoint hx.1 hy.1 hne).mono inf_le_left inf_le_left
    grind
  have heq : (P.parts.image (· ⊓ b)).erase ⊥ = (P.parts.filter (· ⊓ b ≠ ⊥)).image (· ⊓ b) := by
    grind
  have hz : ∑ x ∈ P.parts.filter (¬ · ⊓ b ≠ ⊥), f (x ⊓ b) = 0 := Finset.sum_eq_zero fun x hx => by
    simp only [ne_eq, Decidable.not_not, Finset.mem_filter] at hx
    rw [hx.2, hf]
  simp only [restrict, heq, ← Finset.sum_filter_add_sum_filter_not P.parts (· ⊓ b ≠ ⊥), hz,
    Finset.sum_image hinj, add_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n : ℤ
inst✝ : t.IsLE X n
j : ℤ
hj : WithBotTop.coe n < WithBotTop.coe j
⊢ IsZero ((t.eTruncGE.obj (WithBotTop.coe j)).obj X)

Tactic:
simp only [WithBotTop.coe_lt_coe] at hj

Goal state after:
case coe
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n : ℤ
inst✝ : t.IsLE X n
j : ℤ
hj : n < j
⊢ IsZero ((t.eTruncGE.obj (WithBotTop.coe j)).obj X)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ a ∈ (image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset).sup id

Tactic:
mem_sup

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ ∃ i ∈ image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset, a ∈ id i
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case neg
α : 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 α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ ∃ P,
    P.IsEquipartition ∧
      t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i + 1] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G))

Tactic:
have hi : (i : ℝ) ≤ 4 / ε ^ 5 := by
    have hi : ε ^ 5 / 4 * ↑i ≤ 1 := hP₄.trans (mod_cast P.energy_le_one G)
    rw [div_mul_eq_mul_div, div_le_iff₀ (show (0 : ℝ) < 4 by simp)] at hi
    norm_num at hi
    rwa [le_div_iff₀' (pow_pos hε _)]

Goal state after:
case neg
α : 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 α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
⊢ ∃ P,
    P.IsEquipartition ∧
      t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i + 1] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)) =
    ∑ x ∈ P.parts.offDiag,
      (↑(G.edgeDensity x.1 x.2) ^ 2 + ((if G.IsUniform ε x.1 x.2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25))

Tactic:
by
        rw [sum_add_distrib, sum_sub_distrib, sum_const, nsmul_eq_mul, sum_ite, sum_const_zero,
          zero_add, sum_const, nsmul_eq_mul, ← Finpartition.nonUniforms, ← add_sub_assoc,
          add_sub_right_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hadj : G.Adj v w
⊢ (G.subgraphOfAdj hadj).spanningCoe = fromEdgeSet {s(v, w)}

Tactic:
ext v w
  aesop

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

Goal state before:
pp: case refine_4
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v w : W
⊢ (Subgraph.map f H).Adj v w → H'.Adj v w

Tactic:
· simp only [Relation.Map, map_adj, forall_exists_index, and_imp]
    rintro u u' hu rfl rfl
    exact (h.2 hu).2

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
G' : G.Subgraph
inst✝ : Fintype ↑G'.verts
h : G'.IsSpanning
⊢ G'.verts.toFinset.card = Fintype.card V

Tactic:
by
  simp only [isSpanning_iff.1 h, Set.toFinset_univ]
  congr

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : n ≠ 0
hs : n ≤ #s
⊢ ∃ P, P.IsEquipartition ∧ #P.parts = n

Tactic:
rw [← pos_iff_ne_zero] at hn
  have : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s := by
    rw [tsub_mul, mul_add, ← add_assoc,
      tsub_add_cancel_of_le (Nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one, add_comm,
      mod_add_div]
  refine
    ⟨(indiscrete (card_pos.1 <| hn.trans_le hs).ne_empty).equitabilise this,
      equitabilise_isEquipartition, ?_⟩
  rw [card_parts_equitabilise _ _ (Nat.div_pos hs hn).ne', tsub_add_cancel_of_le (mod_lt _ hn).le]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

Tactic:
obtain h | h := eq_or_ne v w
  · simp [h]
  · refine ⟨fun h ↦ .inr <| h (by simp_all [edge_adj]), fun hadj v' w' hvw' ↦ ?_⟩
    grind [adj_symm]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
i : ℕ
hi : nil.length ≤ i
⊢ nil.getVert i = u✝

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
i : ℕ
hi : i < nil.length
⊢ G.Adj (nil.getVert i) (nil.getVert (i + 1))

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
h : n ≤ nil.length
⊢ nil.getVert n = nil.support[n]

Tactic:
| nil =>

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

Goal state before:
pp: case Adj.mp
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ → (⊤.induce {v, w}).Adj x✝¹ x✝

Tactic:
intro h
      simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff] at h
      obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h <;> simp [hvw, hvw.symm]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n : ℕ
h : n + 1 ≤ (cons h✝ p✝).length
⊢ p✝.getVert (n + 1 - 1) = if h : n + 1 = 0 then u else p✝.support[n + 1 - 1]

Tactic:
exact getVert_eq_support_getElem _ (Nat.sub_le_of_le_add h)

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u✝ : V
d : G.Dart
h : d.toProd.2 = u✝
⊢ List.IsChain G.DartAdj (d :: nil.darts)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
h : nil.support.Nodup
⊢ nil.darts.Nodup

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) nil.support nil.support.tail

Tactic:
| nil =>

Goal state after:
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'
hinj : Function.Injective ⇑f
u v u✝ : V
p' : G.Walk u✝ u✝
h : Walk.map f nil = Walk.map f p'
⊢ nil = p'

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ u✝
ih : ∀ ⦃p' : G.Walk v✝ u✝⦄, Walk.map f p✝ = Walk.map f p' → p✝ = p'
h : Walk.map f (cons h✝ p✝) = Walk.map f nil
⊢ cons h✝ p✝ = nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
hnil : ¬nil.Nil
⊢ w ∈ nil.support ↔ ∃ e ∈ nil.edges, w ∈ e

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u✝ : V
uS : u✝ ∈ S
vS : u✝ ∉ S
⊢ ∃ d ∈ nil.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u✝ u : V
h : G.Adj u u✝
⊢ ∃ x q, ∃ (h' : G.Adj x u✝), cons h nil = q.concat h'

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w x u✝ : V
q : G.Walk u✝ w
r : G.Walk u✝ x
⊢ (nil.append q).reverseAux r = q.reverseAux (nil.reverseAux r)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u✝ : V
q : G.Walk u✝ w
⊢ (nil.reverseAux q).append r = nil.reverseAux (q.append r)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.reverse.reverse = nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.reverseAux q).length = nil.length + q.length

Tactic:
| nil =>

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

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

Tactic:
| nil =>

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

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

Tactic:
| nil =>

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)
⊢ 50 * 2 / ε ^ 5 ≤ ↑m + 1

Tactic:
refine le_trans ?_ (le_add_of_nonneg_right zero_le_one)
    norm_num
    apply hundred_div_ε_pow_five_le_m hPα hPε

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
⊢ p₁.IsSubwalk p₂

Tactic:
have : (s.length + p₁.length) ≤ p₂.length := by grind [_=_ length_support]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₁.IsSubwalk p₂
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ w✝ u✝ : V
inst✝ : DecidableEq V
v w u : V
h : u ∈ nil.support
⊢ G.Walk v u

Tactic:
mem_support_nil_iff.mp h

Goal state after:
V : Type u
G : SimpleGraph V
v✝ w✝ u✝ : V
inst✝ : DecidableEq V
v w u : V
h : u ∈ nil.support
⊢ G.Walk v v
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ : V
h : w ∈ nil.support
⊢ (nil.takeUntil w h).support = ((nil.take (List.idxOf w nil.support)).copy ⋯ ⋯).support

Tactic:
| nil =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ w✝ u✝ : V
inst✝ : DecidableEq V
v w u : V
h : u ∈ nil.support
⊢ G.Walk u v

Tactic:
mem_support_nil_iff.mp h

Goal state after:
V : Type u
G : SimpleGraph V
v✝ w✝ u✝ : V
inst✝ : DecidableEq V
v w u : V
h : u ∈ nil.support
⊢ G.Walk v v
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' h : G.Adj v' w
he : nil.concat h = nil.concat h'
⊢ ∃ (hv : v' = v'), nil.copy ⋯ hv = nil

Tactic:
exact ⟨rfl, rfl⟩

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
p' : G.Walk u✝ v'
he : nil.concat h = p'.concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = p'

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ : V
h : w ∈ nil.support
⊢ (nil.dropUntil w h).support = ((nil.drop (List.idxOf w nil.support)).copy ⋯ ⋯).support

Tactic:
| nil =>

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

Goal state before:
pp: case cons.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : G.Adj w✝ w
h✝ : G.Adj u✝ v✝
h' : G.Adj w✝ w
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ w✝}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = w✝), p✝.copy ⋯ hv = p'
he : p✝.concat h ≍ (p✝.copy ⋯ ⋯).concat h'
⊢ ∃ (hv : w✝ = w✝), (cons h✝¹ p✝).copy ⋯ hv = cons h✝ (p✝.copy ⋯ ⋯)

Tactic:
exact ⟨rfl, rfl⟩

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.support.dropLast ++ [u] = nil.support

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ : V
h : u ∈ nil.support
⊢ List.count s(u, x) (nil.takeUntil u h).edges ≤ 1

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
x u✝ : V
q : G.Walk u✝ w
hx : x ∈ nil.support
⊢ (nil.append q).takeUntil x ⋯ = nil.takeUntil x hx

Tactic:
| nil =>

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
w x : V
p : G.Walk u v
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
⊢ (p.takeUntil w hw).takeUntil x hx = p.takeUntil x ⋯

Tactic:
by
  simp_rw [← takeUntil_append_of_mem_left _ (p.dropUntil w hw) hx, take_spec]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
h : nil.support.Nodup
⊢ nil.edges.Nodup

Tactic:
| nil =>

Goal state after:
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
⊢ w.length ≤ G.edgeFinset.card

Tactic:
let edges := w.edges.toFinset
  have : edges.card = w.length := length_edges _ ▸ List.toFinset_card_of_nodup h.edges_nodup
  rw [← this]
  have : edges ⊆ G.edgeFinset := by
    intro e h
    refine mem_edgeFinset.mpr ?_
    apply w.edges_subset_edgeSet
    simpa [edges] using h
  exact Finset.card_le_card this

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
hp : Walk.nil.IsPath
⊢ Walk.nil.tail.IsPath

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
hp : Walk.nil.IsPath
n : ℕ
hn : n ∈ {i | i ≤ Walk.nil.length}
m : ℕ
hm : m ∈ {i | i ≤ Walk.nil.length}
hnm : Walk.nil.getVert n = Walk.nil.getVert m
⊢ n = m

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
hp : G.Adj nil.penultimate u✝
⊢ nil.dropLast.concat hp = nil

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v u✝ v✝ : V
hadj : G.Adj u✝ v✝
hind : ∀ (hp : G.Adj nil.penultimate v✝), nil.dropLast.concat hp = nil
hp : G.Adj (cons hadj nil).penultimate v✝
⊢ (cons hadj nil).dropLast.concat hp = cons hadj nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Set.InjOn Walk.nil.getVert {i | i ≤ Walk.nil.length} → Walk.nil.IsPath

Tactic:
| nil =>

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

Goal state before:
pp: 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 : ℕ
x✝ : k ≤ p.length ∨ p.length < k
⊢ p.support[k]? = q.support[k]?

Tactic:
cases le_or_gt k p.length with

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.tail.support ~ nil.dropLast.support

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.support.tail ~ nil.support.dropLast

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
x✝ : α
w✝¹ : x✝ ∈ F
ainA : ⟨x✝, ⋯⟩ ∈ A
y✝ : α
w✝ : y✝ ∈ F
binA : ⟨y✝, ⋯⟩ ∈ A
⊢ x✝ ≠ y✝ → G.Adj x✝ y✝

Tactic:
anb

Goal state after:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
x✝ : α
w✝¹ : x✝ ∈ F
ainA : ⟨x✝, ⋯⟩ ∈ A
y✝ : α
w✝ : y✝ ∈ F
binA : ⟨y✝, ⋯⟩ ∈ A
anb : x✝ ≠ y✝
⊢ G.Adj x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.Clique

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

Tactic:
rintro ⟨⟨s, hs, rfl⟩, rfl⟩
    simp [isNClique_iff, hs]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
x✝ : nil.tail.IsPath ∧ 3 ≤ nil.length
h₁ : nil.tail.IsPath
h₂ : 3 ≤ nil.length
⊢ nil.IsCycle

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ : V
⊢ nil.bypass.IsPath

Tactic:
| nil =>

Goal state after: