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

Goal state before:
pp: case neg.refine_2.refine_1.inr
α : 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
hut : u ≠ t
i : α
⊢ i ∈ u \ (t ∪ {y ∈ R.parts | y ⊆ u}.biUnion id) → i ∈ (u \ t) \ {y ∈ R.parts | y ⊆ u \ t}.biUnion id

Tactic:
simpa using

Goal state after:
case neg.refine_2.refine_1.inr
α : 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
hut : u ≠ t
i : α
⊢ i ∈ u → i ∉ t → (∀ x ∈ R.parts, x ⊆ u → i ∉ x) → (i ∈ u ∧ i ∉ t) ∧ ∀ x ∈ R.parts, x ⊆ u \ t → i ∉ x
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
s : Set (Sym2 V)
G : SimpleGraph V
hs : s ⊆ Sym2.diagSet
u v : V
⊢ (G.deleteEdges s).Adj u v ↔ G.Adj u v

Tactic:
simpa using

Goal state after:
V : Type u_1
s : Set (Sym2 V)
G : SimpleGraph V
hs : s ⊆ Sym2.diagSet
u v : V
⊢ G.Adj u v → s(u, v) ∉ s
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
s : Finset (Sym2 V)
hs : s ⊆ G.edgeFinset
hG : p (G.deleteEdges ↑s)
⊢ r ≤ ↑(#s)

Tactic:
simpa using

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
s : Finset (Sym2 V)
hs : s ⊆ G.edgeFinset
hG : p (G.deleteEdges ↑s)
⊢ r ≤ ↑(#s)
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
s : Set G.Subgraph
⊢ ∀ {v w : V}, (∃ G' ∈ s, G'.Adj v w) → G.Adj v w

Tactic:
rintro a b ⟨G', -, hab⟩
        exact G'.adj_sub hab

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
s : Set G.Subgraph
a b : V
h : ∃ G' ∈ s, G'.Adj a b
⊢ ∃ G' ∈ s, G'.Adj b a

Tactic:
simpa using

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a✝ b✝ : V
s : Set G.Subgraph
a b : V
h : ∃ G' ∈ s, G'.Adj a b
⊢ ∃ G' ∈ s, G'.Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
h : Disjoint H₁ H₂
⊢ H₁.edgeSet ⊓ H₂.edgeSet ⊆ ⊥

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
h : Disjoint H₁ H₂
⊢ H₁.edgeSet ∩ H₂.edgeSet = ∅
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case mp
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
f : A.Copy B
⊢ f.toSubgraph ∈ {B' | Nonempty (A ≃g B'.coe)}

Tactic:
simpa using

Goal state after:
case mp
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
f : A.Copy B
⊢ Nonempty (A ≃g (Subgraph.map f.toHom ⊤).coe)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: 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 γ
f : ⊤.Copy G
v w : α
h : G.Adj (f.toEmbedding v) (f.toEmbedding w)
⊢ ⊤.Adj v w

Tactic:
simpa using

Goal state after:
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 γ
f : ⊤.Copy G
v w : α
h : G.Adj (f.toEmbedding v) (f.toEmbedding w)
⊢ ¬v = w
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G.Copy H
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : Fintype ↑(H.neighborSet (f v))
⊢ G.degree v ≤ H.degree (f v)

Tactic:
simpa using

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G.Copy H
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : Fintype ↑(H.neighborSet (f v))
⊢ G.degree v ≤ H.degree (f v)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ ↑{G' | Nonempty (H ≃g G'.coe)} = ↑(image Copy.toSubgraph univ)

Tactic:
simpa using

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ {G' | Nonempty (H ≃g G'.coe)} = Set.range Copy.toSubgraph
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
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ ∑ B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts with B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m ≤
    2 ^ (#P.parts - 1) * m

Tactic:
grw [sum_const, smul_eq_mul, card_filter_atomise_le_two_pow (s := U) hX,
    Finpartition.card_nonuniformWitnesses_le, filter_subset] <;> 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
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
H : G.Subgraph
a b : V
⊢ (H.verts.toFinset, fun a b ↦ decide (H.Adj a b)).2 a b = true → G.Adj a b

Tactic:
simpa using

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a✝ b✝ : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
H : G.Subgraph
a b : V
⊢ H.Adj a b → G.Adj a b
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
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
H : G.Subgraph
a b : V
⊢ (H.verts.toFinset, fun a b ↦ decide (H.Adj a b)).2 a b = true → a ∈ (H.verts.toFinset, fun a b ↦ decide (H.Adj a b)).1

Tactic:
simpa using

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a✝ b✝ : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
H : G.Subgraph
a b : V
⊢ H.Adj a b → a ∈ H.verts
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)
hG : G'.verts.Subsingleton
⊢ G'.degree v = 0

Tactic:
by
  by_cases hv : v ∈ G'.verts
  · rw [← G'.coe_degree ⟨v, hv⟩]
    have := (Set.subsingleton_coe _).mpr hG
    exact G'.coe.degree_eq_zero_of_subsingleton ⟨v, hv⟩
  · exact degree_of_notMem_verts hv

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

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

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
this : w = u ↔ u = w
⊢ w = u ↔ u = w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ (G'.Adj ↑x✝¹ ↑x✝ ∧ ∃ (hv : ↑x✝¹ ∈ G'.verts) (hw : ↑x✝ ∈ G'.verts), G''.Adj ⟨↑x✝¹, hv⟩ ⟨↑x✝, hw⟩) ↔ G''.Adj x✝¹ x✝

Tactic:
simpa using

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ G''.Adj x✝¹ x✝ → G'.Adj ↑x✝¹ ↑x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.IsInduced ↔ ∃ s, G' = ⊤.induce s

Tactic:
by
  refine ⟨fun h ↦ ⟨G'.verts, h.induce_top_verts.symm⟩, fun ⟨s, h⟩ _ hu _ hv hadj ↦ ?_⟩
  rw [h, (h ▸ rfl : s = G'.verts)]
  exact ⟨hu, hv, hadj⟩

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
⊢ G.Adj v p.snd

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ G.Adj v p.snd
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:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ 0 < p.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun x ↦ x.toProd.2) p.darts = p.support.tail

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun x ↦ x.toProd.2) p.darts = 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
⊢ v = v' ∧ w₁.edges = w₂.edges

Tactic:
simpa using

Goal state after:
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
⊢ v = v' ∧ w₁.edges = w₂.edges
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
l✝ : List V
head✝ v : V
l : List V
hne : head✝ :: v :: l ≠ []
hchain : List.IsChain G.Adj (head✝ :: v :: l)
⊢ (ofSupport (head✝ :: v :: l) hne hchain).support = head✝ :: v :: l

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
l✝ : List V
head✝ v : V
l : List V
hne : head✝ :: v :: l ≠ []
hchain : List.IsChain G.Adj (head✝ :: v :: l)
⊢ (ofSupport (v :: l) ⋯ ⋯).support = v :: l
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 using

Goal state after:
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₂ :: l) ⋯ ⋯).darts = d₂ :: l
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
· rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']
        simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.takeUntil u h).length ≤ p.length

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.takeUntil u h).length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.dropUntil u h).length ≤ p.length

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.dropUntil u h).length ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
hsu : ¬1 ≤ (p.takeUntil w h).length
⊢ u = w

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
hsu : ¬1 ≤ (p.takeUntil w h).length
⊢ u = w
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
d : G.Dart
h : d ∈ p.darts
⊢ d.toProd.2 ∈ p.support

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
d : G.Dart
h : d ∈ p.darts
⊢ d.toProd.2 ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
h : n ≤ k
⊢ (p.drop k).IsSubwalk (p.drop n)

Tactic:
induction k, h using Nat.le_induction with
  | base => rfl
  | succ k h ih =>
    apply IsSubwalk.trans ?_ ih
    clear h ih
    induction k generalizing p u with
    | zero => exact p.drop_zero ▸ (p.isSubwalk_rfl.copy rfl rfl p.getVert_zero.symm rfl).tail
    | succ _ ih => cases p <;> simp [drop, ih]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
hl : (p.takeUntil u h).length = p.length
⊢ u = w

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
hl : (p.takeUntil u h).length = p.length
⊢ u = w
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.rotate u h).length = c.length

Tactic:
simpa using

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.rotate u h).length = c.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
n : ℕ
hn : n ≠ 0
⊢ ((cons h p).drop n).support = ((p.drop (n - 1)).copy ⋯ ⋯).support

Tactic:
obtain ⟨_, rfl⟩ := Nat.exists_add_one_eq.mpr (Nat.ne_zero_iff_zero_lt.mp hn)

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
w✝ : ℕ
hn : w✝ + 1 ≠ 0
⊢ ((cons h p).drop (w✝ + 1)).support = ((p.drop (w✝ + 1 - 1)).copy ⋯ ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsTrail
⊢ p.reverse.IsTrail

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsTrail
⊢ p.edges.Nodup
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) := ⋯
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ w.edges

Tactic:
simpa using

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) := ⋯
this : edges.card = w.length
e : Sym2 V
h : e ∈ edges
⊢ e ∈ w.edges
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
⊢ p.reverse.IsPath

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
⊢ p.support.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝ : V
h✝¹ : G.Adj v v✝
h✝ : G.Adj v✝ v
hp : (cons h✝¹ (cons h✝ nil)).IsCircuit
⊢ 3 ≤ (cons h✝¹ (cons h✝ nil)).length

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
v✝ : V
h✝¹ : G.Adj v v✝
h✝ : G.Adj v✝ v
hp : (cons h✝¹ (cons h✝ nil)).IsCircuit
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.reverse.IsCycle
⊢ p.IsCycle

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.reverse.IsCycle
⊢ p.IsCycle
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.snd = p.penultimate

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.snd = p.penultimate
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
hm0 : m = 0
⊢ n = m

Tactic:
simp only [hm0, Walk.getVert_cons p h hn0] at hnm

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hn0 : ¬n = 0
hm0 : m = 0
hnm : p.getVert (n - 1) = (cons h p).getVert 0
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Paths

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

Tactic:
simpa using

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
i : ℕ
hp : Walk.nil.IsPath
hi : i ≤ Walk.nil.length
⊢ i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ (induce s G).Adj ⟨v, hv⟩ ⟨w, hw⟩ ↔ ⊤.Adj ⟨v, hv⟩ ⟨w, hw⟩

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adj
v : α
hv : v ∈ s
w : α
hw : w ∈ s
⊢ G.Adj v w ↔ ¬v = w
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ (cons h q).getVert (n + 1) = (cons h q).getVert (m + 1)

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ q.getVert n = q.getVert m
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : G.IsClique ↑s
ht : (map f s).Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑(map f s)

Tactic:
simpa using

Goal state after:
case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : G.IsClique ↑s
ht : (map f s).Nontrivial
⊢ G.IsClique ↑s
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ (cons h p).support.tail ~ (cons h p).support.dropLast

Tactic:
simpa using

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ p.support ~ (u :: p.support).dropLast
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
hc : (G ⊔ edge v w).IsClique s
x✝ : α
hx : x✝ ∈ s \ {v}
y✝ : α
hy : y✝ ∈ s \ {v}
hxy : x✝ ≠ y✝
⊢ G.Adj x✝ y✝

Tactic:
have := hc hx.1 hy.1 hxy

Goal state after:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
hc : (G ⊔ edge v w).IsClique s
x✝ : α
hx : x✝ ∈ s \ {v}
y✝ : α
hy : y✝ ∈ s \ {v}
hxy : x✝ ≠ y✝
this : (G ⊔ edge v w).Adj x✝ y✝
⊢ G.Adj x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hmem : s(v, w) ∈ p.edges
⊢ w = p.penultimate

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hmem : s(v, w) ∈ p.edges
⊢ w = p.penultimate
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
x : V
w : G.Walk u v
hw : w.IsTrail
hx : x ∈ w.support
⊢ ((w.takeUntil x hx).edges ++ (w.dropUntil x hx).edges).Nodup

Tactic:
simpa using

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
x : V
w : G.Walk u v
hw : w.IsTrail
hx : x ∈ w.support
⊢ w.edges.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Nonempty ((completeGraph (Fin n)).Copy G)
⊢ n ≤ Fintype.card α

Tactic:
simpa using

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Nonempty ((completeGraph (Fin n)).Copy G)
⊢ n ≤ Fintype.card α