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

Goal state before:
pp: case refine_2
V : Type u_1
R : Type u_2
inst✝⁷ : Fintype V
G : SimpleGraph V
inst✝⁶ : DecidableRel G.Adj
inst✝⁵ : DecidableEq V
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
x : V → R
⊢ 0 ≤ (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
positivity

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ 0 ≤ ↑t'

Tactic:
positivity

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ 0 ≤ ↑(t'.choose t) ^ r * ↑t

Tactic:
positivity

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ 0 < ↑(t'.choose t) ^ r * ↑t + ↑r * ↑t'

Tactic:
positivity

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ 0 < ↑t'

Tactic:
positivity

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

Goal state before:
pp: case e'_3
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
hn : u ≠ v
⊢ 2 = {u, v}.card

Tactic:
simp [hn]

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ ∃ G', G'.IsAlternating M.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
refine ⟨p.toSubgraph.spanningCoe ⊔ edge x a, (hcalt.spanningCoe p.toSubgraph).sup_edge (by simpa)
    (fun u' hu'x hadj ↦ ?_) aux, ?_, ?_, by aesop, sup_le_iff.mpr ⟨hle, fun v w hvw ↦ ?_⟩⟩

Goal state after:
case refine_1
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
u' : V
hu'x : u' ≠ x
hadj : p.toSubgraph.spanningCoe.Adj a u'
⊢ M.spanningCoe.Adj a u'

case refine_2
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ (p.toSubgraph.spanningCoe ⊔ edge x a).IsCycles

case refine_3
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ ¬(p.toSubgraph.spanningCoe ⊔ edge x a).Adj x b

case refine_4
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
v w : V
hvw : (edge x a).Adj v w
⊢ (G ⊔ edge a c).Adj v w
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ ν : YoungDiagram
⊢ IsLowerSet ↑(μ.cells ∩ ν.cells)

Tactic:
rw [Finset.coe_inter]

Goal state after:
μ ν : YoungDiagram
⊢ IsLowerSet (↑μ.cells ∩ ↑ν.cells)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
⊢ Primrec₂ fun p ↦ encode

Tactic:
by exact encode_iff.mpr snd

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
d : α
⊢ Primrec₂ fun l n ↦ l.getD n d

Tactic:
simp only [List.getD_eq_getElem?_getD]
  exact option_getD.comp₂ list_getElem? (const _)

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case false
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
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
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h : n ≤ m
⊢ false ∈ p n

Tactic:
rcases h.lt_or_eq_dec with h | h

Goal state after:
case false.inl
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
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
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h✝ : n ≤ m
h : n < m
⊢ false ∈ p n

case false.inr
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
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
pm : (p m).Dom
e : (p m).get pm = false
n : ℕ
h✝ : n ≤ m
h : n = m
⊢ false ∈ p n
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(encode (f a)).ppred = map encode ↑(f a)

Tactic:
cases f a <;> simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a ↦
    Option.casesOn (Sum.casesOn (f a) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)
a : α
⊢ (Option.casesOn (Sum.casesOn (f a) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (f a) (fun b ↦ Part.some (g a b)) (h a))

Tactic:
cases f a <;> simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
⊢ Sum.casesOn (Sum.casesOn (f a) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2) (fun b ↦ Part.some (h a b))
      (g a) =
    Sum.casesOn (f a) (g a) fun c ↦ Part.some (h a c)

Tactic:
cases f a <;> simp

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ (ack (m + 1) 0 + 1) ^ 2 ≤ ack (m + 1 + 3) 0

Tactic:
rw [ack_succ_zero, ack_succ_zero]
    apply ack_add_one_sq_lt_ack_add_three

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case prec
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n ↦ rec (f z) (fun y IH ↦ g (pair z (pair y IH))) n) n < ack m n

Tactic:
obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    -- We prove this simpler inequality first.
    have :
      ∀ {m n},
        rec (f m) (fun y IH => g <| pair m <| pair y IH) n < ack (max a b + 9) (m + n) := by
      intro m n
      -- We induct on n.
      induction n with
      | zero => -- The base case is easy.
        apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
        lia
      | succ n IH => -- We get rid of the first `pair`.
        simp only
        apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
        -- If m is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ m with h₁ | h₁
        · rw [max_eq_left h₁.le]
          gcongr <;> omega
        rw [max_eq_right h₁]
        -- We get rid of the second `pair`.
        apply (ack_pair_lt _ _ _).le.trans
        -- If n is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ n with h₂ | h₂
        · rw [max_eq_left h₂.le, add_assoc]
          exact
            ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp)
              ((le_succ n).trans <| self_le_add_left _ _)
        rw [max_eq_right h₂]
        -- We now use the inductive hypothesis, and some simple algebraic manipulation.
        apply (ack_strictMono_right _ IH).le.trans
        rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]
        exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)
    -- The proof is now simple.
    exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩

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

Goal state before:
pp: case ineq
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 : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀) → f z = 0
z : ℝ
hx :
  z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) →
    f z ∈ Set.Icc (c₁ * f (2 ^ (-↑k - 1) * x₀)) (c₂ * f (2 ^ (-↑k - 1) * x₀))
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
⊢ 2 ^ (-↑k - 1) * x₀ ∈ Set.Icc (2 ^ (-↑k - 1) * x₀) (2 ^ (-↑k) * x₀)

pp: case succ
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 : ℝ
hx :
  z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) →
    f z ∈ Set.Icc (c₁ * f (2 ^ (-↑k - 1) * x₀)) (c₂ * f (2 ^ (-↑k - 1) * x₀))
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
⊢ f z = 0

Tactic:
case ineq =>
        rw [Set.left_mem_Icc]
        gcongr
        · norm_num
        · lia

Goal state after:
case succ
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 : ℝ
hx :
  z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) →
    f z ∈ Set.Icc (c₁ * f (2 ^ (-↑k - 1) * x₀)) (c₂ * f (2 ^ (-↑k - 1) * x₀))
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
⊢ f z = 0
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‖
⊢ 0 < b (min_bi b) / 2

Tactic:
positivity

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)
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 : ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑n‖
hn' : ∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)
i : α
⊢ 0 ≤ ↑n

Tactic:
positivity

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

Goal state before:
pp: p x : ℝ
hx : 1 < x
⊢ x ≠ 0

Tactic:
positivity

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

Goal state before:
pp: p x : ℝ
hx : 0 < x
⊢ 0 < x

Tactic:
positivity

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

Goal state before:
pp: p x : ℝ
hx : 0 < x
⊢ 0 < ?m.422

Tactic:
positivity

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)
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
⊢ 0 ≤ ↑n / log ↑n ^ 2

Tactic:
positivity

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)
⊢ 0 < b (min_bi b) / 2

Tactic:
positivity

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 c : ℝ
hc_mem : c ∈ Set.Ioo 0 1
hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)
n : ℕ
hn₁ : ⌈C / c⌉₊ ≤ n
hn₂ : ∀ (i : α), c * ↑n ≤ ↑(r i n)
i : α
h₁ : 0 < c
⊢ c ≠ 0

Tactic:
positivity

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

Goal state before:
pp: p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x ↦ 1 - ε x) x = x⁻¹ / log x ^ 2
hx_pos : 1 < x
⊢ 0 ≤ x⁻¹ / log x ^ 2

Tactic:
positivity

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
a✝¹ : ℝ
a✝ : 0 < a✝¹
⊢ 0 ≤ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) a✝¹‖

Tactic:
positivity

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)
⊢ 0 < c

Tactic:
positivity

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

Goal state before:
pp: p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x ↦ 1 + ε x) x = -x⁻¹ / log x ^ 2
hx_pos : 1 < x
⊢ 0 ≤ x⁻¹ / log x ^ 2

Tactic:
positivity

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
⊢ 0 < (1 - b (max_bi b)) / 2

Tactic:
positivity

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
a✝¹ : ℝ
a✝ : 0 < a✝¹
⊢ 0 ≤ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) a✝¹‖

Tactic:
positivity

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
this : 0 < b (min_bi b)
⊢ 0 < b'

Tactic:
positivity

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₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ 0 < x / x₀

Tactic:
positivity

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 : α
⊢ 0 ≤ ↑n / log ↑n ^ 2

Tactic:
positivity

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 : α
⊢ 0 ≤ ↑n

Tactic:
positivity

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₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ 0 ≤ x / x₀

Tactic:
positivity

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

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ 0 < x

Tactic:
positivity

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

Goal state before:
pp: x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ x ≠ 0

Tactic:
positivity

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₀
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:
rw [← div_le_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_neg, Int.cast_natCast, neg_neg]
    have : 0 ≤ -logb 2 (x / x₀) := by
      rw [neg_nonneg]
      refine logb_nonpos (by norm_num) (by positivity) ?_
      rw [div_le_one x₀_pos]
      exact le_of_max_le_left hx₀_ge
    exact_mod_cast Nat.floor_le this

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)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
positivity

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)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
this : 0 < b i
⊢ b i ^ p a b ≠ 0

Tactic:
positivity

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

Goal state before:
pp: h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖
x : ℝ
a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖
hx' : 1 < x
this : 0 < log x
⊢ 0 < 1 + 1 / log x

Tactic:
positivity

Goal state after: