mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝³ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝² : v \ u = v
this✝¹ : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this✝ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ (insert w ((s ∪ v) \ u) ∪ u.erase w) \ v.erase z ∈ 𝒜

Tactic:
refine sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ((erase_subset _ _).trans ‹_›) ?_

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝³ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝² : v \ u = v
this✝¹ : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∉ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this✝ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (u.erase w) (v.erase z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ Disjoint (u.erase w) (insert w ((s ∪ v) \ u))
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
⊢ IsInitSeg (∂ 𝒜) (r - 1)

Tactic:
obtain rfl | hr := Nat.eq_zero_or_pos r

Goal state after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
⊢ IsInitSeg (∂ 𝒜) (0 - 1)

case intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Finite α
h₁ : IsInitSeg 𝒜 r
val✝ : Fintype α
hr : r > 0
⊢ IsInitSeg (∂ 𝒜) (r - 1)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : compress U V s ≠ s
⊢ toColex (compress U V s) < toColex s

Tactic:
rw [compress, ite_ne_right_iff] at hA
  rw [compress, if_pos hA.1, lt_iff_exists_filter_lt]
  simp_rw [mem_sdiff (s := s), filter_inj, and_assoc]
  refine ⟨_, hA.1.2 <| max'_mem _ hV, notMem_sdiff_of_mem_right <| max'_mem _ _, fun a ha ↦ ?_⟩
  have : a ∉ V := fun H ↦ ha.not_ge (le_max' _ _ H)
  have : a ∉ U := fun H ↦ ha.not_gt ((le_max' _ _ H).trans_lt h)
  simp [‹a ∉ U›, ‹a ∉ V›]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
⊢ v ∈ H.verts

Tactic:
by_cases hnp : p.Nil
    · exact hnp.eq ▸ hv'
    exact aux (H.edge_vert (h _ hv' _ (Walk.adj_snd hnp)).symm) p.tail

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
h : ¬G.Reachable u v
hb : G.IsBridge e
he : e ∈ G.edgeSet
w : V
p : (G ⊔ edge u v).Walk w w
hp : p.IsCycle
hpe : e ∈ p.edges
e' : Sym2 V
he' : e' ∈ p.edges
h' : e' ∈ (edge u v).edgeSet
⊢ p.IsCycle ∧ s(u, v) ∈ p.edges

Tactic:
simp_all

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u x : V
hxu : x ≠ u
hx : (G.neighborSet x).Subsingleton
w : V
hxv : x ≠ u
hw : Walk.nil.IsTrail
hxw : x ∈ Walk.nil.support
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet w)
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ G.neighborFinset w ⊆ s

Tactic:
rw [isBipartiteWith_neighborFinset' h hw]

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet w)
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ {v ∈ s | G.Adj v w} ⊆ s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ G.IsBridge s(u, v) ↔ ¬G.IsEdgeReachable 2 u v

Tactic:
refine ⟨fun h ↦ h.not_isEdgeReachable_two, fun hc hr ↦ hc fun s hs₂ ↦ ?_⟩
  by_cases! hs₁ : s.encard ≠ (1 : ℕ)
  · apply G.isEdgeReachable_one.mpr huv.reachable
    exact lt_of_le_of_ne (ENat.lt_natCast_add_one_iff.mp hs₂) hs₁
  obtain ⟨x, rfl⟩ := s.encard_eq_one.mp hs₁
  obtain rfl | hx := eq_or_ne s(u, v) x
  · exact hr
  · exact deleteEdges_adj.mpr ⟨huv, hx⟩ |>.reachable

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
simp only [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha✝ : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb✝ : b ∈ (G.subgraphOfAdj hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha✝⟩ ⟨b, hb✝⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
w u x : V
hadj : nil.toSubgraph.Adj w x
⊢ ¬nil.Nil

Tactic:
simp_all

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
w u v x v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
hadj : (cons h✝ p✝).toSubgraph.Adj w x
⊢ ¬(cons h✝ p✝).Nil

Tactic:
simp_all

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

Goal state before:
pp: case refine_1.inl.inl
W₁ : Type u_2
W₂ : Type u_3
val✝¹ val✝ : W₁
h : s(Sum.inl val✝¹, Sum.inl val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inl val✝¹, Sum.inl val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
simp_all

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

Goal state before:
pp: case refine_1.inl.inr
W₁ : Type u_2
W₂ : Type u_3
val✝¹ : W₁
val✝ : W₂
h : s(Sum.inl val✝¹, Sum.inr val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inl val✝¹, Sum.inr val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
simp_all

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

Goal state before:
pp: case refine_1.inr.inl
W₁ : Type u_2
W₂ : Type u_3
val✝¹ : W₂
val✝ : W₁
h : s(Sum.inr val✝¹, Sum.inl val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝¹, Sum.inl val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
simp_all

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

Goal state before:
pp: case refine_1.inr.inr
W₁ : Type u_2
W₂ : Type u_3
val✝¹ val✝ : W₂
h : s(Sum.inr val✝¹, Sum.inr val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝¹, Sum.inr val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
simp_all

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
W₁ : Type u_2
W₂ : Type u_3
inst✝ : DecidableRel fun x1 x2 ↦ x1 ∈ x2
hG : G.IsBipartiteWith s t
⊢ Function.Injective fun x ↦
    match x with
    | ⟨e, he⟩ =>
      Sym2.fromRelNdrec e he
        (fun u v h ↦
          ⋯.by_cases (fun h ↦ ⟨s(Sum.inl ⟨u, ⋯⟩, Sum.inr ⟨v, ⋯⟩), ⋯⟩) fun h ↦ ⟨s(Sum.inl ⟨v, ⋯⟩, Sum.inr ⟨u, ⋯⟩), ⋯⟩)
        ⋯

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
case mk.mk
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
W₁ : Type u_2
W₂ : Type u_3
inst✝ : DecidableRel fun x1 x2 ↦ x1 ∈ x2
hG : G.IsBipartiteWith s t
val✝¹ : Sym2 V
a✝¹ : V × V
property✝¹ : Quot.mk (Sym2.Rel V) a✝¹ ∈ G.edgeSet
val✝ : Sym2 V
a✝ : V × V
property✝ : Quot.mk (Sym2.Rel V) a✝ ∈ G.edgeSet
⊢ (fun x ↦
          match x with
          | ⟨e, he⟩ =>
            Sym2.fromRelNdrec e he
              (fun u v h ↦
                ⋯.by_cases (fun h ↦ ⟨s(Sum.inl ⟨u, ⋯⟩, Sum.inr ⟨v, ⋯⟩), ⋯⟩) fun h ↦
                  ⟨s(Sum.inl ⟨v, ⋯⟩, Sum.inr ⟨u, ⋯⟩), ⋯⟩)
              ⋯)
        ⟨Quot.mk (Sym2.Rel V) a✝¹, property✝¹⟩ =
      (fun x ↦
          match x with
          | ⟨e, he⟩ =>
            Sym2.fromRelNdrec e he
              (fun u v h ↦
                ⋯.by_cases (fun h ↦ ⟨s(Sum.inl ⟨u, ⋯⟩, Sum.inr ⟨v, ⋯⟩), ⋯⟩) fun h ↦
                  ⟨s(Sum.inl ⟨v, ⋯⟩, Sum.inr ⟨u, ⋯⟩), ⋯⟩)
              ⋯)
        ⟨Quot.mk (Sym2.Rel V) a✝, property✝⟩ →
    ⟨Quot.mk (Sym2.Rel V) a✝¹, property✝¹⟩ = ⟨Quot.mk (Sym2.Rel V) a✝, property✝⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i' ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
w : V
hw : G.Adj u w ∧ G.Adj v w
this : G.edist u v ≤ ↑(Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)).length
⊢ G.edist u v ≤ 2

Tactic:
simp_all

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h✝ : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i - 1 ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h✝ : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i + 1 ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
this : p.getVert (i - 1) ≠ p.getVert (i + 1)
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2

Tactic:
simp_all

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this✝ : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : ¬v = p.getVert 2
hadj : ¬G.Adj v (p.getVert 2)
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2

Tactic:
exact ⟨p.adj_snd hnp, p.adj_getVert_succ (hp ▸ hl), hadj, hv⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c v : V
r : ℕ∞
⊢ v ∈ G.ball c r ↔ c ∈ G.ball v r

Tactic:
by
  simp [ball, edist_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i' ∈ {i | i ≤ p.length - 1}

Tactic:
rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i ∈ {i | i ≤ p.length - 1}

Tactic:
rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl2 : p.getVert (i' + 1) = v
hl1 : i' = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
⊢ G.Adj a₁ c.1 ∧ b₁ = c.2 ∨ H.Adj b₁ c.2 ∧ a₁ = c.1

Tactic:
simp_all

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ i ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
rw [Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: case hv
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce {v, w} ⊔ ⊤.induce s ⊔ ⊤.induce t).verts = (⊤.induce (s ∪ t)).verts

Tactic:
· simp only [Subgraph.verts_sup, Subgraph.induce_verts]
    rw [Set.union_assoc]
    simp [Set.insert_subset_iff, Set.singleton_subset_iff, hv, hw]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Finset α
⊢ ¬(hasse α).IsNClique 3 s

Tactic:
⟨hc, hcard⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Finset α
hc : (hasse α).IsClique ↑s
hcard : s.card = 3
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
a : V
p : G.Walk a a
hp₁ : p.IsCycle
hp₂ : p.length = n
x : ℕ
hx : x < n
y : ℕ
hy : y < n
hab : (cycleGraph n).Adj ⟨x, hx⟩ ⟨y, hy⟩
x✝ : x = y
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G'✝ : SimpleGraph V'
G' : G.Subgraph
G'' : G'.coe.Subgraph
u v : ↑G''.verts
hreachable : G''.coe.Reachable u v
⊢ ↑↑u ∈ (Subgraph.coeSubgraph G'').verts

Tactic:
simp_all

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G'✝ : SimpleGraph V'
G' : G.Subgraph
G'' : G'.coe.Subgraph
u v : ↑G''.verts
hreachable : G''.coe.Reachable u v
⊢ ↑↑v ∈ (Subgraph.coeSubgraph G'').verts

Tactic:
simp_all

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this✝ : 3 ≤ p.length
this : p.support.tail.length ≤ 2
⊢ False

Tactic:
rw [List.length_tail, p.length_support] at this

Goal state after:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this✝ : 3 ≤ p.length
this : p.length + 1 - 1 ≤ 2
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : ↑(G.subgraphOfAdj h).verts
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this✝ : s(u, v) = s(↑w, ↑p.snd)
this : s(u, v) = s(↑p.penultimate, ↑w)
⊢ False

Tactic:
simp_all

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
w : ↑(G.subgraphOfAdj h).verts
p : (G.subgraphOfAdj h).coe.Walk w w
hp : p.IsCycle
this✝ : ↑p.penultimate = ↑w ∧ ↑w = ↑p.snd ∨ ↑p.penultimate = ↑p.snd
this : u = ↑p.penultimate ∧ v = ↑w ∨ u = ↑w ∧ v = ↑p.penultimate
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ b ∈ G.edgeFinset, ∃ a, ∃ (ha : a ∈ {default}ᶜ), ((f a).firstDart ⋯).edge = b

Tactic:
simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
⊢ ∀ (x y : V), G.Adj x y → ∃ a, ∃ (h : ¬a = default), ((f a).firstDart ⋯).edge = s(x, y)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
hr : 0 < r
⊢ (turanGraph n r).CliqueFree (r + 1)

Tactic:
cliqueFree_iff

Goal state after:
n r : ℕ
hr : 0 < r
⊢ IsEmpty ((completeGraph (Fin (r + 1))).Copy (turanGraph n r))
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
p : G.Walk u u
hOdd : Odd p.length
h : ¬3 ≤ G.chromaticNumber
h' : G.chromaticNumber ≤ 2
c : G.Coloring (Fin 2) := Nonempty.some ⋯
c' : G.Coloring Bool := (G.recolorOfEquiv finTwoEquiv) c
this : ¬c' u = true ↔ c' u = true
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
⊢ e ∈ G.edgeSet → K

Tactic:
refine Sym2.hrec f (fun a b ↦ ?_) e

Goal state after:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
C : G.EdgeLabeling K
f : (x y : V) → G.Adj x y → K
f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H
e : Sym2 V
a b : V
⊢ f a b ≍ f b a
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: ι : Type u_1
V : ι → Type u_2
⊢ ∀ (a b c : (i : ι) × V i),
    ¬(completeMultipartiteGraph V).Adj a b →
      ¬(completeMultipartiteGraph V).Adj b c → ¬(completeMultipartiteGraph V).Adj a c

Tactic:
simp_all

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case right
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
ha : G.Adj v w
⊢ #G.edgeFinset < #(G.replaceVertex v w).edgeFinset

Tactic:
G.card_edgeFinset_replaceVertex_of_adj ha,

Goal state after:
case right
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
large_eq : fp.part w = large
small_eq : fp.part v = small
ha : G.Adj v w
⊢ #G.edgeFinset < #G.edgeFinset + G.degree v - G.degree w - 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ (∑ w ∈ range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
← card_filter,

Goal state after:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ #({i ∈ range r | c % r ≠ (n + i) % r}) = r - 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ #({i ∈ range r | c % r = (n + i) % r}) + #({i ∈ range r | c % r ≠ (n + i) % r}) = r

Tactic:
card_filter_add_card_filter_not,

Goal state after:
n r c : ℕ
hr : r > 0
this : #({i ∈ range r | c % r = (n + i) % r}) = 1
⊢ #(range r) = r
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
⊢ 0 < G.eccent u ↔ Nontrivial α

Tactic:
by
  rw [pos_iff_ne_zero, ← not_subsingleton_iff_nontrivial, ← eccent_eq_zero_iff]

Goal state after: