mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.AkraBazzi.SumTransform

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

Tactic:
]

Goal state after:
case hdb
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
u : ℕ
hu : r i n ≤ u ∧ u < n
⊢ ↑n ^ (p a b + 1) ≤ ↑u ^ (p a b + 1)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: 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
⊢ 1 * x = x

Tactic:
by ring

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

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
⊢ 0 < b'

Tactic:
]

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
⊢ ↑n₀ ≤ b' * ↑n

α : 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.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₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ p a b * (↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑n ^ (p a b + 1))) =
    ↑n ^ p a b * (↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑n ^ (p a b + 1)))

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
a : ℕ
⊢ Nat.rec (cf.eval (a, 0).1)
      (fun y IH ↦ do
        let i ← IH
        cg.eval (Nat.pair (a, 0).1 (Nat.pair y i)))
      (a, 0).2 =
    cf.eval a

Tactic:
]

Goal state after:
cf cg : Code
a : ℕ
⊢ Nat.rec (cf.eval (a, 0).1)
      (fun y IH ↦ do
        let i ← IH
        cg.eval (Nat.pair (a, 0).1 (Nat.pair y i)))
      (a, 0).2 =
    cf.eval a
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
a : ℕ
⊢ cf.eval (a, 0).1 = cf.eval a

Tactic:
]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
a k : ℕ
⊢ Nat.rec (cf.eval (a, k.succ).1)
      (fun y IH ↦ do
        let i ← IH
        cg.eval (Nat.pair (a, k.succ).1 (Nat.pair y i)))
      (a, k.succ).2 =
    (unpaired
          (fun a n ↦
            Nat.rec (cf.eval a)
              (fun y IH ↦ do
                let i ← IH
                cg.eval (Nat.pair a (Nat.pair y i)))
              n)
          (Nat.pair a k)).bind
      fun ih ↦ cg.eval (Nat.pair a (Nat.pair k ih))

Tactic:
]

Goal state after:
cf cg : Code
a k : ℕ
⊢ Nat.rec (cf.eval (a, k.succ).1)
      (fun y IH ↦ do
        let i ← IH
        cg.eval (Nat.pair (a, k.succ).1 (Nat.pair y i)))
      (a, k.succ).2 =
    (unpaired
          (fun a n ↦
            Nat.rec (cf.eval a)
              (fun y IH ↦ do
                let i ← IH
                cg.eval (Nat.pair a (Nat.pair y i)))
              n)
          (Nat.pair a k)).bind
      fun ih ↦ cg.eval (Nat.pair a (Nat.pair k ih))
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₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ (p a b + 1) * (c₂ * g ↑n / ↑n ^ (p a b + 1)) = c₂ * (↑n ^ (p a b + 1) / ↑n ^ (p a b + 1)) * g ↑n

Tactic:
]

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

Tactic:
]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure 0)
      n
⊢ n < k + 1

Tactic:
]

Goal state after:
case zero
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure 0)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure n.succ)
      n
⊢ n < k + 1

Tactic:
]

Goal state after:
case succ
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure n.succ)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case left
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).1)
      n
⊢ n < k + 1

Tactic:
]

Goal state after:
case left
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).1)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case right
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).2)
      n
⊢ n < k + 1

Tactic:
]

Goal state after:
case right
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).2)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case pair
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) a✝¹ n <*> evaln (k + 1) a✝ n)
      n
⊢ n < k + 1

Tactic:
]

Goal state after:
case pair
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) a✝¹ n <*> evaln (k + 1) a✝ n)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case comp
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        let x ← evaln (k + 1) a✝ n
        evaln (k + 1) a✝¹ x)
      n
⊢ n < k + 1

Tactic:
]

Goal state after:
case comp
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        let x ← evaln (k + 1) a✝ n
        evaln (k + 1) a✝¹ x)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case prec
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) a✝¹ a) fun y ↦ do
                let i ← evaln k (a✝¹.prec a✝) (Nat.pair a y)
                evaln (k + 1) a✝ (Nat.pair a (Nat.pair y i)))
            n)
      n
⊢ n < k + 1

Tactic:
]

Goal state after:
case prec
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) a✝¹ a) fun y ↦ do
                let i ← evaln k (a✝¹.prec a✝) (Nat.pair a y)
                evaln (k + 1) a✝ (Nat.pair a (Nat.pair y i)))
            n)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case rfind'
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) a✝ (Nat.pair a m)
              if x = 0 then pure m else evaln k a✝.rfind' (Nat.pair a (m + 1)))
            n)
      n
⊢ n < k + 1

Tactic:
]

Goal state after:
case rfind'
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝ : Code
h :
  x ∈
    (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) a✝ (Nat.pair a m)
              if x = 0 then pure m else evaln k a✝.rfind' (Nat.pair a (m + 1)))
            n)
      n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure 0)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure 0)
      n =
    some x

Tactic:
]

Goal state after:
case zero
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure 0)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure 0)
      n =
    some x
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure n.succ)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure n.succ)
      n =
    some x

Tactic:
]

Goal state after:
case succ
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure n.succ)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure n.succ)
      n =
    some x
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case ha
α : 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)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
i : α
a✝ : i ∈ univ
j : ℕ
x✝ : j ∈ range (r i n)
⊢ 0 ≤ g ↑j ∧ 0 ≤ ↑j ^ (p a b + 1) ∨ g ↑j ≤ 0 ∧ ↑j ^ (p a b + 1) ≤ 0

Tactic:
]

Goal state after:
case ha
α : 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)
C_pos : 0 ≤ C
g_pos : 0 ≤ g ↑n
i : α
a✝ : i ∈ univ
j : ℕ
x✝ : j ∈ range (r i n)
⊢ 0 ≤ g ↑j ∧ 0 ≤ ↑j ^ (p a b + 1) ∨ g ↑j ≤ 0 ∧ ↑j ^ (p a b + 1) ≤ 0
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case left
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).1)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure (unpair n).1)
      n =
    some x

Tactic:
]

Goal state after:
case left
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).1)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure (unpair n).1)
      n =
    some x
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case right
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).2)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure (unpair n).2)
      n =
    some x

Tactic:
]

Goal state after:
case right
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).2)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure (unpair n).2)
      n =
    some x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hfg : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun x ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun x ↦ f x + g x) x) (c₂ * (fun x ↦ f x + g x) x)

Tactic:
]

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hfg : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun x ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun x ↦ f x + g x) x) (c₂ * (fun x ↦ f x + g x) x)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case pair
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) a✝¹ n <*> evaln (k + 1) a✝ n)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        Nat.pair <$> evaln (k₂ + 1) a✝¹ n <*> evaln (k₂ + 1) a✝ n)
      n =
    some x

Tactic:
]

Goal state after:
case pair
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) a✝¹ n <*> evaln (k + 1) a✝ n)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        Nat.pair <$> evaln (k₂ + 1) a✝¹ n <*> evaln (k₂ + 1) a✝ n)
      n =
    some x