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

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ rf
⊢ let PR := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg);
  let CO := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg);
  let PC := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg);
  let RF := fun a cf hf ↦ rf a (cf, hf);
  let F := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a);
  Primrec fun a ↦ F a (c a)

Tactic:
intro _ _ _ _ F

Goal state after:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ rf
PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf ↦ rf a (cf, hf)
F : α → Code → σ := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
⊢ Primrec fun a ↦ F a (c a)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH ↦ g (pair m (pair y IH))) n
⊢ ack (b + (4 + 4)) (ack (max a b + 8 + 1) (m + n)) ≤ ack (max a b + 8) (ack (max a b + 8 + 1) (m + n))

Tactic:
exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ p * z ^ (p - 1) * (1 + ε z) - z ^ (p - 1) / log z ^ 2) ~[atTop] fun z ↦ p * z ^ (p - 1)

Tactic:
refine IsEquivalent.add_isLittleO ?one ?two
      case one => calc
        (fun z => p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1) * 1 :=
              IsEquivalent.mul IsEquivalent.refl isEquivalent_one_add_smoothingFn_one
        _ = fun z => p * z ^ (p - 1) := by ext; ring
      case two => calc
        (fun z => -(z ^ (p - 1) / (log z ^ 2))) =o[atTop] fun z => z ^ (p - 1) / 1 := by
            simp_rw [isLittleO_neg_left, div_eq_mul_inv]
            refine IsBigO.mul_isLittleO (isBigO_refl _ _)
              (IsLittleO.inv_rev ?_ (by simp))
            rw [isLittleO_const_left]
            refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
            exact Tendsto.comp (g := fun z => z ^ 2)
              (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _

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 / x₀ ≤ 1

Tactic:
div_le_one x₀_pos

Goal state after:
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 ≤ 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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < 1 - ε ↑(r i n)

Tactic:
by
  rw [Filter.eventually_all]
  exact fun i => (R.tendsto_atTop_r_real i).eventually eventually_one_sub_smoothingFn_pos_real

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
⊢ let PR := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg);
  let CO := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg);
  let PC := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg);
  let RF := fun a cf hf ↦ rf a (cf, hf);
  let F := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a);
  Computable fun a ↦ F a (c a)

Tactic:
intro _ _ _ _ F

Goal state after:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg ↦ pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf ↦ rf a (cf, hf)
F : α → Code → σ := fun a c ↦ Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
⊢ Computable fun a ↦ F a (c a)
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
⊢ Tendsto (fun p ↦ ∑ i, a i * b i ^ p) atBot atTop

Tactic:
have h₁ : Tendsto (fun p : ℝ => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop :=
    Tendsto.const_mul_atTop (R.a_pos (max_bi b)) <| tendsto_rpow_atBot_of_base_lt_one _
      (by have := R.b_pos (max_bi b); linarith) (R.b_lt_one _)
  refine tendsto_atTop_mono (fun p => ?_) h₁
  refine Finset.single_le_sum (f := fun i => (a i : ℝ) * b i ^ p) (fun i _ => ?_) (mem_univ _)
  positivity [R.a_pos i, R.b_pos i]

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

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
x : ℝ
hx₁ : 0 ≤ f x
hx₂ : 0 ≤ g x
⊢ f x * g x = |f x| * |g x|

Tactic:
abs_of_nonneg hx₁,

Goal state after:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
x : ℝ
hx₁ : 0 ≤ f x
hx₂ : 0 ≤ g x
⊢ f x * g x = f x * |g 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
⊢ 1 / 2 < 1 - ε ↑n →
    (∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)) →
      ⌈↑n₀ / b'⌉₊ ≤ 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:
h_smoothing_gt_half

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
⊢ (∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)) →
    ⌈↑n₀ / b'⌉₊ ≤ 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)
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₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) cf a) fun y ↦ do
                let i ← evaln k (cf.prec cg) (Nat.pair a y)
                evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
⊢ Nat.rec (evaln (k + 1) cf (unpair n).1)
        (fun n_1 n_ih ↦
          (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
            evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        0 =
      some x →
    Nat.rec (evaln (k₂ + 1) cf (unpair n).1)
        (fun n_1 n_ih ↦
          (evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
            evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        0 =
      some x

Tactic:
simp [Option.bind_eq_some_iff]

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₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) cf a) fun y ↦ do
                let i ← evaln k (cf.prec cg) (Nat.pair a y)
                evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
⊢ evaln (k + 1) cf (unpair n).1 = some x → evaln (k₂ + 1) cf (unpair n).1 = some 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 : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
n : ℕ
hn : n₀ ≤ n
⊢ (∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))) →
    0 < 1 + ε ↑n →
      (∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n) →
        1 / 2 < 1 - ε ↑n →
          (∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)) →
            ⌈↑n₀ / b'⌉₊ ≤ n →
              ⌈rexp 1⌉₊ ≤ n →
                ∀ C ≥ 2 * c₁,
                  (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) →
                    (1 + ε ↑n) * asympBound g a b n ≤ C * T n

Tactic:
bound2

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))
⊢ 0 < 1 + ε ↑n →
    (∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n) →
      1 / 2 < 1 - ε ↑n →
        (∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)) →
          ⌈↑n₀ / b'⌉₊ ≤ n →
            ⌈rexp 1⌉₊ ≤ n →
              ∀ C ≥ 2 * c₁,
                (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) → (1 + ε ↑n) * asympBound g a b n ≤ C * T n
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
⊢ 1 / 2 < 1 - ε ↑n →
    (∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)) →
      ⌈↑n₀ / b'⌉₊ ≤ n →
        ⌈rexp 1⌉₊ ≤ n →
          ∀ C ≥ 2 * c₁,
            (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) → (1 + ε ↑n) * asympBound g a b n ≤ C * T n

Tactic:
h_smoothing_gt_half

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
⊢ (∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)) →
    ⌈↑n₀ / b'⌉₊ ≤ n →
      ⌈rexp 1⌉₊ ≤ n →
        ∀ C ≥ 2 * c₁,
          (∀ m ∈ Ico n₀ n, (1 + ε ↑m) * asympBound g a b m ≤ C * T m) → (1 + ε ↑n) * asympBound g a b n ≤ C * T n
Module: Mathlib.Computability.PartrecCode

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

Tactic:
simp [Option.bind_eq_some_iff]

Goal state after:
case zero
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
x : ℕ
⊢ evaln (k + 1) cf (unpair n).1 = some x → x ∈ cf.eval (unpair n).1
Module: Mathlib.Computability.PartrecCode

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

Tactic:
simp [Option.bind_eq_some_iff]

Goal state after:
case succ
k : ℕ
cf cg : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n
n : ℕ
left✝ : n ≤ k
m : ℕ
IH :
  ∀ (x : ℕ),
    Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          m =
        some x →
      x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) m
x : ℕ
⊢ ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 m) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair m x_1)) = some x →
        ∃
          a ∈
            Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
              m,
          x ∈ cg.eval (Nat.pair (unpair n).1 (Nat.pair m a))
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case prec.zero
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n₁ n x : ℕ
⊢ x ∈ Nat.rec (cf.eval n₁) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) 0 →
    ∃ k,
      n ≤ k ∧
        Nat.rec (evaln (k + 1) cf n₁)
            (fun n n_ih ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun i ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            0 =
          some x

Tactic:
simp [Option.bind_eq_some_iff]

Goal state after:
case prec.zero
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n₁ n x : ℕ
⊢ x ∈ cf.eval n₁ → ∃ k, n ≤ k ∧ evaln (k + 1) cf n₁ = some x
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case prec.zero
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n₁ n x : ℕ
⊢ x ∈ cf.eval n₁ → ∃ k, n ≤ k ∧ evaln (k + 1) cf n₁ = some x

Tactic:
intro h
      rcases hf h with ⟨k, hk⟩
      exact ⟨_, le_max_left _ _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk⟩

Goal state after:
Module: Mathlib.Computability.PartrecCode

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

Tactic:
simp [Option.bind_eq_some_iff]

Goal state after:
case prec.succ
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n₁ m : ℕ
IH :
  ∀ {n x : ℕ},
    x ∈ Nat.rec (cf.eval n₁) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m →
      ∃ k,
        n ≤ k ∧
          Nat.rec (evaln (k + 1) cf n₁)
              (fun n n_ih ↦
                (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun i ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
              m =
            some x
n x : ℕ
⊢ ∀ x_1 ∈ Nat.rec (cf.eval n₁) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m,
    x ∈ cg.eval (Nat.pair n₁ (Nat.pair m x_1)) →
      ∃ k,
        n ≤ k ∧
          ∃ a, evaln k (cf.prec cg) (Nat.pair n₁ m) = some a ∧ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair m a)) = some x
Module: Mathlib.Data.Num.Bitwise

Goal state before:
pp: C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (nz (msb b))

Tactic:
by rw [← bit_one]; exact s b (SNum.zero (Not b)) (z (Not b))

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case succ
i : ℕ
ih : ∀ (n : ℕ), n.testBit i = n.bits.getI i
n : ℕ
⊢ n.testBit (i + 1) = n.bits.getI (i + 1)

Tactic:
| succ i ih =>

Goal state after:
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.false
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j

pp: case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j

Tactic:
· simp [testBit_two_pow_of_ne hij]

Goal state after:
case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j

Tactic:
· simp [testBit_two_pow_of_ne hij]

Goal state after:
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.length = (filter Option.isSome l).length + (filter Option.isNone l).length

Tactic:
l.length_eq_length_filter_add Option.isSome,

Goal state after:
α : Type u_1
l : List (Option α)
⊢ (filter Option.isSome l).length + (filter (fun x ↦ !x.isSome) l).length =
    (filter Option.isSome l).length + (filter Option.isNone l).length
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ M.accepts
hlen : Fintype.card (Set σ) ≤ x.length
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Tactic:
by
  rw [← toDFA_correct] at hx ⊢
  exact M.toDFA.pumping_lemma hx hlen

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ M.toεNFA.εClosure S = S

Tactic:
ext a
  refine ⟨?_, εNFA.εClosure.base _⟩
  rintro (⟨_, h⟩ | ⟨_, _, h, _⟩)
  · exact h
  · cases h

Goal state after:
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
⊢ { l // BlankExtends l l₁ ∧ BlankExtends l l₂ }

Tactic:
by
  refine
    if hl : l₁.length ≤ l₂.length then ⟨l₁, BlankExtends.refl _, Or.elim h id fun h' ↦ ?_⟩
    else ⟨l₂, Or.elim h (fun h' ↦ ?_) id, BlankExtends.refl _⟩
  · exact (BlankExtends.refl _).above_of_le h' hl
  · exact (BlankExtends.refl _).above_of_le h' (le_of_not_ge hl)

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₂ : σ₂
⊢ ∃ c₁ c₂, Reaches f₂ a₂ c₂ ∧ tr c₁ c₂ ∧ Reaches f₁ a₁ c₁

Tactic:
exact ⟨_, _, ReflTransGen.refl, aa, ReflTransGen.refl⟩

Goal state after: