mathlib-initiative/mathlib-tactics huggingface dataset:
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
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #(P.nonUniforms G 1) ≤ #P.parts * (#P.parts - 1)

Tactic:
refine (card_filter_le _
    (fun uv => ¬SimpleGraph.IsUniform G 1 (Prod.fst uv) (Prod.snd uv))).trans ?_

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #P.parts.offDiag ≤ #P.parts * (#P.parts - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ ∀ x ∈ (R.extend ⋯ ⋯ ⋯).parts, #x = m ∨ #x = m + 1

Tactic:
simp only [mem_insert, forall_eq_or_imp, extend_parts, and_iff_left hR₁, htn, hn]
    exact ite_eq_or_eq _ _ _

Goal state after:
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.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts) /
      ↑(#P.parts) ^ 2 =
    (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      (↑(#P.parts) ^ 2 * (4 ^ 2) ^ #P.parts)

Tactic:
div_mul_eq_div_div_swap,

Goal state after:
α : 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.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts) /
      ↑(#P.parts) ^ 2 =
    (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / (4 ^ 2) ^ #P.parts /
      ↑(#P.parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
⊢ G.deleteEdges G'.edgeSet = G \ G'

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ ⇑(g.comp f) = ⇑g ∘ ⇑f

Tactic:
ext; simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ofLE G G ⋯ = id G

Tactic:
ext; simp

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

Goal state before:
pp: V : Type u_1
G₁ G₂ G₃ : SimpleGraph V
h₁₂ : G₁ ≤ G₂
h₂₃ : G₂ ≤ G₃
⊢ (ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂) = ofLE G₁ G₃ ⋯

Tactic:
ext; simp

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f✝ f : G →g G'
H : G.Subgraph
⊢ ∀ {v w : W}, Relation.Map H.Adj (⇑f) (⇑f) v w → G'.Adj v w

Tactic:
rintro _ _ ⟨u, v, h, rfl, rfl⟩

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f✝ f : G →g G'
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ G'.Adj (f u) (f v)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f✝ f : G →g G'
H : G.Subgraph
⊢ ∀ {v w : W}, Relation.Map H.Adj (⇑f) (⇑f) v w → v ∈ ⇑f '' H.verts

Tactic:
rintro _ _ ⟨u, v, h, rfl, rfl⟩

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f✝ f : G →g G'
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ f u ∈ ⇑f '' H.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f✝ f : G →g G'
H : G.Subgraph
⊢ ∀ (a b : W), Relation.Map H.Adj (⇑f) (⇑f) a b → Relation.Map H.Adj (⇑f) (⇑f) b a

Tactic:
rintro _ _ ⟨u, v, h, rfl, rfl⟩

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f✝ f : G →g G'
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ Relation.Map H.Adj (⇑f) (⇑f) (f v) (f u)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ H.Free (G.killCopies H)

Tactic:
killCopies_of_ne_bot hH,

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ H.Free (G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some}))
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
⊢ (G'.neighborSet v).toFinset.card = Fintype.card ↑(G'.neighborSet v)

Tactic:
Set.toFinset_card

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
⊢ Fintype.card ↑(G'.neighborSet v) = Fintype.card ↑(G'.neighborSet v)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, (G.singletonSubgraph v).Adj v_1 w → H.Adj v_1 w

Tactic:
exact fun _ _ ↦ False.elim

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ a ∈ G.edgeFinset \ G.incidenceFinset t, ∀ b ∈ image (fun x ↦ s(x, t)) (G.neighborFinset s), a ≠ b

Tactic:
intro e

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
⊢ e ∈ G.edgeFinset \ G.incidenceFinset t → ∀ b ∈ image (fun x ↦ s(x, t)) (G.neighborFinset s), e ≠ b
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj ⋯).neighborSet w = {v}

Tactic:
exact neighborSet_fst_subgraphOfAdj hvw.symm

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
⊢ #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t

Tactic:
have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
  rw [G.edgeFinset_replaceVertex_of_not_adj hn,
    card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image, card_sdiff_of_subset inc,
    ← Nat.sub_add_comm <| card_le_card inc, card_incidenceFinset_eq_degree]
  congr 2
  rw [card_image_of_injective, card_neighborFinset_eq_degree]
  unfold Function.Injective
  aesop

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

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

Tactic:
by simpa [not_nil_iff_lt_length] using hp

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
h : { fst := u', snd := v', adj := h✝ } ∈ p.darts
⊢ ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]

Tactic:
have ⟨i, hi, h⟩ := List.getElem_of_mem h

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝¹ : G.Adj u' v'
h✝ : { fst := u', snd := v', adj := h✝¹ } ∈ p.darts
i : ℕ
hi : i < p.darts.length
h : p.darts[i] = { fst := u', snd := v', adj := h✝¹ }
⊢ ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

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✝
ih : p'.edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) p'.support p'.support.tail
⊢ (cons h✝ p').edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) (cons h✝ p').support (cons h✝ p').support.tail

Tactic:
cases p'

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

case cons.cons
V : Type u
G : SimpleGraph V
u v 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✝).edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) (cons h✝ p✝).support (cons h✝ p✝).support.tail
⊢ (cons h✝¹ (cons h✝ p✝)).edges =
    List.zipWith (fun x1 x2 ↦ s(x1, x2)) (cons h✝¹ (cons h✝ p✝)).support (cons h✝¹ (cons h✝ p✝)).support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ u c v : V
h₁ : G.Adj u v
w₁ : G.Walk v c
v' : V
h₂ : G.Adj u v'
w₂ : G.Walk v' c
h : (cons' u v c h₁ w₁).edges = (cons' u v' c h₂ w₂).edges
⊢ cons' u v c h₁ w₁ = cons' u v' c h₂ w₂

Tactic:
by
    obtain ⟨rfl, h₃⟩ : v = v' ∧ w₁.edges = w₂.edges := by simpa [h₁, h₂.ne] using h
    rw [edges_injective h₃]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
⊢ nil.edgeSet = ∅

Tactic:
ext; simp

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

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).edgeSet = insert s(u, v) p.edgeSet

Tactic:
ext; simp

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
⊢ (Walk.map f p).edgeSet = Sym2.map ⇑f '' p.edgeSet

Tactic:
ext; simp

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:
cases p'

Goal state after:
case nil.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
h : Walk.map f nil = Walk.map f nil
⊢ nil = nil

case nil.cons
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✝
h : Walk.map f nil = Walk.map f (cons h✝ p✝)
⊢ nil = cons h✝ p✝
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:
cases p' <;> simp at h ⊢

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

Goal state before:
pp: case a
α : 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
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ m ≤ #s

Tactic:
exact mod_cast m_le_card_of_mem_chunk_parts (h𝒜 hs)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).edgeSet = p.edgeSet

Tactic:
ext; simp

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:
constructor
    · rintro ⟨_ | _, _, ⟨⟩⟩
      simp
    · rintro ⟨rfl, _, _⟩
      simp

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

Goal state before:
pp: case cons.mpr
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv) → (cons h p).IsSubwalk nil

Tactic:
rintro ⟨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:
cases p'

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

case nil.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : nil.concat h = (cons h✝ p✝).concat h'
⊢ ∃ (hv : u✝ = v'), nil.copy ⋯ hv = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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

Tactic:
cases p'

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

case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : cons h✝¹ (p✝¹.concat h) = (cons h✝ p✝).concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
p' : G.Walk u✝ w
⊢ (nil.append p').support = nil.support ++ p'.support.tail

Tactic:
cases p'

Goal state after:
case nil.nil
V : Type u
G : SimpleGraph V
u v w : V
⊢ (nil.append nil).support = nil.support ++ nil.support.tail

case nil.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w
⊢ (nil.append (cons h✝ p✝)).support = nil.support ++ (cons h✝ p✝).support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝.append p').support = p✝.support ++ p'.support.tail
p' : G.Walk w✝ w
⊢ ((cons h✝ p✝).append p').support = (cons h✝ p✝).support ++ p'.support.tail

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✝
p✝ : G.Walk v✝ w
p_ih✝ : ∀ (p' : G.Walk w w), (p✝.append p').support = p✝.support ++ p'.support.tail
⊢ ((cons h✝ p✝).append nil).support = (cons h✝ p✝).support ++ nil.support.tail

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✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝¹.append p').support = p✝¹.support ++ p'.support.tail
v✝ : V
h✝ : G.Adj w✝ v✝
p✝ : G.Walk v✝ w
⊢ ((cons h✝¹ p✝¹).append (cons h✝ p✝)).support = (cons h✝¹ p✝¹).support ++ (cons h✝ p✝).support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos.inr
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬(u, x).2 = u
p' : G.Walk (u, x).1 w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
ha : G.Adj (u, x).2 (u, x).1
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
cases p'

Goal state after:
case pos.inr.nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x : V
h' : ¬(u, x).2 = u
ha : G.Adj (u, x).2 (u, x).1
ih : ∀ (h : u ∈ nil.support), List.count s(u, x) (nil.takeUntil u h).edges ≤ 1
a✝ : List.Mem u nil.support
⊢ List.count s(u, x) (nil.takeUntil u ⋯).edges + 1 ≤ 1

case pos.inr.cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬(u, x).2 = u
ha : G.Adj (u, x).2 (u, x).1
v✝ : V
h✝ : G.Adj (u, x).1 v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (h : u ∈ (cons h✝ p✝).support), List.count s(u, x) ((cons h✝ p✝).takeUntil u h).edges ≤ 1
a✝ : List.Mem u (cons h✝ p✝).support
⊢ List.count s(u, x) ((cons h✝ p✝).takeUntil u ⋯).edges + 1 ≤ 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.reverse.edgeSet = p.edgeSet

Tactic:
ext; simp

Goal state after:
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).edgeSet = p.edgeSet ∪ q.edgeSet

Tactic:
ext; simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).edgeSet = p.edgeSet

Tactic:
ext; simp

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
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ edges ⊆ G.edgeFinset

Tactic:
intro e

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
e : Sym2 V
⊢ e ∈ edges → e ∈ G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
v : Fin p.support.length
hv : p.support.get v ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f (p.support.get v)
this : Injective fun i ↦ (List.map (⇑f) p.support)[↑i]
⊢ u = v

Tactic:
List.length_map

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ : V
p : G.Walk u✝ v✝
f : G →g G'
h : (Walk.map f p).IsPath
u : Fin p.support.length
hu : p.support.get u ∈ {w | w ∈ p.support}
v : Fin p.support.length
hv : p.support.get v ∈ {w | w ∈ p.support}
hf : f (p.support.get u) = f (p.support.get v)
this : Injective fun i ↦ (List.map (⇑f) p.support)[↑i]
⊢ u = v
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ G.IsNClique n s → H.IsNClique n s

Tactic:
by
  simp_rw [isNClique_iff]
  exact And.imp_left (IsClique.mono h)

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

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

Tactic:
or_iff_right (by rintro ⟨h', rfl⟩; exact h'.not_gt hn)

Goal state after:
α : 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
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
sc : G.IsClique ↑s
sm : ∀ (t : Finset α), G.IsClique ↑t → #t ≤ #s
t : Finset α
tc : G.IsClique ↑t
tcard : #t = G.cliqueNum
⊢ #s = G.cliqueNum

Tactic:
exact eq_of_le_of_not_lt sc.card_le_cliqueNum (by simp [← tcard, sm t tc])

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

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
hp : (Walk.map f p).IsPath
⊢ p.IsPath

Tactic:
rw [isPath_def]
  rw [isPath_def, support_map] at hp
  exact hp.of_map

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε / 9 * ↑((Fintype.card G + Fintype.card G + Fintype.card G) ^ 2) ≤ ↑(#A)

Tactic:
mul_comm_div,

Goal state after:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε * (↑((Fintype.card G + Fintype.card G + Fintype.card G) ^ 2) / 9) ≤ ↑(#A)
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * A)) * ↑(#(A * A)) = σₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
rw [← mulConst_mul_card]; ring

Goal state after:
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * A)) * ↑(#(A * A)) = σₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
by rw [← mulConst_mul_card]; ring

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: ε : ℝ
hε : 0 < ε
n : ℕ
hn : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = rothNumberNat n
hs₃ : ThreeAPFree ↑A
⊢ ↑(rothNumberNat n) ≤ ε * ↑n

Tactic:
← hs₂,

Goal state after:
ε : ℝ
hε : 0 < ε
n : ℕ
hn : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = rothNumberNat n
hs₃ : ThreeAPFree ↑A
⊢ ↑(#A) ≤ ε * ↑n
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
⊢ insert 0 A ⊆ (insert a A).subsetSum

Tactic:
insert_subset_iff,

Goal state after:
M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
⊢ 0 ∈ (insert a A).subsetSum ∧ A ⊆ (insert a A).subsetSum
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: ⊢ bitIndices 0 = []

Tactic:
by simp [bitIndices]

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

Goal state before:
pp: ⊢ bitIndices 1 = [0]

Tactic:
by simp [bitIndices]

Goal state after: