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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

Tactic:
by_cases hw : w ∈ s

Goal state after:
case pos
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∈ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

case neg
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∉ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
i : ℕ
hi : i < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert i) ((cons hxy i').getVert (i + 1))

Tactic:
cases i

Goal state after:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
hi : 0 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert 0) ((cons hxy i').getVert (0 + 1))

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert (n✝ + 1)) ((cons hxy i').getVert (n✝ + 1 + 1))
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case refine_1.inl.inr
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
t : Finset β
a : ↥L
ht : ¬∃ b, g b = t
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ t)

Tactic:
· simpa [extend_apply' _ _ _ ht] using! mul_nonneg
        (extend_nonneg (fun a : L ↦ h₃ a) le_rfl _) (extend_nonneg (fun a : L ↦ h₄ a) le_rfl _)

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

Goal state before:
pp: W₁ : Type u_2
W₂ : Type u_3
⊢ Function.Injective fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
by grind [Function.Injective]

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ u ≠ v

pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ ¬G.Adj u v

pp: case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ (G.commonNeighbors u v).Nonempty

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
⊢ G.edist u v ≤ 2

pp: case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v

Tactic:
· simp +decide [← G.edist_eq_zero_iff.not (b := u = v), h]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ ¬G.Adj u v

case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ (G.commonNeighbors u v).Nonempty

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
⊢ G.edist u v ≤ 2

case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ i ∈ {i | i ≤ p.length}

Tactic:
Set.mem_ofPred

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ i ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ 0 ∈ {i | i ≤ p.length}

Tactic:
Set.mem_ofPred

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ 0 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ i + 1 ∈ {i | i ≤ p.length}

Tactic:
Set.mem_ofPred

Goal state after:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ i + 1 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ 0 ∈ {i | i ≤ p.length}

Tactic:
Set.mem_ofPred

Goal state after:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ 0 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
⊢ (G □ H).neighborSet x = G.neighborSet x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ H.neighborSet x.2

Tactic:
by
  ext ⟨a', b'⟩
  simp only [mem_neighborSet, Set.mem_union, boxProd_adj, Set.mem_prod, Set.mem_singleton_iff]
  simp only [eq_comm, and_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this✝ : Nonempty α
this : Nonempty β
⊢ H.Connected

Tactic:
exact ⟨h.preconnected.ofBoxProdRight⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
x : V
hp : p.length + (#(s.erase x) + 1) = n
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
⊢ (p.takeUntil x hx).length + #(s.erase x) < n

Tactic:
have := p.length_takeUntil_le_length hx

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u : V
n : ℕ
ih :
  ∀ m < n,
    ∀ {v : V} {p : G.Walk u v} (s : Finset V),
      {x ∈ s | x ∈ p.support}.Nonempty →
        p.length + #s = m → ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
v : V
p : G.Walk u v
s : Finset V
x : V
hp : p.length + (#(s.erase x) + 1) = n
hxs : x ∈ s
hx : x ∈ p.support
h : {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support}.Nonempty
this : (p.takeUntil x hx).length ≤ p.length
⊢ (p.takeUntil x hx).length + #(s.erase x) < n
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: case inl
V✝ : Type u_1
G✝ : SimpleGraph V✝
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⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨x, hx⟩ - ⟨y, hy⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

pp: case inr
V✝ : Type u_1
G✝ : SimpleGraph V✝
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⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨y, hy⟩ - ⟨x, hx⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]

Tactic:
· simp_rw [show x = y + 1 by grind [Fin.sub_val_of_le]]
        exact p.isChain_adj_support.getElem _ _ |>.symm

Goal state after:
case inr
V✝ : Type u_1
G✝ : SimpleGraph V✝
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⟩
hne : x ≠ y
hle : x > y
hab : ↑(⟨y, hy⟩ - ⟨x, hx⟩) = 1
⊢ G.Adj p.support[⟨x, hx⟩.succ] p.support[⟨y, hy⟩.succ]
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

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

Tactic:
by
  rcases Hs.eq_empty_or_nonempty with rfl | hnemp
  · simp
  · intro u p hp
    obtain ⟨H, hH, hpH⟩ := p.exists_mem_contains_edges_of_directed Hs hnemp h_dir
    exact h_acyc H hH (p.transfer H hpH) <| Walk.IsCycle.transfer hp hpH

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
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
inhabit V

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
⊢ G.edgeFinset.card + 1 = Fintype.card V
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 : ℕ
s✝ t✝ : V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
hd : G.degree t < G.degree s
⊢ #G.edgeFinset < #(G.replaceVertex s t).edgeFinset

Tactic:
have := G.card_edgeFinset_replaceVertex_of_not_adj hn

Goal state after:
case right
V : Type u_1
inst✝² : Fintype V
G✝ : SimpleGraph V
inst✝¹ : DecidableRel G✝.Adj
r : ℕ
s✝ t✝ : V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
hd : G.degree t < G.degree s
this : #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t
⊢ #G.edgeFinset < #(G.replaceVertex s t).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case pos
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ↑u = n + 2 - 1
hv : ↑v = n + 2 - 1
⊢ 2 ≠ 2

pp: case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ↑u = n + 2 - 1
hv : ¬↑v = n + 2 - 1
⊢ 2 ≠ ⟨↑v % 2, ⋯⟩

pp: case pos
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ 2

pp: case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ ⟨↑v % 2, ⋯⟩

Tactic:
· simp [Fin.eq_mk_iff_val_eq.mpr hu, Fin.eq_mk_iff_val_eq.mpr hv] at hadj

Goal state after:
case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ↑u = n + 2 - 1
hv : ¬↑v = n + 2 - 1
⊢ 2 ≠ ⟨↑v % 2, ⋯⟩

case pos
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ 2

case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ ⟨↑v % 2, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ ∑ x, #((turanGraph (n + r) r).neighborFinset x) =
    ∑ x, #((turanGraph n r).neighborFinset x) + 2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
neighborFinset_eq_filter,

Goal state after:
n r : ℕ
⊢ ∑ x, #{w | (turanGraph (n + r) r).Adj x w} = ∑ x, #{w | (turanGraph n r).Adj x w} + 2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
v : Fin (n + r)
| ∑ i, if ↑v % r ≠ ↑i % r then 1 else 0

Tactic:
Fin.sum_univ_eq_sum_range fun w ↦ if v % r ≠ w % r then 1 else 0,

Goal state after:
n r : ℕ
v : Fin (n + r)
| ∑ i ∈ range (n + r), if ↑v % r ≠ i % r then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

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

Tactic:
simp_rw [mem_map, mem_univ, Embedding.coeFn_mk, true_and] at h

Goal state after:
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 : ∃ a, map { toFun := fun j ↦ f (a, j), inj' := ⋯ } univ = p✝
⊢ #p✝ = t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) * (n' / r) ^ 2 / 2) =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * (n' / r + 1) ^ 2 / 2

Tactic:
← Nat.div_mul_right_comm rd,

Goal state after:
case inr.inr.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) / 2 * (n' / r) ^ 2) =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * (n' / r + 1) ^ 2 / 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) / 2 * (n' / r) ^ 2) =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) * (n' / r + 1) ^ 2 / 2

Tactic:
← Nat.div_mul_right_comm rd,

Goal state after:
case inr.inr.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
⊢ n' * (r - 1) + r.choose 2 + (n' % r * (n' / r) * (r - 1) + r * (r - 1) / 2 * (n' / r) ^ 2) =
    n' % r * (n' / r + 1) * (r - 1) + r * (r - 1) / 2 * (n' / r + 1) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
⊢ s(↑⟨v, ⋯⟩, Exists.choose ⋯) = s(v, w)

Tactic:
← h hvw.fst_mem |>.choose_spec.right w hvw

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
⊢ s(↑⟨v, ⋯⟩, w) = s(v, w)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
i j : ℕ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ ∑ x ∈ X, #(G.neighborFinset x ∩ W) + ∑ x ∈ Xᶜ, #(G.neighborFinset x ∩ W) ≤ #X * (#W - i) + #Xᶜ * (#W - j)

Tactic:
neighborFinset_eq_filter,

Goal state after:
α : Type u_1
G : SimpleGraph α
i j : ℕ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ ∑ x ∈ X, #({w | G.Adj x w} ∩ W) + ∑ x ∈ Xᶜ, #({w | G.Adj x w} ∩ W) ≤ #X * (#W - i) + #Xᶜ * (#W - j)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
hv : v✝ ∈ (G.subgraphOfAdj h).verts
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1

Tactic:
rw [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at hv

Goal state after:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
hv : v✝ = v ∨ v✝ = w
⊢ ∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hv : v ∈ s
⊢ G.Adj v ↑(f ⟨v, hv⟩)

Tactic:
exact hadj ⟨v, _⟩

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(G.degree a)

Tactic:
← sum_incMatrix_apply

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ∑ e, incMatrix R G a e
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M₁ : G.Subgraph
h₁ : M₁ ∈ Set.ofPred IsMatching
M₂ : G.Subgraph
h₂ : M₂ ∈ Set.ofPred IsMatching
h : M₁.edgeSet = M₂.edgeSet
⊢ ⋃ e ∈ M₁.edgeSet, ↑e = M₂.verts

Tactic:
h₂.verts_eq_biUnion_edgeSet,

Goal state after:
V : Type u_1
G : SimpleGraph V
M₁ : G.Subgraph
h₁ : M₁ ∈ Set.ofPred IsMatching
M₂ : G.Subgraph
h₂ : M₂ ∈ Set.ofPred IsMatching
h : M₁.edgeSet = M₂.edgeSet
⊢ ⋃ e ∈ M₁.edgeSet, ↑e = ⋃ e ∈ M₂.edgeSet, ↑e
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = ∑ v, M.coe.degree v

Tactic:
simp [h, Finset.card_univ]

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

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a b : α
h : a = b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = ↑(G.degree a)

Tactic:
subst b

Goal state after:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
a : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(G.degree a)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case pos
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun w ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun w ↦ M'.Adj v w) y → y = w'
hww' : w = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Tactic:
simp_all [← imp_iff_not_or]

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

Goal state before:
pp: case pos
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : G'.Adj v w
⊢ ∃! w, ⊤.Adj v w

Tactic:
obtain ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj h
    have hmadj : M.Adj v w ↔ ¬M.Adj v w' := by simpa using hG' hw'.1 h hw'.2
    use w'
    simp only [Subgraph.top_adj, SimpleGraph.sup_adj, sdiff_adj, Subgraph.spanningCoe_adj,
      hmadj.mp hw.1, hw'.2, not_true_eq_false, and_self, not_false_eq_true, or_true, true_and]
    rintro y (hl | hr)
    · grind
    · obtain ⟨w'', hw''⟩ := hG'cyc.other_adj_of_adj hr.1
      by_contra! hc
      simp_all [show M.Adj v y ↔ ¬M.Adj v w' by simpa using hG' hc hr.1 hw'.2]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
⊢ Disjoint M1.verts M2.verts

Tactic:
Subgraph.verts_iSup,

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
⊢ Disjoint M1.verts (⋃ i, (complMatch i).verts)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α × β → σ
⊢ Primrec₂ (Function.curry f) ↔ Primrec f

Tactic:
← uncurry,

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α × β → σ
⊢ Primrec (Function.uncurry (Function.curry f)) ↔ Primrec f