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

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
h : G ≠ ⊥
⊢ 2 ≤ G.chromaticNumber

Tactic:
· obtain ⟨_, _, h⟩ := ne_bot_iff_exists_adj.mp h
    exact two_le_chromaticNumber_of_adj h

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ Disjoint ↑(G.neighborSet v).toFinset ↑s

Tactic:
Set.coe_toFinset

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ Disjoint (G.neighborSet v) ↑s
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
⊢ Disjoint ↑(G.neighborSet w).toFinset ↑t

Tactic:
Set.coe_toFinset

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
⊢ Disjoint (G.neighborSet w) ↑t
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
i : ℕ
hi : i < w.length
⊢ w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))

Tactic:
by
  induction w generalizing i with
  | nil => cases hi
  | cons hxy i' ih =>
    cases i
    · simp
    · simp only [Walk.toSubgraph, getVert_cons_succ, Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq,
        Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
      right
      exact ih (Nat.succ_lt_succ_iff.mp hi)

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
this✝ : G.dist v w = 1
this : G.dist w v = 1
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

Tactic:
have : G.dist u w ≤ G.dist u v + G.dist v w := hadj.reachable.dist_triangle_right u

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
this✝¹ : G.dist v w = 1
this✝ : G.dist w v = 1
this : G.dist u w ≤ G.dist u v + G.dist v w
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
hh : G.dist u' v' < p₂.length
ru : G.Walk u u'
rv : G.Walk v' v
h : p₁ = (ru.append p₂).append rv
s : G.Walk u' v'
h✝ : s.IsPath ∧ s.length = G.dist u' v'
r : G.Walk u v := (ru.append s).append rv
⊢ False

Tactic:
have : p₁.length = ru.length + p₂.length + rv.length := by simp [h]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h₁ : p₁.length = G.dist u v
hh : G.dist u' v' < p₂.length
ru : G.Walk u u'
rv : G.Walk v' v
h : p₁ = (ru.append p₂).append rv
s : G.Walk u' v'
h✝ : s.IsPath ∧ s.length = G.dist u' v'
r : G.Walk u v := (ru.append s).append rv
this : p₁.length = ru.length + p₂.length + rv.length
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Prod

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

Tactic:
classical
  rintro a₁ a₂
  obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
  exact ⟨w.ofBoxProdLeft⟩

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

Goal state before:
pp: case h
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
hp : p.length + #s = n
x : V
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 + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}.erase x ⊆ ∅
⊢ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅

Tactic:
erase_eq_of_notMem

Goal state after:
case h
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
hp : p.length + #s = n
x : V
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 + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅
⊢ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support} ⊆ ∅

case h
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
hp : p.length + #s = n
x : V
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 + #(s.erase x) < n
y : V
hys : y ∈ s.erase x
hyp : y ∈ (p.takeUntil x hx).support
h : {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}.erase x ⊆ ∅
⊢ x ∉ {t ∈ s.erase y | t ∈ (p.takeUntil y ⋯).support}
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case mpr
V : Type u_1
G : SimpleGraph V
⊢ (Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath) → G.Connected ∧ ∀ (u v : V) (x y : G.Path u v), x = y

Tactic:
rintro ⟨hV, h⟩
    refine ⟨Connected.mk ?_, ?_⟩
    · intro v w
      obtain ⟨p, _⟩ := h v w
      exact p.reachable
    · rintro v w ⟨p, hp⟩ ⟨q, hq⟩
      simp only [ExistsUnique.unique (h v w) hp hq]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
⊢ (∀ (b : SimpleGraph V), H.Free b → #b.edgeFinset ≤ m) ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m

Tactic:
exact ⟨fun h _ _ h' ↦ by convert! h _ h', fun h _ h' ↦ by convert! h h'⟩

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

Goal state before:
pp: n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
⊢ ∀ ⦃G : SimpleGraph (Fin n)⦄ [inst : DecidableRel G.Adj],
    H'.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H

Tactic:
intro _ _ h'

Goal state after:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
G✝ : SimpleGraph (Fin n)
inst✝ : DecidableRel G✝.Adj
h' : H'.Free G✝
⊢ #G✝.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ A.compl i j = 0 ∨ A.compl i j = 1

Tactic:
by
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
  without the `simp`. This is probably a problem at Mathlib's end rather than `grind`'s,
  as we are relying on seeing through the definition of `Matrix`, and `of`. -/
  simp [compl]
  grind

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
⊢ (G ⊔ edge u v).IsAcyclic → G.IsAcyclic ∧ (G.Reachable u v → u = v ∨ G.Adj u v)

Tactic:
refine fun hacyc ↦ ⟨hacyc.anti le_sup_left, fun hreach ↦ False.elim ?_⟩

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
hadj : ¬G.Adj u v
hacyc : (G ⊔ edge u v).IsAcyclic
hreach : G.Reachable u v
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ ∃! w, G.Adj u w

Tactic:
refine ⟨_, p.adj_snd hnil, fun w hadj ↦ ?_⟩

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
w : V
hadj : (fun w ↦ G.Adj u w) w
⊢ w = p.snd
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ Set.univ.PairwiseDisjoint C.labelGraph

Tactic:
intro _ _ _ _ h

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
x✝ : K
a✝¹ : x✝ ∈ Set.univ
y✝ : K
a✝ : y✝ ∈ Set.univ
h : x✝ ≠ y✝
⊢ Function.onFun Disjoint C.labelGraph x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj (e 0) (e 1)
⊢ False

Tactic:
have h1 : ¬ G.Adj (e 1) (e 2) := by simp [pathGraph_adj]

Goal state after:
α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj (e 0) (e 1)
h1 : ¬G.Adj (e 1) (e 2)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
⊢ G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1

Tactic:
grind [dist_ne_of_adj, Adj.diff_dist_adj]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsTree
u v w : V
hadj : G.Adj v w
⊢ G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1

Tactic:
grind [dist_ne_of_adj, Adj.diff_dist_adj]

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : G.Reachable u v
p : G.Path u v
⊢ ↑p ∈ G.finsetWalkLength (↑⟨(↑p).length, ⋯⟩) u v

Tactic:
simp [mem_finsetWalkLength_iff]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ n ≥ 3, (cycleGraph n).Free G

Tactic:
by
  refine ⟨fun h n hn hle ↦ ?_, fun h v p hcyc ↦ h p.length hcyc.three_le_length ?_⟩
  · have ⟨v, p, hcyc, hlen⟩ := cycleGraph_isContained_iff hn |>.mp hle
    exact h p hcyc
  · exact cycleGraph_isContained_iff hcyc.three_le_length |>.mpr ⟨v, p, hcyc, rfl⟩

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

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ (c ∈ univ ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (c ∈ univ ∧ c.supp ⊆ c'.supp) ∧ Odd (↑(filter (Membership.mem c.supp) univ)).ncard

Tactic:
coe_filter,

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ (c ∈ univ ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (c ∈ univ ∧ c.supp ⊆ c'.supp) ∧ Odd {x | x ∈ univ ∧ x ∈ c.supp}.ncard
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:
mul_comm 2,

Goal state after:
case e_a.e_a
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = r.choose 2 * 2
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
hr : ¬G.radius = ⊤
w : α
hw : G.eccent w = G.radius
⊢ ¬G.ediam = ⊤

Tactic:
have hdiam : G.ediam ≤ 2 * G.eccent w := ediam_le_two_mul_eccent w

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
hr : ¬G.radius = ⊤
w : α
hw : G.eccent w = G.radius
hdiam : G.ediam ≤ 2 * G.eccent w
⊢ ¬G.ediam = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
⊢ G.ediam ≤ 2 * G.radius

Tactic:
· by_cases hdiam : G.ediam = ⊤
    · simp [hdiam, ediam_eq_top_iff_radius_eq_top.mp hdiam]
    · obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius
      obtain ⟨_, _, h⟩ := G.exists_edist_eq_ediam_of_ne_top hdiam
      apply le_trans (h ▸ G.edist_triangle (v := w))
      rw [two_mul]
      exact hw ▸ add_le_add (G.edist_comm ▸ G.edist_le_eccent) G.edist_le_eccent

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
⊢ Pairwise fun C D ↦ Disjoint ↑C ↑D

Tactic:
rintro C D ne
  rw [Set.disjoint_iff]
  exact fun u ⟨uC, uD⟩ => ne (uC.choose_spec.symm.trans uD.choose_spec)

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑(#G.edgeFinset * (n - 1)) ≤ (↑n + 1) * ↑(extremalNumber n H)

Tactic:
← Nat.cast_add_one,

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑(#G.edgeFinset * (n - 1)) ≤ ↑(n + 1) * ↑(extremalNumber n H)
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
__IsCycle✝ : (Walk.map f (cons y p)).IsCycle := IsCycle.map (Bijective.injective hf) (isCycle hp)
⊢ List.count (f x) (List.map (⇑f) p.support) = 1

Tactic:
rw [List.count_map_of_injective _ _ hf.injective]

Goal state after:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
__IsCycle✝ : (Walk.map f (cons y p)).IsCycle := IsCycle.map (Bijective.injective hf) (isCycle hp)
⊢ List.count x p.support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle

Tactic:
cases (finite_or_infinite α).symm

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
h✝ : Infinite α
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle

case inr
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a v : α
p : G.Walk a a
hv : v ∈ p.support
h✝ : Finite α
⊢ (p.rotate v hv).IsHamiltonianCycle ↔ p.IsHamiltonianCycle
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
h : e ∉ G.incidenceSet a
⊢ incMatrix R G a e = 0

Tactic:
by
  rw [incMatrix_apply, Set.indicator_of_notMem h]

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 : α
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(G.degree a)

Tactic:
exact incMatrix_mul_transpose_diag (R := R) G

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
R : Type u_3
inst✝ : AddCommMonoidWithOne R
i : V
⊢ ↑(#{w | G.Adj i w}.toFinset) = ∑ j, if G.Adj i j then 1 else 0

Tactic:
rw [sum_boole, Set.toFinset_ofPred]

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
e : ↑G.edgeSet
⊢ Sym2.map ⇑f ↑e ∈ G'.edgeSet

Tactic:
by rcases e with ⟨⟨⟩, h⟩; exact f.toHom.map_adj h

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

Goal state before:
pp: case neg.inr.inl
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

pp: case neg.inr.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
· rw [G'.adj_congr_of_sym2 (by grind : s(v, w) = s(u, x))]
    simp only [hnadj, false_iff, not_not]
    rcases hr.1 with ⟨rfl, rfl⟩ | ⟨hrr1, hrr2⟩
    · exact (hx' _ hww'.symm h1.symm).symm
    · grind

Goal state after:
case neg.inr.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case refine_2
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
⊢ #(Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ) = r ∨ t = 0

Tactic:
simp_rw [card_map, card_univ, card_coe]

Goal state after:
case refine_2
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
⊢ #K.parts = r ∨ t = 0
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: p : ℕ
⊢ unpaired
      (fun z n ↦
        Nat.rec 1
          (fun y IH ↦
            unpaired (fun x1 x2 ↦ x1 * x2)
              (Nat.pair (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2 (unpair (Nat.pair z (Nat.pair y IH))).1))
          n)
      p =
    unpaired (fun x1 x2 ↦ x1 ^ x2) p

Tactic:
by
    simp; induction p.unpair.2 <;> simp [*, Nat.pow_succ]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ.nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH : ∀ (l : List β) (x : σ), (G a)^[n] (x, l) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take n l), List.drop n l)
x : σ
⊢ (G a)^[n] (G a (x, [])) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take (n + 1) []), List.drop (n + 1) [])

Tactic:
simp [G, IH]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ.cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH : ∀ (l : List β) (x : σ), (G a)^[n] (x, l) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take n l), List.drop n l)
x : σ
b : β
l : List β
⊢ (G a)^[n] (G a (x, b :: l)) =
    (List.foldl (fun s b ↦ h a (s, b)) x (List.take (n + 1) (b :: l)), List.drop (n + 1) (b :: l))

Tactic:
simp [G, IH]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
⊢ (rfindOpt f).Dom

Tactic:
have fd : (rfind fun n => (f n).isSome).Dom :=
      ⟨Nat.find h', by simpa using s.symm, fun _ _ => trivial⟩

Goal state after:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
fd : (rfind fun n ↦ ↑(Option.some (f n).isSome)).Dom
⊢ (rfindOpt f).Dom
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ (Nat.casesOn (encode (o a)) (Option.some (f a)) fun n ↦ Option.map (g a) (decode n)) =
    Option.some (Option.casesOn (o a) (f a) (g a))

Tactic:
cases o a

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ (Nat.casesOn (encode Option.none) (Option.some (f a)) fun n ↦ Option.map (g a) (decode n)) =
    Option.some (Option.casesOn Option.none (f a) (g a))

case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
val✝ : β
⊢ (Nat.casesOn (encode (Option.some val✝)) (Option.some (f a)) fun n ↦ Option.map (g a) (decode n)) =
    Option.some (Option.casesOn (Option.some val✝) (f a) (g a))