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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this✝ : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v, G.degree v = 2 * G.edgeFinset.card
hle : ∑ v, 2 ≤ ∑ v, G.degree v
⊢ G.minDegree = 1

Tactic:
rw [Finset.sum_const, Finset.card_univ, smul_eq_mul] at hle

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this✝ : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v, G.degree v = 2 * G.edgeFinset.card
hle : Fintype.card V * 2 ≤ ∑ v, G.degree v
⊢ G.minDegree = 1
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 : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
hn : ¬fp.IsEquipartition
⊢ False

Tactic:
rw [Finpartition.not_isEquipartition] at hn

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
hn : ∃ a ∈ fp.parts, ∃ b ∈ fp.parts, #b + 1 < #a
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ Odd {c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}.ncard ↔ Odd c'.supp.ncard

Tactic:
by
  simp_rw [← Nat.card_coe_set_eq]
  classical
  cases nonempty_fintype V
  rw [Nat.card_eq_card_toFinset c'.supp, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]
  simp only [Finset.card_disjiUnion, Set.toFinset_card, Fintype.card_ofFinset]
  rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset]
  congr! 2
  ext c
  simp_rw [Set.toFinset_ofPred, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : ¬Even K.supp.ncard
⊢ Even (K.supp \ s).ncard

Tactic:
have : K.supp.ncard ≠ 0 := Nat.ne_of_odd_add (Nat.not_even_iff_odd.mp h)

Goal state after:
case neg
V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : ¬Even K.supp.ncard
this : K.supp.ncard ≠ 0
⊢ Even (K.supp \ s).ncard
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u ≤ 1
v : α
⊢ u ≠ v → G.Adj u v

Tactic:
huv

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
u : α
h : G.eccent u ≤ 1
v : α
huv : u ≠ v
⊢ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case mpr
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
v : α
⊢ G.edist u v ≤ 1

Tactic:
edist_le_one_iff_adj_or_eq

Goal state after:
case mpr
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
v : α
⊢ G.Adj u v ∨ u = v
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.ediam = ⊤
⊢ G.ediam.toNat = 0

Tactic:
h,

Goal state after:
α : Type u_1
G : SimpleGraph α
h : G.ediam = ⊤
⊢ ⊤.toNat = 0
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
K L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Finite (G.ComponentCompl ↑∅)

pp: case inr
V : Type u
G : SimpleGraph V
K✝ L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
⊢ Finite (G.ComponentCompl ↑K)

Tactic:
· dsimp [ComponentCompl]
    rw [Finset.coe_empty, Set.compl_empty]
    have := Gpc.out.subsingleton_connectedComponent
    exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm

Goal state after:
case inr
V : Type u
G : SimpleGraph V
K✝ L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
⊢ Finite (G.ComponentCompl ↑K)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inr
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w ↦ N.Adj v w) w ∧ ∀ (y : V), (fun w ↦ N.Adj v w) y → y = w
y : V
h : N'.Adj v y
⊢ y = w

Tactic:
rw [Set.disjoint_left] at hd

Goal state after:
case h.inr
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : ∀ ⦃a : V⦄, a ∈ N.support → a ∉ N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w ↦ N.Adj v w) w ∧ ∀ (y : V), (fun w ↦ N.Adj v w) y → y = w
y : V
h : N'.Adj v y
⊢ y = w
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)
⊢ ∃ y, t ≤ #{w | pi K w = y}

Tactic:
by
  have : Nonempty (K.parts.pi (·.powersetCard t)) := by
    simp_rw [nonempty_coe_sort, pi_nonempty, powersetCard_nonempty]
    intro p hp
    rw [K.card_mem_parts hp]
    exact ht_lt_t'.le
  apply exists_le_card_fiber_of_mul_le_card
  simp_rw [card_coe]
  calc #(K.parts.pi (·.powersetCard t)) * t
    _ = (∏ x ∈ K.parts, (#x).choose t) * t := by
        simp_rw [Finset.card_pi, card_powersetCard]
    _ = (∏ p ∈ K.parts, t'.choose t) * t :=
        congrArg (· * t) <| prod_congr rfl
          fun p hp ↦ congrArg (Nat.choose · t) <| K.card_mem_parts hp
    _ ≤ t'.choose t ^ r * t := by
        rw [prod_const, K.card_parts.resolve_right ht'_pos.ne']
    _ ≤ #(filter K t) := by
        refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt ht_lt_t')
        rw [← @Nat.cast_le ℝ, Nat.cast_mul _ (t' - t), Nat.cast_mul _ (t' - t),
          Nat.cast_sub ht_lt_t'.le]
        exact mul_le_card_filter_mul K hr_pos ht'_pos hδ (mod_cast hN)

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
⊢ ∃ k v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j

Tactic:
obtain ⟨_, _, _, s, t, hw⟩ :=
    exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hnc
  let P : ℕ → Prop := fun k ↦ ∃ v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t
  have hk : P #(s ∩ t) := ⟨_, _, _, _, _, hw⟩
  classical
  obtain ⟨_, _, _, _, _, hw⟩ := Nat.findGreatest_spec (hw.card_inter_lt_of_cliqueFree h.1).le hk
  exact ⟨_, _, _, _, _, _, hw, hw.card_inter_lt_of_cliqueFree h.1,
         fun _ hj _ _ _ _ _ hv ↦ hj.not_ge <| Nat.le_findGreatest
           (hv.card_inter_lt_of_cliqueFree h.1).le ⟨_, _, _, _, _, hv⟩⟩

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

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

Tactic:
simp_rw [degree, card_eq_sum_ones]
    exact sum_comm' (by simp [and_comm, adj_comm])

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
β : Type u_2
H : SimpleGraph β
a b : α
p : G.Walk a b
f : G →g H
hp : p.IsHamiltonian
h : (Walk.map f p).IsPath
⊢ Injective ⇑f

Tactic:
rw [← Set.injOn_univ, ← hp.setOfPred_support]
  exact h.injOn_support_of_isPath_map

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h✝ : Nonempty α
x✝ : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective fun x ↦ p.support.get x
⊢ Fintype.card α = p.length + 1

Tactic:
h,

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h✝ : Nonempty α
x✝ : p.IsPath ∧ p.length = Fintype.card α - 1
hp : p.IsPath
h : p.length = Fintype.card α - 1
this : Injective fun x ↦ p.support.get x
⊢ Fintype.card α = Fintype.card α - 1 + 1
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
p : G.Walk a a
hf : Bijective ⇑f
hp : p.IsHamiltonianCycle
x : α
⊢ List.count (f x) (Walk.map f p).tail.support = 1

Tactic:
rcases p with (_ | ⟨y, p⟩)

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

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) (Walk.map f (cons y p)).tail.support = 1
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case inl
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v : V
⊢ ↑(Fintype.card ↑(G.commonNeighbors v v)) =
    (k • 1 v v + ℓ • if G.Adj v v then 1 else 0) + μ • if v ≠ v ∧ ¬G.Adj v v then 1 else 0

Tactic:
rw [← Set.toFinset_card]

Goal state after:
case inl
V : Type u
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝¹ : DecidableEq V
α : Type u_1
inst✝ : Semiring α
h : G.IsSRGWith n k ℓ μ
v : V
⊢ ↑(#(G.commonNeighbors v v).toFinset) =
    (k • 1 v v + ℓ • if G.Adj v v then 1 else 0) + μ • if v ≠ v ∧ ¬G.Adj v v then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Fintype.card ↑{v | Odd (G.degree v)} = 0 ∨ Fintype.card ↑{v | Odd (G.degree v)} = 2

Tactic:
rw [← Set.toFinset_card]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ {v | Odd (G.degree v)}.toFinset.card = 0 ∨ {v | Odd (G.degree v)}.toFinset.card = 2
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective ⇑f
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this✝¹ : IsAntichain H.Adj sᶜ
this✝ : IsAntichain G.Adj (⇑f ⁻¹' sᶜ)
this : G.IsVertexCover (⇑f ⁻¹' s)
⊢ (⇑f ⁻¹' s).encard ≤ H.vertexCoverNum

Tactic:
← hs₁

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective ⇑f
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this✝¹ : IsAntichain H.Adj sᶜ
this✝ : IsAntichain G.Adj (⇑f ⁻¹' sᶜ)
this : G.IsVertexCover (⇑f ⁻¹' s)
⊢ (⇑f ⁻¹' s).encard ≤ s.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
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
⊢ Disjoint M1.support M2.support

Tactic:
rw [hM1.2.support_eq_verts, hM2.support_eq_verts, Subgraph.verts_iSup,
      Set.disjoint_iUnion_right]

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

Goal state before:
pp: case refine_2.groupElts
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    ∃ g, ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ }.groupElts ≍ { index := i₁, groupElts := g₂ }.groupElts

Tactic:
· exact heq_of_eq (hg₁.symm.trans hg₂)

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

Goal state before:
pp: α : 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
⊢ Primrec fun a ↦ List.foldl (fun s b ↦ h a (s, b)) (g a) (f a)

Tactic:
suffices ∀ a n, F a n = (((f a).take n).foldl (fun s b => h a (s, b)) (g a), (f a).drop n) by
    refine hF.of_eq fun a => ?_
    rw [this, List.take_of_length_le (length_le_encode _)]

Goal state after:
α : 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 : ℕ), F a n = (List.foldl (fun s b ↦ h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f g : List.Vector ℕ n → ℕ
h : List.Vector ℕ (n + 2) → ℕ
hf : Primrec' f
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' fun v ↦ Nat.rec (g v) (fun y IH ↦ h (y ::ᵥ IH ::ᵥ v)) (f v)

Tactic:
simpa using comp' (prec hg hh) (hf.cons idv)

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
gt_zero : 0 < b (min_bi b)
⊢ ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)

Tactic:
exact ⟨b (min_bi b) / 2, ⟨⟨by positivity, R.bi_min_div_two_lt_one⟩, R.eventually_bi_mul_le_r⟩⟩

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

Goal state before:
pp: ⊢ -deriv ε =ᶠ[atTop] fun x ↦ x⁻¹ / log x ^ 2

Tactic:
filter_upwards with x
      simp [deriv_smoothingFn, neg_div]

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially (-f)

Tactic:
by
  intro b hb
  obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf b hb
  refine ⟨c₂, hc₂_mem, c₁, hc₁_mem, ?_⟩
  filter_upwards [hf] with x hx
  intro u hu
  simp only [Pi.neg_apply, Set.neg_mem_Icc_iff, neg_mul_eq_mul_neg, neg_neg]
  exact hx u hu

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

Goal state before:
pp: case h₂
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₃ * |g x| ≤ |g u|

Tactic:
exact (hg u hu).1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
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
i : α
this : ↑n₀ / b' ≤ ↑n
⊢ ↑n₀ ≤ b' * ↑n

Tactic:
rwa [div_le_iff₀, mul_comm] at this

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
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
i : α
this : ↑n₀ / b' ≤ ↑n
⊢ 0 < b'
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case h₂
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] 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, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g 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)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
fx_nonneg : 0 ≤ f x
gx_nonneg : 0 ≤ g x
⊢ c₃ * g x ≤ g u

Tactic:
exact (hg u hu).1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑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
h_exp : ⌈rexp 1⌉₊ ≤ n
i : α
this : ↑n₀ / b' ≤ ↑n
⊢ ↑n₀ ≤ b' * ↑n

Tactic:
rwa [div_le_iff₀, mul_comm] at this

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
bound2 : ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
h_smoothing_pos : 0 < 1 + ε ↑n
h_sumTransform : ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑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
h_exp : ⌈rexp 1⌉₊ ≤ n
i : α
this : ↑n₀ / b' ≤ ↑n
⊢ 0 < b'