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

Goal state before:
pp: case h.inl
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} = ∅
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

pp: case h.inr
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
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅

Tactic:
· use x, hxs, hx, h.le

Goal state after:
case h.inr
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
⊢ ∃ x ∈ s, ∃ (h : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x ⋯).support} ⊆ ∅
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n : ℕ
v w : Fin (n + 2)
⊢ (cycleGraph (n + 2)).Adj v w ↔ w = v - 1 ∨ w = v + 1

Tactic:
cycleGraph_adj,

Goal state after:
n : ℕ
v w : Fin (n + 2)
⊢ v - w = 1 ∨ w - v = 1 ↔ w = v - 1 ∨ w = v + 1
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
⊢ (induce s G).Connected

Tactic:
by
  rw [connected_iff_exists_forall_reachable]
  refine ⟨⟨u, hu⟩, ?_⟩
  rintro ⟨v, hv⟩
  obtain ⟨sv, svs, hu', hv', uv⟩ := patches hv
  exact uv.map (induceHomOfLE _ svs).toHom

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

Goal state before:
pp: n : ℕ
⊢ (cycle n).length = n + 3

Tactic:
unfold cycleGraph.cycle

Goal state after:
n : ℕ
⊢ (have hadj := ⋯;
      cons hadj (cycleCons n (Fin.last (n + 2)))).length =
    n + 3
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ (induce (↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset)) G).Connected

Tactic:
· apply G.induce_connected_of_patches u
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_ofPred_eq, Walk.start_mem_support, exists_prop, and_true]
      exact ⟨u, ut⟩
    intro v hv
    simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv
    obtain ⟨w, wt, hw⟩ := hv
    refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
      exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
    · simp only [Set.mem_ofPred_eq, Walk.start_mem_support, exists_true_left]
      refine ⟨hw, Walk.connected_induce_support _ _ _⟩

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
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ G.finsetWalkLengthLT n u v ↔ p ∈ {p | p.length < n}

Tactic:
by
    rw [← Finset.mem_coe, coe_finsetWalkLengthLT_eq]

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

Goal state before:
pp: case zero
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
u v : V
⊢ (adjMatrix α G ^ 0) u v = ↑(#(G.finsetWalkLength 0 u v))

Tactic:
obtain rfl | h := eq_or_ne u v <;> simp [finsetWalkLength, *]

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
hacyc : (G ⊔ edge u v).IsAcyclic
hreach : G.Reachable u v
⊢ ((G ⊔ edge u v).deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2

Tactic:
convert! hreach

Goal state after:
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
⊢ (G ⊔ edge u v).deleteEdges {s(u, v)} = G
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✝ : 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' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
use G.replaceVertex s t, inferInstance, cf.replaceVertex s t

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
⊢ #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
h✝ : ↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ 2

Tactic:
refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val ?_))
        exact u.val.mod_lt Nat.zero_lt_two

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

Goal state before:
pp: case mpr
α : Type u
G : SimpleGraph α
w✝² : Type u
w✝¹ : w✝² → Type u
w✝ : ∀ (i : w✝²), Nonempty (w✝¹ i)
e : G ≃g completeMultipartiteGraph w✝¹
x✝² x✝¹ x✝ : α
h1 : ¬G.Adj x✝² x✝¹
h2 : ¬G.Adj x✝¹ x✝
⊢ ¬G.Adj x✝² x✝

Tactic:
rw [← e.map_rel_iff] at *

Goal state after:
case mpr
α : Type u
G : SimpleGraph α
w✝² : Type u
w✝¹ : w✝² → Type u
w✝ : ∀ (i : w✝²), Nonempty (w✝¹ i)
e : G ≃g completeMultipartiteGraph w✝¹
x✝² x✝¹ x✝ : α
h1 : ¬(completeMultipartiteGraph w✝¹).Adj (e x✝²) (e x✝¹)
h2 : ¬(completeMultipartiteGraph w✝¹).Adj (e x✝¹) (e x✝)
⊢ ¬(completeMultipartiteGraph w✝¹).Adj (e x✝²) (e x✝)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
⊢ G.IsCompleteMultipartite ↔ ∃ ι V, ∃ (_ : ∀ (i : ι), Nonempty (V i)), Nonempty (G ≃g completeMultipartiteGraph V)

Tactic:
by
  constructor <;> intro h
  · exact ⟨_, _, fun _ ↦ ⟨_, h.setoid.refl _⟩, ⟨h.iso⟩⟩
  · obtain ⟨_, _, _, ⟨e⟩⟩ := h
    refine ⟨fun _ _ _ h1 h2 ↦ ?_⟩
    rw [← e.map_rel_iff] at *
    exact completeMultipartiteGraph.isCompleteMultipartite _ |>.trans _ _ _ h1 h2

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
⊢ ∃ w, w.IsCycle

Tactic:
have := @h {s(u, w)} (by simp)

Goal state after:
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
this : (G.deleteEdges {s(u, w)}).Reachable u w
⊢ ∃ w, w.IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (∑ u, #u.supp.toFinset)

Tactic:
← Set.ncard_eq_toFinset_card',

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (∑ x, x.supp.ncard)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.ediam = 1 ↔ G = ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ediam_top⟩

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : G.ediam = 1
⊢ G = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_3
α : Type u_1
G : SimpleGraph α
x✝ : Nonempty α ∧ Subsingleton α
left✝ : Nonempty α
right✝ : Subsingleton α
⊢ ⨅ u, G.eccent u = 0

Tactic:
ENat.iInf_eq_zero

Goal state after:
case refine_3
α : Type u_1
G : SimpleGraph α
x✝ : Nonempty α ∧ Subsingleton α
left✝ : Nonempty α
right✝ : Subsingleton α
⊢ ∃ i, G.eccent i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
h_bdd : BddBelow {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
h_tto :
  Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop
    (𝓝 (sInf ((fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) '' Set.Ici 2)))
⊢ Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop (𝓝 H.turanDensity)

Tactic:
rwa [← h_tto.limUnder_eq] at h_tto

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)
⊢ Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)

Tactic:
simp_rw [nonempty_coe_sort, pi_nonempty, powersetCard_nonempty]

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)
⊢ ∀ a ∈ K.parts, t ≤ #a
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : 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))
⊢ ‖Fin (r + 1)‖ ≤ #(insert w₁ s)

Tactic:
by simp [hw.isNClique_fst_left.2]

Goal state after:
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 = 2 * M.coe.edgeFinset.card

Tactic:
← M.coe.sum_degrees_eq_twice_card_edges

Goal state after:
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
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v : V
⊢ v ∈ M.verts

Tactic:
· obtain ⟨w, hw, -⟩ := hm v
    exact M.edge_vert hw

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ ↑{x | x ∈ G.incidenceSet a ∩ G.incidenceSet b} = {s(a, b)}

Tactic:
coe_filter_univ

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Fintype (Sym2 α)
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ {x | x ∈ G.incidenceSet a ∩ G.incidenceSet b} = {s(a, b)}
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u : Set V
hc : G.IsClique u
hu : u.Finite
⊢ Even u.ncard ↔ ∃ M, M.verts = u ∧ M.IsMatching

Tactic:
by
  refine ⟨fun h ↦ ?_, by
    rintro ⟨M, rfl, hMr⟩
    simpa [Set.ncard_eq_toFinset_card _ hu, Set.toFinite_toFinset,
      ← Set.toFinset_card] using! @hMr.even_card _ _ _ hu.fintype⟩
  obtain ⟨t, u, rfl, hd, hcard⟩ := Set.exists_union_disjoint_ncard_eq_of_even h
  obtain ⟨f⟩ : Nonempty (t ≃ u) := by
    rw [← Cardinal.eq, ← t.cast_ncard (Set.finite_union.mp hu).1,
      ← u.cast_ncard (Set.finite_union.mp hu).2]
    exact congrArg Nat.cast hcard
  exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd f
    fun v ↦ hc (by simp) (by simp) <| hd.ne_of_mem (by simp) (by simp)

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

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝¹ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝ : DecidableRel G.Adj
a b c d : α
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hbc : b ≠ a
hca : True
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj w₂ y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj w₂ z}) ≤ 2
haj : ¬G.Adj w₂ a
hbj : ¬G.Adj w₂ b
hcj : ¬G.Adj w₂ a
hdj : ¬G.Adj w₂ b
hbx : ¬w₂ = b
⊢ False

Tactic:
· exact hbj <| hw.isNClique_snd_right.1 (mem_insert_self ..) (mem_insert_of_mem hbt) hbx

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

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2

Tactic:
by
  simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl,
    Set.toFinset_sdiff, Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
  simp_rw [compl_neighborFinset_sdiff_inter_eq]
  have hne : v ≠ w := ne_of_adj _ ha
  rw [compl_adj] at ha
  rw [card_sdiff_of_subset, ← insert_eq, card_insert_of_notMem, card_singleton,
    ← Finset.compl_union]
  · rw [card_compl, h.card_neighborFinset_union_of_not_adj hne ha.2, ← h.card]
  · simp only [hne.symm, not_false_iff, mem_singleton]
  · intro u
    simp only [mem_union, mem_compl, mem_neighborFinset, mem_inter, mem_singleton]
    rintro (rfl | rfl) <;> simpa [adj_comm] using ha.2

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

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

Tactic:
induction p.unpair.2

Goal state after:
case zero
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) 0 = (unpair p).1 + 0

case succ
p n✝ : ℕ
a✝ : Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) n✝ = (unpair p).1 + n✝
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) (n✝ + 1) = (unpair p).1 + (n✝ + 1)
Module: Mathlib.Computability.Primrec.Basic

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

Tactic:
induction p.unpair.2

Goal state after:
case zero
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) 0 = (unpair p).1 - 0

case succ
p n✝ : ℕ
a✝ : Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) n✝ = (unpair p).1 - n✝
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) (n✝ + 1) = (unpair p).1 - (n✝ + 1)
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

Goal state after:
case zero
p : ℕ
⊢ Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) 0 = (unpair p).1 * 0

case succ
p n✝ : ℕ
a✝ : Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) n✝ = (unpair p).1 * n✝
⊢ Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) (n✝ + 1) = (unpair p).1 * (n✝ + 1)
Module: Mathlib.Computability.Primrec.Basic

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

Tactic:
induction p.unpair.2

Goal state after:
case zero
p : ℕ
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) 0 = (unpair p).1 ^ 0

case succ
p n✝ : ℕ
a✝ : Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) n✝ = (unpair p).1 ^ n✝
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) (n✝ + 1) = (unpair p).1 ^ (n✝ + 1)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inr.inl
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : m = n
⊢ (p m).Dom

pp: case inr.inr
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : n < m
⊢ (p m).Dom

Tactic:
· rw [h₃]
          exact h₁.fst

Goal state after:
case inr.inr
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : n < m
⊢ (p m).Dom
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
⊢ ∀ (a' : α),
    b ∈ f.fix a' → ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
intro a₁

Goal state after:
case refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
⊢ b ∈ f.fix a₁ → ∀ (k : ℕ), Sum.inr a₁ ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Nat.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False

Tactic:
simp_rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at hc

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
hc : ¬Gmax.universalVerts.ncard < (⊤.deleteVerts Gmax.universalVerts).coe.oddComponents.ncard
⊢ False
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
⊢ (deriv fun z ↦ z ^ p * (1 - ε z)) =ᶠ[atTop] fun x ↦
    deriv (fun x ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x ↦ 1 - ε x) x

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Goal state after:
p x : ℝ
hx : 1 < x
⊢ deriv (fun z ↦ z ^ p * (1 - ε z)) x = deriv (fun x ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x ↦ 1 - ε x) x
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
⊢ (deriv fun x ↦ x ^ p * (1 + ε x)) =ᶠ[atTop] fun x ↦
    deriv (fun x ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x ↦ 1 + ε x) x

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Goal state after:
p x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ x ^ p * (1 + ε x)) x = deriv (fun x ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x ↦ 1 + ε x) x
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case inl
p : ℝ
hp : p = 0
⊢ GrowsPolynomially fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖

Tactic:
| inl hp =>

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

Goal state before:
pp: case inl
p : ℝ
hp : p = 0
⊢ GrowsPolynomially fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖

Tactic:
| inl hp =>

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
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
hn : ‖↑n / log ↑n ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖
hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
i : α
⊢ ↑(r i n) ≤ c * ↑n

Tactic:
rw [Real.norm_of_nonneg (by positivity)] at hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
hn : ↑n / log ↑n ^ 2 ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖
hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
i : α
⊢ ↑(r i n) ≤ c * ↑n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case h₂
x : ℝ
hx : rexp 1 ≤ x
this : 1 < x
⊢ 1 ≤ log x

Tactic:
calc 1 = log (exp 1) := by simp
       _ ≤ log x := log_le_log (exp_pos _) hx

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

Goal state before:
pp: ⊢ (deriv fun x ↦ 1 - ε x) =ᶠ[atTop] -deriv ε

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 - ε x) x = (-deriv ε) x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (deriv fun x ↦ 1 + ε x) =ᶠ[atTop] deriv ε

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 + ε x) x = deriv ε x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (deriv fun x ↦ 1 - ε x) =ᶠ[atTop] fun z ↦ -deriv ε z

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 - ε x) x = -deriv ε x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (deriv fun x ↦ 1 + ε x) =ᶠ[atTop] fun z ↦ deriv ε z

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 + ε x) x = deriv ε x
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case e_a.e_a
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ ↑(#(Ico (r i n) n)) = ↑n - ↑(r i n)

Tactic:
rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]

Goal state after: