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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ right.toRight
j : V
hj : j ∈ right.toRight
⊢ Sum.inr i = Sum.inr j → i = j

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n✝ : ℕ
u v : V
n : ℕ
w : ↑(G.neighborSet u)
x✝¹ x✝ : G.Walk (↑w) v
⊢ (fun p ↦ Walk.cons ⋯ p) x✝¹ = (fun p ↦ Walk.cons ⋯ p) x✝ → x✝¹ = x✝

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ left.toRight
j : V
hj : j ∈ left.toRight
⊢ Sum.inr i = Sum.inr j → i = j

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ right.toLeft
j : V
hj : j ∈ right.toLeft
⊢ Sum.inl i = Sum.inl j → i = j

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ∀ ⦃v w : V ⊕ V⦄,
    G.bipartiteDoubleCover.Adj v w →
      v ∈ {v | v.isLeft = true} ∧ w ∈ {w | w.isRight = true} ∨ v ∈ {w | w.isRight = true} ∧ w ∈ {v | v.isLeft = true}

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
s : Set G
u v d : G
⊢ (circulantGraph s).Adj (u + d) (v + d) ↔ (circulantGraph s).Adj u v

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
u v u✝ : V
⊢ ∀ e ∈ nil.edges, e ∈ hHs.some.edgeSet

Tactic:
simp

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

Goal state before:
pp: case inl
V : Type u_1
h_acyc : ∀ H ∈ ∅, H.IsAcyclic
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) ∅
⊢ (sSup ∅).IsAcyclic

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u✝ : V
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) nil.edges
⊢ nil.IsPath

Tactic:
simp

Goal state after:
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
a : V
ha : a ∈ {default}ᶜ
⊢ ((f a).firstDart ⋯).edge ∈ G.edgeFinset

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
f : W → V
⊢ ∀ {a b : W}, ⋯.toGraph.Adj a b → h.toGraph.Adj (f a) (f b)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
f : W ↪ V
⊢ ∀ {a b : W}, h.toGraph.Adj (f a) (f b) ↔ ⋯.toGraph.Adj a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
f : V ≃ W
⊢ ∀ {a b : W}, h.toGraph.Adj (f.symm a) (f.symm b) ↔ ⋯.toGraph.Adj a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝¹ : Zero α
inst✝ : One α
i✝ j✝ : V
⊢ adjMatrix α ⊥ i✝ j✝ = 0 i✝ j✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
⊢ (adjMatrix α G).diag = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Zero α
inst✝¹ : One α
H : SimpleGraph W
inst✝ : DecidableRel H.Adj
f : G ↪g H
i✝ j✝ : V
⊢ (adjMatrix α H).submatrix (⇑f) (⇑f) i✝ j✝ = adjMatrix α G i✝ j✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : MulZeroOneClass α
⊢ adjMatrix α G ⊙ adjMatrix α G = adjMatrix α G

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
i : V
⊢ (adjMatrix α G * adjMatrix α G) i i = ↑(G.degree i)

Tactic:
by simp [filter_true_of_mem]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
a : α
v : V
⊢ (adjMatrix α G *ᵥ Function.const V a) v = ↑(G.degree v) * a

Tactic:
simp

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

Goal state before:
pp: case refine_2
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
h : G.Adj x y
h' : (f x).length ≤ (f y).length
⊢ ((cons ⋯ (f x)).firstDart ⋯).toProd = (y, x)

Tactic:
simp

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

Goal state before:
pp: n r : ℕ
hr : 0 < r
f : (completeGraph (Fin (r + 1))).Copy (turanGraph n r)
⊢ Fintype.card (Fin r) < Fintype.card (Fin (r + 1))

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v u✝ : α
⊢ Even Walk.nil.length ↔ (c u✝ = true ↔ c u✝ = true)

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
⊢ ¬G.Adj t u

Tactic:
have dst := h.degree_eq_of_not_adj hst

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
⊢ ¬G.Adj t u
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Infinite V
⊢ Nat.card V ≤ Nat.card ↑G.edgeSet + 1

Tactic:
simp

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

Goal state before:
pp: case a
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
⊢ 3 ≤ (cycleGraph n).chromaticNumber

Tactic:
have hn3 : n - 3 + 3 = n := by
      refine Nat.sub_add_cancel (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne h ?_))
      intro h2
      rw [← h2] at hOdd
      exact (Nat.not_odd_iff.mpr rfl) hOdd
    let w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)
    have hOdd' : Odd w.length := by
      rw [cycleGraph.length_cycle, hn3]
      exact hOdd
    rw [← hn3]
    exact Walk.three_le_chromaticNumber_of_odd_loop w hOdd'

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 : TopEdgeLabeling V K
f : V' ↪ V
⊢ ∀ {a b : V'}, ⊤.Adj a b → ⊤.Adj (f a) (f b)

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
⊢ ∀ (x : V), ¬G.Adj x x

Tactic:
simp

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

Goal state before:
pp: α : Type u
⊢ ∀ (a b c : α), ¬⊥.Adj a b → ¬⊥.Adj b c → ¬⊥.Adj a c

Tactic:
simp

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
⊢ ∀ {a b : Fin r × Fin t},
    (SimpleGraph.completeMultipartiteGraph (const (Fin r) (Fin t))).Adj ((Equiv.sigmaEquivProd (Fin r) (Fin t)).symm a)
        ((Equiv.sigmaEquivProd (Fin r) (Fin t)).symm b) ↔
      (completeEquipartiteGraph r t).Adj a b

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
v w : V
⊢ G.Reachable v w ↔ v ∈ (G.connectedComponentMk w).supp

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
huv : u ≠ v
n : ℕ
hn : 2 ≤ n
h✝ : G.IsEdgeReachable n u v
w : V
hw : G.Adj u w
h : G.IsEdgeReachable 2 u w
⊢ {s(u, w)}.encard < ↑2

Tactic:
simp

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

Goal state before:
pp: case a
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑v.2 * r ≤ ↑⟨↑v.2 * r + ↑v.1, ⋯⟩

Tactic:
exact Nat.le_add_right (↑v.2 * r) ↑v.1

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

Goal state before:
pp: r t : ℕ
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nat.succ 1 ≤ r ∧ t ≠ 0

Tactic:
← Fin.nontrivial_iff_two_le,

Goal state after:
r t : ℕ
⊢ (completeEquipartiteGraph r t).edgeSet.Nonempty ↔ Nontrivial (Fin r) ∧ t ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case map_rel_iff'
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
⊢ ↑(zm ⟨a, ⋯⟩) % r ≠ ↑(zm ⟨b, ⋯⟩) % r ↔ G.Adj a b

Tactic:
have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩

Goal state after:
case map_rel_iff'
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this :
  h.finpartition.part ↑⟨a, ⋯⟩ = h.finpartition.part ↑⟨b, ⋯⟩ ↔
    ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
⊢ ↑(zm ⟨a, ⋯⟩) % r ≠ ↑(zm ⟨b, ⋯⟩) % r ↔ G.Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
⊢ ∀ {p : Finset V}, p ∈ ∅ → #p = t

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
h : r = 0 ∨ t = 0
⊢ (↑∅).Pairwise fun x1 x2 ↦ G.IsCompleteBetween ↑x1 ↑x2

Tactic:
simp

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

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
| n

Tactic:
rw [← Fintype.card_fin n]

Goal state after:
n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
| Fintype.card (Fin n)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inl
n c : ℕ
⊢ (∑ w ∈ range 0, if c % 0 ≠ (n + w) % 0 then 1 else 0) = 0 - 1

Tactic:
simp

Goal state after:
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}) = r - #({i ∈ range r | c % r = (n + i) % r})

Tactic:
apply Nat.eq_sub_of_add_eq'

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}) + #({i ∈ range r | c % r ≠ (n + i) % r}) = r
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : t = 0
⊢ ∀ {p : Finset V}, p ∈ ∅ → #p = t

Tactic:
simp

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : t = 0
⊢ (↑∅).Pairwise fun x1 x2 ↦ G.IsCompleteBetween ↑x1 ↑x2

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ¬G.Connected
⊢ G.ediam = ⊤

Tactic:
by
  rw [connected_iff_exists_forall_reachable] at h
  push Not at h
  obtain ⟨_, hw⟩ := h Classical.ofNonempty
  rw [eq_top_iff, ← edist_eq_top_of_not_reachable hw]
  exact edist_le_ediam

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

Goal state before:
pp: case h
α : Type u_1
G : SimpleGraph α
inst✝¹ : Nonempty α
inst✝ : Finite α
w : α
hw : G.eccent w = G.radius
v : α
hv : G.edist w v = G.eccent w
⊢ G.eccent w = G.radius

Tactic:
hw

Goal state after:
case h
α : Type u_1
G : SimpleGraph α
inst✝¹ : Nonempty α
inst✝ : Finite α
w : α
hw : G.eccent w = G.radius
v : α
hv : G.edist w v = G.eccent w
⊢ G.radius = G.radius
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
i₁ i₂ : Fin r
h :
  (fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ) i₁ =
    (fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ) i₂
⊢ i₁ = i₂

pp: case neg.refine_3
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
⊢ #(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ) = r ∨ t = 0

pp: case neg.refine_4
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
p✝ : Finset V
h : p✝ ∈ map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ
⊢ #p✝ = t

pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ : Finset V
h₁ : x✝³ ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
x✝² : Finset V
h₂ : x✝² ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
hne : x✝³ ≠ x✝²
x✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
⊢ G.Adj x✝¹ x✝

Tactic:
· simp_rw [Finset.ext_iff] at h
      have : NeZero t := ⟨ht⟩
      obtain ⟨_, heq⟩ : ∃ j, f (i₁, j) = f (i₂, 0) := by simpa using h <| f (i₂, 0)
      apply f.injective at heq
      rw [Prod.mk.injEq] at heq
      exact heq.left

Goal state after:
case neg.refine_3
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
⊢ #(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ) = r ∨ t = 0

case neg.refine_4
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
p✝ : Finset V
h : p✝ ∈ map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ
⊢ #p✝ = t

case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ : Finset V
h₁ : x✝³ ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
x✝² : Finset V
h₂ : x✝² ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
hne : x✝³ ≠ x✝²
x✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a.e_a
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = 2 * r.choose 2

Tactic:
· rw [mul_comm 2, Nat.choose_two_right, Nat.div_two_mul_two_of_even (Nat.even_mul_pred_self r)]
    conv_rhs => enter [1]; rw [← card_range r]
    rw [← smul_eq_mul, ← sum_const]
    congr!; exact sum_ne_add_mod_eq_sub_one

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

Goal state before:
pp: case neg.refine_3
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
⊢ #(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ) = r ∨ t = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L M : Set V
x✝¹ Y Z : (Finset V)ᵒᵖ
h : x✝¹ ⟶ Y
h' : Y ⟶ Z
C : G.ComponentCompl ↑(Opposite.unop x✝¹)
x✝ : V
⊢ x✝ ∈ ((ConcreteCategory.hom (↾ComponentCompl.hom ⋯)).toFun C).supp ↔
    x✝ ∈ ((ConcreteCategory.hom (↾ComponentCompl.hom ⋯ ≫ ↾ComponentCompl.hom ⋯)).toFun C).supp

Tactic:
simp

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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
v : V
⊢ (G.singletonSubgraph v).verts.Finite

Tactic:
simp

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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
u v : V
e : G.Adj u v
⊢ (G.subgraphOfAdj e).verts.Finite

Tactic:
simp

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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v : V
⊢ v ∈ (↑(Opposite.unop (Opposite.op ⟨G.singletonSubgraph v, ⋯⟩))).verts

Tactic:
simp

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
| n

Tactic:
rw [← Fintype.card_fin n]

Goal state after:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
| Fintype.card (Fin n)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G H : SimpleGraph α
h : G ≤ H
a : α
w : G.Walk a a
hw : w.IsCycle
⊢ ↑(Walk.mapLe h w).length ≤ ↑w.length

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.egirth = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Finset ι
s : ι → Set α
⊢ ∅.ncard = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Finset ι
s : ι → Set α
⊢ ∅.encard = 0

Tactic:
simp

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

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
| n

Tactic:
rw [← Fintype.card_fin n]

Goal state after:
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
| Fintype.card (Fin n)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).ncard = (⋃ i ∈ univ, s i).ncard

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).encard = (⋃ i ∈ univ, s i).encard

Tactic:
simp

Goal state after: