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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
v : V
⊢ v ∈ (G.replaceVertex s t).neighborFinset u ↔ v ∈ G.neighborFinset u \ {t}

Tactic:
simp_rw [mem_neighborFinset, mem_sdiff, mem_singleton, replaceVertex]

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
v : V
⊢ (if u = t then if v = t then False else G.Adj s v else if v = t then G.Adj u s else G.Adj u v) ↔
    v ∈ G.neighborFinset u ∧ ¬v = t
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, w.IsCycle

Tactic:
classical
  obtain ⟨w, hw, h⟩ := exists_adj_isEdgeReachable_two huv (h.anti hn)
  have := @h {s(u, w)} (by simp)
  obtain ⟨w, p, hp₁, hp₂⟩ := adj_and_reachable_delete_edges_iff_exists_cycle.mp ⟨hw, this⟩
  exact ⟨p.rotate _ (p.fst_mem_support_of_mem_edges hp₂), hp₁.rotate _⟩

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

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ (turanGraph n (Fintype.card α - 1)).IsTuranMaximal (Fintype.card α - 1)

Tactic:
exact isTuranMaximal_turanGraph (Nat.sub_pos_iff_lt.mpr Fintype.one_lt_card)

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ G.radius = G.ediam ↔ ∃ e, ∀ (u : α), G.eccent u = e

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

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : G.radius = G.ediam
⊢ ∃ e, ∀ (u : α), G.eccent u = e

case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∃ e, ∀ (u : α), G.eccent u = e
⊢ G.radius = G.ediam
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ Set.univ ⊆ G.center ↔ ∃ e, ∀ (u : α), G.eccent u = e

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

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : Set.univ ⊆ G.center
⊢ ∃ e, ∀ (u : α), G.eccent u = e

case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∃ e, ∀ (u : α), G.eccent u = e
⊢ Set.univ ⊆ G.center
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : u ∈ Set.univ
⊢ u ∈ G.center

Tactic:
mem_center_iff,

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : u ∈ Set.univ
⊢ G.eccent u = G.radius
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
u : α
⊢ u ∈ G.center

Tactic:
mem_center_iff,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
u : α
⊢ G.eccent u = G.radius
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ u ∈ ⊥.center

Tactic:
mem_center_iff,

Goal state after:
case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ ⊥.eccent u = ⊥.radius
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ u ∈ ⊤.center

Tactic:
mem_center_iff,

Goal state after:
case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ ⊤.eccent u = ⊤.radius
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
B : SimpleGraph (Fin m ⊕ Fin n)
left✝ : B ≤ completeBipartiteGraph (Fin m) (Fin n)
h : (completeBipartiteGraph (Fin s) (Fin t)).Free B
⊢ #(SimpleGraph.map (⇑finSumFinEquiv) B).edgeFinset ≤
    extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)

Tactic:
refine card_edgeFinset_le_extremalNumber <|
    (h.congr_left ?_).congr_right (Iso.map finSumFinEquiv B).symm

Goal state after:
m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
B : SimpleGraph (Fin m ⊕ Fin n)
left✝ : B ≤ completeBipartiteGraph (Fin m) (Fin n)
h : (completeBipartiteGraph (Fin s) (Fin t)).Free B
⊢ completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t)
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)
⊢ ∀ a ∈ K.parts, t ≤ #a

Tactic:
intro p

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)
p : Finset (Fin n)
⊢ p ∈ K.parts → t ≤ #p
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ≠ c → G.Adj w b
⊢ G.IsNClique r (insert a (insert b (s.erase c)))

Tactic:
by
  rw [insert_comm, ← erase_insert_of_ne (fun h : a = c ↦ ha (h ▸ hc) |>.elim)]
  simp_rw [adj_comm, ← notMem_singleton] at hd
  exact hs.insert_erase (fun _ h ↦ hd _ (mem_sdiff.1 h).1 (mem_sdiff.1 h).2) (mem_insert_of_mem hc)

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

Goal state before:
pp: case refine_2.inr
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ ⟨v, ⋯⟩ ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}

Tactic:
simp [h.toEdge_eq_of_adj huv.symm]

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

Goal state before:
pp: case inl
ε : ℝ
hε : 0 < ε
r t : ℕ
h0 : r = 0 ∨ t = 0
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → completeEquipartiteGraph (r + 1) t ⊑ G

Tactic:
rw [← Nat.le_zero_eq, ← @Nat.add_le_add_iff_right r 0 1, zero_add] at h0

Goal state after:
case inl
ε : ℝ
hε : 0 < ε
r t : ℕ
h0 : r + 1 ≤ 1 ∨ t = 0
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → completeEquipartiteGraph (r + 1) t ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
h : Maximal (fun H ↦ H.CliqueFree (r + 1)) G
⊢ G.Colorable r ↔ G.IsCompleteMultipartite

Tactic:
match r with
  | 0 => exact ⟨fun _ ↦ ⟨fun x ↦ cliqueFree_one.1 h.1 |>.elim' x⟩,
                fun _ ↦ G.colorable_zero_iff.2 <| cliqueFree_one.1 h.1⟩
  | r + 1 =>
    refine ⟨fun hc ↦ ?_, fun hc ↦ hc.colorable_of_cliqueFree h.1⟩
    contrapose hc
    obtain ⟨_, _, _, _, _, hw⟩ :=
      exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hc
    exact hw.not_colorable_succ

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

Goal state before:
pp: case h
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w ↦ M.Adj v w) v' ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = v'
⊢ ∀ (y : W), (fun w ↦ (Subgraph.map f M).Adj (f v) w) y → y = f v'

Tactic:
rintro _ ⟨w, w', hw, hw', rfl⟩

Goal state after:
case h
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun w ↦ M.Adj v w) v' ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = v'
w w' : V
hw : M.Adj w w'
hw' : f w = f v
⊢ f w' = f v'
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this✝ : DecidablePred fun x ↦ x ∈ (M.induce c.supp).verts := fun a ↦ G.instDecidableMemSupp c a
this : Even (Fintype.card ↑c.supp)
⊢ Even (Fintype.card ↑c.supp)

Tactic:
exact this

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
inst✝ : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j : V
⊢ G.Reachable i j → x i = x j

Tactic:
⟨w⟩

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j : V
w : G.Walk i j
⊢ x i = x j
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
⊢ LinearIndependent ℝ G.lapMatrix_ker_basis_aux

Tactic:
rw [Fintype.linearIndependent_iff]
  intro g h0
  rw [Subtype.ext_iff] at h0
  have h : ∑ c, g c • lapMatrix_ker_basis_aux G c = fun i ↦ g (connectedComponentMk G i) := by
    simp only [lapMatrix_ker_basis_aux, SetLike.mk_smul_mk]
    repeat rw [AddSubmonoid.coe_finsetSum]
    ext i
    simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, mul_ite, mul_one, mul_zero, sum_ite_eq,
      mem_univ, ↓reduceIte]
  rw [h] at h0
  intro c
  obtain ⟨i, h'⟩ : ∃ i : V, G.connectedComponentMk i = c := Quot.exists_rep c
  exact h' ▸ congrFun h0 i

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

Goal state before:
pp: case h.inr
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
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w

Tactic:
have ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj hr.1
      simp_all [show M.Adj v y ↔ ¬M.Adj v w' by simpa using hG' hw'.1 hr.1 hw'.2]

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

Goal state before:
pp: case cons
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 : p.IsTrail → (Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝)
ht : (cons huv p).IsTrail
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) (cons huv p).edges) ↔ u✝ ≠ w✝ → x ≠ u✝ ∧ x ≠ w✝

Tactic:
rw [isTrail_cons] at ht

Goal state after:
case cons
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 : p.IsTrail → (Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝)
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) (cons huv p).edges) ↔ u✝ ≠ w✝ → x ≠ u✝ ∧ x ≠ w✝
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
a✝ : Nontrivial V
x : V
n : ℕ
hn : ∀ (i : Set V), G.IsVertexCover i → ↑n ≤ i.encard
⊢ G.IsVertexCover (Set.univ \ {x})

Tactic:
by grind [IsVertexCover, Adj.ne']

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Nonempty V
inst✝ : Finite V
⊢ G.vertexCoverNum + 1 ≤ ENat.card V

Tactic:
vertexCoverNum_le_card_sub_one,

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Nonempty V
inst✝ : Finite V
⊢ ENat.card V - 1 + 1 ≤ ENat.card V
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ 1 + 1 ≤ (Set.univ \ t).encard

Tactic:
rw [Set.encard_sdiff (by simp) (Set.finite_of_encard_eq_coe ht₁), Set.encard_univ]

Goal state after:
V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
⊢ 1 + 1 ≤ ENat.card V - t.encard
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
⊢ ∃ M, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts

Tactic:
obtain ⟨t, ht, M1, hM1⟩ := Subgraph.IsMatching.exists_of_universalVerts
      (disjoint_image_val_universalVerts _).symm (by
        simp only [IsTutteViolator, not_lt] at h
        rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq])

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
⊢ ∃ M, M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ (((↑(Option.some a)).bind fun a ↦ Part.map encode (↑f a)).bind fun n_1 ↦
      Nat.rec ((↑(Option.some a)).bind fun a ↦ Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode ((fun p ↦ h p.1 p.2) a))
        n_1) =
    (↑(Option.some a)).bind fun a ↦
      Part.map encode ((fun a ↦ Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (f a)) a)

Tactic:
simp only [coe_some, PFun.coe_val, bind_some]

Goal state after:
case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ ((Part.map encode (Part.some (f a))).bind fun n_1 ↦
      Nat.rec (Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode (h a.1 a.2))
        n_1) =
    Part.map encode (Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (f a))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case refine_2
H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
this :
  Primrec' fun v ↦
    Nat.rec 0
      (fun y IH ↦
        have x := (y ::ᵥ IH ::ᵥ v).head;
        have y := (y ::ᵥ IH ::ᵥ v).tail.head;
        if x.succ < y.succ * y.succ then y else y.succ)
      v.head
⊢ Primrec' fun v ↦ Nat.rec 0 (fun x y ↦ if x + 1 < (y + 1) * (y + 1) then y else y + 1) v.head

Tactic:
exact this

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

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : f (2 ^ (-↑k - 1) * x₀) = 0
z : ℝ
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
hx : z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) → f z = 0
this : z ≤ 2 ^ (-↑k - 1) * x₀
⊢ z ≤ 2 ^ (-↑k - 1) * x₀

Tactic:
exact this

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

Goal state before:
pp: case ind.inr
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
⊢ 0 < ∑ i, a i * T (r i n) + g ↑n

Tactic:
have := R.g_nonneg

Goal state after:
case ind.inr
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ 0 < ∑ i, a i * T (r i n) + g ↑n
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 : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * ↑n)
h_log_pos : 0 < log ↑n
⊢ (log (b i * ↑n))⁻¹ - (log ↑n)⁻¹ = (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n)

Tactic:
inv_sub_inv (by have := hn' i; positivity) (by aesop)

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * ↑n)
h_log_pos : 0 < log ↑n
⊢ (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n) = (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case h₂
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 ≤ ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1)

Tactic:
have := R.g_nonneg

Goal state after:
case h₂
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ 0 ≤ ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inr.inr
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, g x ≤ 0
hmain : (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ |f x| * |g x|
⊢ GrowsPolynomially fun x ↦ |f x| * |g x|

Tactic:
exact this

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |f x|) u ∈ Set.Icc (c₁ * (fun x ↦ |f x|) x) (c₂ * (fun x ↦ |f x|) x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
hc₄_mem : c₄ > 0
hg✝ :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ |g x|) u ∈ Set.Icc (c₃ * (fun x ↦ |g x|) x) (c₄ * (fun x ↦ |g x|) x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ c₁ * |f x| * (c₃ * |g x|) ≤ |f u| * |g u|

Tactic:
by
           gcongr
           · exact (hf u hu).1
           · exact (hg u hu).1

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := ⋯
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound1 : ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
h_smoothing_pos : 0 < 1 - ε ↑n
h_sumTransform : ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
h_smoothing_gt_half : 1 / 2 < 1 - ε ↑n
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
n₀_div_le_n : ⌈↑n₀ / b'⌉₊ ≤ n
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
C : ℝ
hC : C ≥ 2 * c₁⁻¹
h_ind : ∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
i : α
a✝ : i ∈ univ
⊢ c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n

Tactic:
· exact h_sumTransform i

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

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
hfg₃ : ‖g u‖ ≤ 1 / 2 * f u
⊢ 3 / 2 * f u ≤ 3 / 2 * (c₂ * f x)

Tactic:
gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.refine_1
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
⊢ Nat.rec (evaln (k + 1) cf (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      m =
    some y

Tactic:
have := evaln_mono k.le_succ h₁

Goal state after:
case succ.refine_1
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x y : ℕ
h₁ : evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some y
h₂ : evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m y)) = some x
this : y ∈ evaln k.succ (cf.prec cg) (Nat.pair (unpair n).1 m)
⊢ Nat.rec (evaln (k + 1) cf (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      m =
    some y