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

Goal state before:
pp: n : ℕ
h : Even n
⊢ ∀ {v w : Fin n}, (cycleGraph n).Adj v w → decide (↑v % 2 = 0) ≠ decide (↑w % 2 = 0)

Tactic:
by
    intro u v hadj
    match n with
    | 0 => exact u.elim0
    | 1 => simp at h
    | n + 2 =>
      simp only [ne_eq, decide_eq_decide]
      simp only [cycleGraph_adj] at hadj
      cases hadj with
      | inl huv | inr huv =>
        rw [← add_eq_of_eq_sub' huv.symm, ← Fin.even_iff_mod_of_even h,
          ← Fin.even_iff_mod_of_even h, Fin.even_add_one_iff_odd]
        apply Classical.not_iff.mpr
        simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
⊢ G.minDegree = 1

Tactic:
by
  by_cases q : 2 ≤ G.minDegree
  · have := h.card_edgeFinset
    have := G.sum_degrees_eq_twice_card_edges
    have hle : ∑ v : V, 2 ≤ ∑ v, G.degree v := by
      gcongr
      exact le_trans q (G.minDegree_le_degree _)
    rw [Finset.sum_const, Finset.card_univ, smul_eq_mul] at hle
    lia
  · have := h.preconnected.minDegree_pos_of_nontrivial
    lia

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w✝ : α
hv : w✝ ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he : Fin.ofNat 2 (Nonempty.some ⋯).length = Fin.ofNat 2 (Nonempty.some ⋯).length
⊢ (Nonempty.some ⋯).length % 2 = (Nonempty.some ⋯).length % 2

Tactic:
← Fin.val_natCast,

Goal state after:
α : Type u_1
G : SimpleGraph α
h : ∀ (u : α) (w : G.Walk u u), ¬Odd w.length
c : G.ConnectedComponent
w✝ : α
hv : w✝ ∈ c.supp
a b : ↥c
hab : c.toSimpleGraph.Adj a b
he : Fin.ofNat 2 (Nonempty.some ⋯).length = Fin.ofNat 2 (Nonempty.some ⋯).length
⊢ ↑↑(Nonempty.some ⋯).length = ↑↑(Nonempty.some ⋯).length
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this : z = v
⊢ False

Tactic:
subst_vars

Goal state after:
case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ EdgeLabeling.labelGraph G.toTopEdgeLabeling 1 = G

Tactic:
by ext x y; simpa [imp_false] using G.ne_of_adj

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

Goal state before:
pp: case map_rel_iff'.inr
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 : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
lc : ∀ (x : V), ↑(zm ⟨x, ⋯⟩) < Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) = ↑(zm ⟨b, ⋯⟩) % Fintype.card V

Tactic:
Nat.mod_eq_of_lt (lc b),

Goal state after:
case map_rel_iff'.inr
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 : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
lc : ∀ (x : V), ↑(zm ⟨x, ⋯⟩) < Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) = ↑(zm ⟨b, ⋯⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ ⊤.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) ⊤ ↔
    Nonempty (G ≃g turanGraph (Fintype.card V) (Fintype.card α - 1))

Tactic:
← isTuranMaximal_iff_nonempty_iso_turanGraph (Nat.sub_pos_iff_lt.mpr one_lt_card),

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ ⊤.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) ⊤ ↔ G.IsTuranMaximal (Fintype.card α - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ (c.supp \ s).ncard = c.supp.ncard - 1

Tactic:
by
  obtain ⟨a, ha⟩ := exists_inter_eq_singleton hrep h
  rw [← Set.sdiff_inter_self_eq_sdiff, ha, Set.ncard_sdiff, Set.ncard_singleton]
  simp [← ha]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u v w : α
⊢ G.edist v u + G.edist u w = G.edist u v + G.edist u w

Tactic:
by rw [edist_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
⊢ ⊤.diam = 1

Tactic:
rw [diam, ediam_top, ENat.toNat_one]

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

Goal state before:
pp: n r : ℕ
⊢ #(turanGraph n r).edgeFinset = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
rcases r.eq_zero_or_pos with rfl | hr
  · rw [Nat.mod_zero, tsub_self, zero_mul, Nat.zero_div, zero_add]
    have := card_edgeFinset_top_eq_card_choose_two (V := Fin n)
    rw [Fintype.card_fin] at this; convert! this; exact turanGraph_zero
  · have ring₁ (n) : (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) =
        n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2 := by
      nth_rw 1 [← Nat.mod_add_div n r, Nat.sq_sub_sq, add_tsub_cancel_left,
        show (n % r + r * (n / r) + n % r) * (r * (n / r)) * (r - 1) =
          (2 * ((n % r) * (n / r) * (r - 1)) + r * (r - 1) * (n / r) ^ 2) * r by grind]
      rw [Nat.mul_div_mul_right _ _ hr, Nat.mul_add_div zero_lt_two]
    rcases lt_or_ge n r with h | h
    · rw [Nat.mod_eq_of_lt h, tsub_self, zero_mul, Nat.zero_div, zero_add]
      have := card_edgeFinset_top_eq_card_choose_two (V := Fin n)
      rw [Fintype.card_fin] at this; convert! this
      rw [turanGraph_eq_top]; exact .inr h.le
    · let n' := n - r
      have n'r : n = n' + r := by lia
      rw [n'r, card_edgeFinset_turanGraph_add, card_edgeFinset_turanGraph, ring₁, ring₁,
        add_rotate, ← add_assoc, Nat.add_mod_right, Nat.add_div_right _ hr]
      congr 1
      have rd : 2 ∣ r * (r - 1) := (Nat.even_mul_pred_self _).two_dvd
      rw [← Nat.div_mul_right_comm rd, ← Nat.div_mul_right_comm rd, ← Nat.choose_two_right]
      have ring₂ : n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
          n' % r * (n' / r + 1) * (r - 1) + r.choose 2 +
          r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2 := by grind
      rw [ring₂, ← add_assoc]; congr 1
      rw [← add_rotate, ← add_rotate _ _ (r.choose 2)]; congr 1
      rw [Nat.choose_two_right, Nat.div_mul_cancel rd, mul_add_one, add_mul, ← add_assoc,
        ← add_rotate, add_comm _ (_ * _)]; congr 1
      rw [← mul_rotate, ← add_mul, add_comm, mul_comm _ r, Nat.div_add_mod n' r]

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

Goal state before:
pp: case h₁
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ v ∈ K.vertsᶜ \ filter K t, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤
    ∑ x ∈ K.vertsᶜ \ filter K t, (↑(#K.verts) - ↑t' + ↑t)

Tactic:
refine sum_le_sum (fun v hv ↦ ?_)

Goal state after:
case h₁
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
v : Fin n
hv : v ∈ K.vertsᶜ \ filter K t
⊢ ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ↑(#K.verts) - ↑t' + ↑t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ v ∈ filter K t, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ∑ x ∈ filter K t, ↑(#K.verts)

Tactic:
refine sum_le_sum (fun v hv ↦ ?_)

Goal state after:
case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
v : Fin n
hv : v ∈ filter K t
⊢ ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ↑(#K.verts)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
⊢ G'.egirth ≤ G.egirth

Tactic:
by
  by_cases hacyc : G.IsAcyclic
  · simp [hacyc.egirth_eq_top]
  obtain ⟨a, w, hw, hwl⟩ := exists_egirth_eq_length.mpr hacyc
  rw [hwl, ← w.length_map h.some.toHom]
  exact egirth_le_length <| hw.map h.some.injective

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.girth = w.length) ↔ ¬G.IsAcyclic

Tactic:
refine ⟨by tauto, fun h ↦ ?_⟩
  obtain ⟨_, _, _⟩ := exists_egirth_eq_length.mpr h
  simp_all only [girth, ENat.toNat_natCast]
  tauto

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

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ #(K.parts.pi fun x ↦ powersetCard t x) * t = (∏ x ∈ K.parts, (#x).choose t) * t

Tactic:
Finset.card_pi,

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ (∏ i ∈ K.parts, #(powersetCard t i)) * t = (∏ x ∈ K.parts, (#x).choose t) * t
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inl
α : Type u_1
b✝ : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h2 : G.IsNClique r (insert b✝ s)
h3 : b✝ ∉ s
b : α
h1 : G.IsNClique r (insert b s)
ha : G.Adj b b✝
hb : b ∈ insert b s
⊢ G.Adj b✝ b

pp: case inr
α : Type u_1
a b✝ : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b✝ s)
h3 : b✝ ∉ s
ha : G.Adj a b✝
b : α
hb : b ∈ insert a s
h : b ∈ s
⊢ G.Adj b✝ b

Tactic:
· exact ha.symm

Goal state after:
case inr
α : Type u_1
a b✝ : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b✝ s)
h3 : b✝ ∉ s
ha : G.Adj a b✝
b : α
hb : b ∈ insert a s
h : b ∈ s
⊢ G.Adj b✝ b
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inl.inl
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hcx : C x = C v
y : α
hcy : C y = C v
hx : x = w₁
hy : y = w₂
⊢ False

Tactic:
subst_vars

Goal state after:
case inl.inl
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v : α
t : Finset α
C : G.Coloring (Fin (r + 1))
x : α
hcx : C x = C v
y : α
hcy : C y = C v
h : Set.SurjOn (⇑C) (insert x ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert y ↑t) Set.univ
hw : G.IsFiveWheelLike r k v x y s t
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v✝ : V
hv : v✝ ∈ M.verts
⊢ ∃! w, (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w

Tactic:
obtain ⟨w, hvw, hw⟩ := h hv

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v✝ : V
hv : v✝ ∈ M.verts
w : V
hvw : M.Adj v✝ w
hw : ∀ (y : V), (fun w ↦ M.Adj v✝ w) y → y = w
⊢ ∃! w, (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
⊢ ∀ (w : V), p.toSubgraph.Adj v w ↔ G.Adj v w

Tactic:
refine fun w ↦ Subgraph.adj_iff_of_neighborSet_equiv (?_ : Nonempty _).some (Set.toFinite _)
  have := hp.ncard_neighborSet_toSubgraph_eq_two (by aesop)
  rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _),
    ← Set.cast_ncard (finite_neighborSet_toSubgraph p),
    hcyc
      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
        Set.nonempty_of_ncard_ne_zero <| by simp [this]),
    this]

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'
a✝ b✝ : ↑G.edgeSet
⊢ ¬⟨Sym2.map ⇑f ↑a✝, ⋯⟩ = ⟨Sym2.map ⇑f ↑b✝, ⋯⟩ ↔ ¬a✝ = b✝

Tactic:
Subtype.mk.injEq,

Goal state after:
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
a✝ b✝ : ↑G.edgeSet
⊢ ¬Sym2.map ⇑f ↑a✝ = Sym2.map ⇑f ↑b✝ ↔ ¬a✝ = b✝
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
⊢ G.ediam ≤ 2

Tactic:
rw [ediam_le_iff]
    intro u v
    by_contra! hc
    obtain ⟨hn, ha, he⟩ := two_lt_edist_iff.mp hc
    have h := h.of_not_adj hn ha
    simp_all

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

Goal state before:
pp: case convert_3.e_a.e_a
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset v ∩ G.neighborFinset w) = ℓ

Tactic:
neighborFinset_def,

Goal state after:
case convert_3.e_a.e_a
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : G.Adj v w
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #((G.neighborSet v).toFinset ∩ (G.neighborSet w).toFinset) = ℓ
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #(G.neighborFinset v ∩ G.neighborFinset w) = μ

Tactic:
neighborFinset_def,

Goal state after:
case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ w ≠ v
⊢ #((G.neighborSet v).toFinset ∩ (G.neighborSet w).toFinset) = μ
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
decide_eq_true_eq

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : x = u✝ ∨ x = v✝
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : ∀ (i : Set V), G.IsVertexCover i → ↑n ≤ i.encard
v w : V
x✝ : G.Adj v w
⊢ v ∈ (fun x ↦ (Quot.out x).1) '' G.edgeSet ∨ w ∈ (fun x ↦ (Quot.out x).1) '' G.edgeSet

Tactic:
by grind [Sym2.out_fst_mem s(v, w), mem_edgeSet]

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ g • x ∈ g • ↑pt ↔ x ∈ pt

Tactic:
Set.smul_mem_smul_set_iff,

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ ↑pt ↔ x ∈ pt
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: p : ℕ
⊢ Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2

Tactic:
induction p.unpair.2 <;> simp [*, mul_succ, add_comm _ (unpair p).fst]

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₁ : PrimrecBounded f
h₂ : PrimrecRel fun a b ↦ f a = b
⊢ Primrec f

Tactic:
rcases h₁ with ⟨g, pg, hg : ∀ x, f x ≤ g x⟩
  refine (nat_findGreatest pg h₂).of_eq fun n => ?_
  exact (Nat.findGreatest_spec (P := fun b => f n = b) (hg n) rfl).symm

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inr.inr
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : n < m
⊢ n ∈ rfind p

Tactic:
· injection mem_unique h₁ (rfind_min hm h)

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
⊢ ((Nat.pair <$> (↑(decode n)).bind fun a ↦ map encode (↑f a)) <*> (↑(decode n)).bind fun a ↦ map encode (↑g a)) =
    (↑(decode n)).bind fun a ↦ map encode ((↑fun a ↦ (f a, g a)) a)

Tactic:
by cases decode (α := α) n <;> simp [Seq.seq]

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

Goal state before:
pp: H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (1 + 2)
x : ℕ
⊢ ℕ

Tactic:
have y := v.tail.head

Goal state after:
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (1 + 2)
x y : ℕ
⊢ ℕ
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < r i x

Tactic:
exact fun i => (R.tendsto_atTop_r i).eventually_gt_atTop 0

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (fun n ↦ ε (b i * ↑n) - ε ↑n) ~[atTop] fun n ↦ -log (b i) / log ↑n ^ 2

Tactic:
by
  calc (fun (n : ℕ) => 1 / log (b i * n) - 1 / log n)
    _ =ᶠ[atTop] fun (n : ℕ) => (log n - log (b i * n)) / (log (b i * n) * log n) := by
      filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'
      have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
      simp only [one_div]
      rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]
    _ =ᶠ[atTop] (fun (n : ℕ) ↦ (log n - log (b i) - log n) / ((log (b i) + log n) * log n)) := by
      filter_upwards [eventually_ne_atTop 0] with n hn
      have : 0 < b i := R.b_pos i
      rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]
    _ = (fun (n : ℕ) => -log (b i) / ((log (b i) + log n) * log n)) := by ext; congr; ring
    _ ~[atTop] (fun (n : ℕ) => -log (b i) / (log n * log n)) := by
      refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)
      have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by
        ext; simp [add_comm]
      rw [this]
      exact IsEquivalent.add_isLittleO IsEquivalent.refl
        <| IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i))
          isLittleO_const_log_atTop
    _ = (fun (n : ℕ) => -log (b i) / (log n) ^ 2) := by ext; congr 1; rw [← pow_two]

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 < asympBound g a b n

Tactic:
calc 0 < (n : ℝ) ^ p a b * (1 + 0) := by aesop (add safe Real.rpow_pos_of_pos)
       _ ≤ asympBound g a b n := by
        simp only [asympBound_def']
        gcongr n ^ p a b * (1 + ?_)
        have := R.g_nonneg
        aesop (add safe Real.rpow_nonneg, safe div_nonneg, safe Finset.sum_nonneg)

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case neg.inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
refine Or.inr (Or.inr ?_)
      simp only [lt_iff_le_and_ne]
      rw [eventually_and]
      exact ⟨h', h⟩

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
x : ℝ
hx₁ : f x ≤ 0
hx₂ : 0 ≤ g x
⊢ f x * g x = -|f x| * |g x|

Tactic:
rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case pos
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n x : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
m0 : m = 0
h₂ : (unpair n).2 = x
⊢ ∃ a,
    (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x

Tactic:
exact
          ⟨0, ⟨by simpa [m0] using hf _ _ h₁, fun {m} => (Nat.not_lt_zero _).elim⟩, by simp [h₂]⟩

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
hguv : g.Produces u v
⊢ ∃ r ∈ g.rules, Symbol.nonterminal r.input ∈ u

Tactic:
by
  obtain ⟨w, l, r⟩ := hguv
  exact ⟨w, l, r.nonterminal_input_mem⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (Option.none.bind fun a ↦ evaln k c a) = evaln k c n

Tactic:
cases e : evaln k c n
      · rfl
      exact kn.elim (evaln_bound e)

Goal state after: