mathlib-initiative/mathlib-tactics huggingface dataset:
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'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑(#K.verts) * (1 - 1 / ↑r + ε) * ↑n - ↑n * (↑(#K.verts) - (↑t' - ↑t)) - ↑(#K.verts) * (↑t' - ↑t)

Tactic:
← mul_rotate,

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'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑n * ↑(#K.verts) * (1 - 1 / ↑r + ε) - ↑n * (↑(#K.verts) - (↑t' - ↑t)) - ↑(#K.verts) * (↑t' - ↑t)
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})
⊢ ∑ v, #(G.neighborFinset v ∩ W) ≤ #X * (#W - i) + #Xᶜ * (#W - j)

Tactic:
by
    simp_rw [← union_compl X, sum_union disjoint_compl_right (s₁ := X), neighborFinset_eq_filter,
             filter_inter, univ_inter, card_eq_sum_ones X, card_eq_sum_ones Xᶜ, sum_mul, one_mul]
    gcongr <;> grind [card_filter_add_card_filter_not]

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

Goal state before:
pp: case h.inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hl : v ∈ s
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

pp: case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Tactic:
· use f ⟨v, hl⟩
    simp only [hl, exists_const, true_or, exists_true_left, true_and]
    rintro y (rfl | ⟨hys, rfl⟩)
    · rfl
    · exact (h.ne_of_mem hl (f ⟨y, hys⟩).coe_prop rfl).elim

Goal state after:
case h.inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hr : v ∈ t
⊢ ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ (↑c).supp
hw : (fun w ↦ M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w ↦ M.Adj (↑⟨v', hv'⟩) w) y → y = w
hwnu : w ∉ u
⊢ w ∈ ⊤.verts

Tactic:
trivial

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✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
w v' : V
hv'✝ : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'✝⟩ ∈ (↑c).supp
hw : (fun w ↦ M.Adj (↑⟨v', hv'✝⟩) w) w ∧ ∀ (y : V), (fun w ↦ M.Adj (↑⟨v', hv'✝⟩) w) y → y = w
hwnu : w ∉ u
hv' : v' ∉ u
⊢ v' ∉ u

Tactic:
trivial

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
⊢ ∃ w ∈ u, ∃ v, M.Adj (↑v) w ∧ v ∈ (↑c).supp

Tactic:
by_contra! h
  have hMmatch : (M.induce c.val.supp).IsMatching := by
    intro v hv
    obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
    obtain ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ := hv
    use w
    have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv
    refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩
    apply ConnectedComponent.mem_coe_supp_of_adj ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ ⟨by trivial, hwnu⟩
    simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.mem_sdiff, Set.mem_univ, true_and,
      Subgraph.induce_adj, hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1,
      and_true] at hv' ⊢
    trivial
  apply Nat.not_even_iff_odd.2 c.prop
  have : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c.val)).verts := Fintype.ofFinite _
  classical
  have := Fintype.ofFinite c.val.supp
  simpa [Finset.card_image_of_injective] using hMmatch.even_card

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
⊢ (fun w' ↦ w ≠ w' ∧ G.Adj v w') y → y = w'

Tactic:
⟨hwy, hwy'⟩

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
⊢ y = w'
Module: Mathlib.Combinatorics.SimpleGraph.LineGraph

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
e₁ e₂ : ↑G.edgeSet
hadj : e₁ ≠ e₂ ∧ (↑↑e₁ ∩ ↑↑e₂).Nonempty
⊢ e₂ ≠ e₁ ∧ (↑↑e₂ ∩ ↑↑e₁).Nonempty

Tactic:
by rwa [ne_comm, Set.inter_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
⊢ P.partOfVertex v ≠ P.partOfVertex w

Tactic:
intro hn
  have hw := P.mem_partOfVertex w
  rw [← hn] at hw
  exact P.independent _ (P.partOfVertex_mem v) (P.mem_partOfVertex v) hw (G.ne_of_adj h) h

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ ↑n
h₂ : ↑n ≤ ENat.card V
⊢ ∃ s, s.encard = ↑n ∧ G.IsVertexCover s

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := vertexCoverNum_exists G
  obtain ⟨r, hr₁, _, hr₃⟩ :=
    Set.exists_superset_subset_encard_eq (by simp) (le_of_eq_of_le hs₁ h₁) (Set.encard_univ _ ▸ h₂)
  exact ⟨r, hr₃, hs₂.subset hr₁⟩

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

Goal state before:
pp: this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : k = 0
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 ↦ x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
then

Goal state after:
this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : k = 0
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 ↦ x1 / x2) (a, k).1 (a, k).2 = q
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:
cases decode (α := α) n <;> simp [Seq.seq]

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

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x' b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x' b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x' b
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x' b
hxc : x' ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
hx' : x'✝ ∈ {x', b}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj x' b

Tactic:
hw _ hM1xb,

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x' b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x' b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x' b
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x' b
hxc : x' ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
hx' : x'✝ ∈ {x', b}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj x' w
Module: Mathlib.Computability.Partrec

Goal state before:
pp: f : ℕ →. ℕ
⊢ Partrec f ↔ Nat.Partrec f

Tactic:
simp [Partrec, map_id']

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

Goal state before:
pp: n : ℕ
a b f g : List.Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : List.Vector ℕ n
⊢ Nat.rec (g v) (fun y IH ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) (b v - a v) = if a v < b v then f v else g v

Tactic:
by
    cases e : b v - a v
    · simp [not_lt.2 (Nat.sub_eq_zero_iff_le.mp e)]
    · simp [Nat.lt_of_sub_eq_succ e]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
⊢ encode cf < encode (cf.comp cg) ∧ encode cg < encode (cf.comp cg)

Tactic:
have : encode (pair cf cg) < encode (comp cf cg) := by simp [encodeCode_eq, encodeCode]

Goal state after:
cf cg : Code
this : encode (cf.pair cg) < encode (cf.comp cg)
⊢ encode cf < encode (cf.comp cg) ∧ encode cg < encode (cf.comp cg)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: 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

Tactic:
rw [deriv_fun_mul]

Goal state after:
case hc
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun z ↦ z ^ p) x

case hd
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun z ↦ 1 - ε z) x
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: 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

Tactic:
rw [deriv_fun_mul]

Goal state after:
case hc
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ x ^ p) x

case hd
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1 + ε x) x
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)
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖
n : ℕ
hn' : ∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)
i : α
hn : ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ↑n
⊢ b (min_bi b) * ↑n - ‖↑n / log ↑n ^ 2‖ ≤ b i * ↑n - ‖↑n / log ↑n ^ 2‖

Tactic:
gcongr; aesop

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 : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
m : ℕ
⊢ ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0

Tactic:
induction m with

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
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x ↦ ‖deriv q x‖
i✝ : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
i : α
⊢ b (min_bi b) / 2 ≤ b i / 2

Tactic:
gcongr; aesop

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
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x ↦ ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x ↦ ‖deriv q x‖) x) (c₂ * (fun x ↦ ‖deriv q x‖) x)
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖q ↑(r i x) - q (b i * ↑x)‖ ≤ c * ‖deriv q ↑x * (↑(r i x) - b i * ↑x)‖

Tactic:
refine ⟨c₂, ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x ↦ ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x ↦ ‖deriv q x‖) x) (c₂ * (fun x ↦ ‖deriv q x‖) x)
⊢ ∀ᶠ (x : ℕ) in atTop, ‖q ↑(r i x) - q (b i * ↑x)‖ ≤ c₂ * ‖deriv q ↑x * (↑(r i x) - b i * ↑x)‖
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case lb
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 : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ 2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊ - 1) * x₀ ≤ x

pp: case ub
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 : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ x ≤ 2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊) * x₀

Tactic:
case lb =>
    rw [← le_div_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (zpow_pos (by norm_num) _)
      (by positivity)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_sub, Int.cast_neg, Int.cast_natCast, Int.cast_one, neg_sub, sub_neg_eq_add]
    calc -logb 2 (x / x₀) ≤ ⌈-logb 2 (x / x₀)⌉₊ := Nat.le_ceil (-logb 2 (x / x₀))
         _ ≤ _ := by rw [add_comm]; exact_mod_cast Nat.ceil_le_floor_add_one _

Goal state after:
case ub
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 : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ x ≤ 2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊) * x₀
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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ deriv (fun x ↦ x ^ p a b * (1 - ε x)) x =
    deriv (fun z ↦ z ^ p a b) x * (1 - ε x) + x ^ p a b * deriv (fun z ↦ 1 - ε z) x

Tactic:
rw [deriv_fun_mul]

Goal state after:
case hc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ x ^ p a b) x

case hd
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1 - ε x) x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 1 / 2 * x ≤ 3 / 4 * x

Tactic:
by gcongr ?_ * x; norm_num

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 1 / 2 * x ≤ 3 / 4 * x

Tactic:
by gcongr ?_ * x; norm_num

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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ deriv (fun x ↦ x ^ p a b * (1 + ε x)) x =
    deriv (fun z ↦ z ^ p a b) x * (1 + ε x) + x ^ p a b * deriv (fun z ↦ 1 + ε z) x

Tactic:
rw [deriv_fun_mul]

Goal state after:
case hc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ x ^ p a b) x

case hd
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1 + ε x) x
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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
⊢ ∀ᶠ (x : ℕ) in atTop, b i ^ p a b * ↑x ^ p a b * (1 + ε ↑x) ≤ ↑(r i x) ^ p a b * (1 + ε ↑(r i x))

Tactic:
have h_deriv_q : deriv q =O[atTop] fun x => x ^ ((p a b) - 1) :=
    calc deriv q
      _ = deriv fun x => (fun z => z ^ (p a b)) x * (fun z => 1 + ε z) x := by rfl
      _ =ᶠ[atTop] fun x => deriv (fun z => z ^ (p a b)) x * (1 + ε x)
          + x ^ (p a b) * deriv (fun z => 1 + ε z) x := by
        filter_upwards [eventually_ne_atTop 0, eventually_gt_atTop 1] with x hx hx'
        rw [deriv_fun_mul] <;> aesop
      _ =O[atTop] fun x => x ^ ((p a b) - 1) := by
        refine IsBigO.add ?left ?right
        case left =>
          calc (fun x => deriv (fun z => z ^ (p a b)) x * (1 + ε x))
            _ =O[atTop] fun x => x ^ ((p a b) - 1) * (1 + ε x) :=
              IsBigO.mul (isBigO_deriv_rpow_const_atTop (p a b)) (isBigO_refl _ _)
            _ =O[atTop] fun x => x ^ ((p a b) - 1) * 1 :=
              IsBigO.mul (isBigO_refl _ _) isEquivalent_one_add_smoothingFn_one.isBigO
            _ = fun x => x ^ ((p a b) - 1) := by ext; rw [mul_one]
        case right =>
          calc (fun x => x ^ (p a b) * deriv (fun z => 1 + ε z) x)
            _ =O[atTop] (fun x => x ^ (p a b) * x⁻¹) :=
              IsBigO.mul (isBigO_refl _ _) isLittleO_deriv_one_add_smoothingFn.isBigO
            _ =ᶠ[atTop] fun x => x ^ ((p a b) - 1) := by
              filter_upwards [eventually_gt_atTop 0] with x hx
              rw [← Real.rpow_neg_one, ← Real.rpow_add hx, ← sub_eq_add_neg]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
⊢ ∀ᶠ (x : ℕ) in atTop, b i ^ p a b * ↑x ^ p a b * (1 + ε ↑x) ≤ ↑(r i x) ^ p a b * (1 + ε ↑(r i x))
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
n₀_le_r : ∀ (i : α), n₀ ≤ r i n
r_le_n : ∀ (i : α), r i n < n
⊢ ∀ C ≥ 2 * c₁⁻¹,
    (∀ m ∈ Ico n₀ n, T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)) → T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)

Tactic:
intro C hC h_ind

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
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)
⊢ T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)