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

Goal state before:

Tactic:
(fun z => z ^ (p - 1) / (log z ^ 2)) =o[atTop] fun z => z ^ (p - 1) / 1 := by
          simp_rw [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.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 : ℝ
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ ↑(r i n)

Tactic:
obtain ⟨c, hc_mem, hc⟩ := R.exists_eventually_const_mul_le_r
  filter_upwards [eventually_ge_atTop ⌈C / c⌉₊, hc] with n hn₁ hn₂ i
  have h₁ := hc_mem.1
  calc C
    _ = c * (C / c) := by
      rw [← mul_div_assoc]
      exact (mul_div_cancel_left₀ _ (by positivity)).symm
    _ ≤ c * ⌈C / c⌉₊ := by gcongr; simp [Nat.le_ceil]
    _ ≤ c * n := by gcongr
    _ ≤ r i n := hn₂ i

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)
⊢ (fun n ↦ q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n ↦ deriv q ↑n * (↑(r i n) - b i * ↑n)

Tactic:
rw [isBigO_iff]

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)
⊢ ∃ c, ∀ᶠ (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.AkraBazzi

Goal state before:
pp: case hbc
α : 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' : ℝ := ⋯
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)
h_tendsto : Tendsto (fun x ↦ b' * x) atTop atTop
n : ℕ
hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
h_ge_n₀ : R.n₀ ≤ n
h_n_pos : 0 < n
h_bn : 1 < b' * ↑n
⊢ b' ≤ b i

Tactic:
exact hb' i

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
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * ↑n)
h_log_pos : 0 < log ↑n
⊢ log (b i * ↑n) ≠ 0

Tactic:
have := hn' i; positivity

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

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

Tactic:
exact hf.neg

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

Goal state before:
pp: case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun x ↦ |f x|
⊢ GrowsPolynomially (-f)

Tactic:
exact hf.neg

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 : α
⊢ b' * ↑n ≤ ↑(r i n)

Tactic:
by grind

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 : α
⊢ n₀ ≤ r i n

Tactic:
exact_mod_cast
      calc n₀ ≤ b' * n := by
                have : (n₀ : ℝ) / b' ≤ n := by
                  exact_mod_cast calc
                    (n₀ : ℝ) / b' ≤ ⌈n₀ / b'⌉₊ := Nat.le_ceil (↑n₀ / b')
                    _ ≤ n := by exact_mod_cast n₀_div_le_n
                rwa [div_le_iff₀, mul_comm] at this
                grind only
        _ ≤ r i n := by grind

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
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
⊢ R.n₀ ≤ n

Tactic:
by grind

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
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
⊢ r i n ∈ Ico n₀ n

Tactic:
by grind

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

Goal state before:
pp: case hbc
α : 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
⊢ T (r i n) ≤ C * ((1 - ε ↑(r i n)) * asympBound g a b (r i n))

Tactic:
· exact h_ind (r i n) (by grind)

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

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

Tactic:
by grind

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

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

Tactic:
exact_mod_cast
      calc n₀ ≤ b' * n := by
                have : (n₀ : ℝ) / b' ≤ n := by
                  exact_mod_cast calc
                    (n₀ : ℝ) / b' ≤ ⌈n₀ / b'⌉₊ := Nat.le_ceil (↑n₀ / b')
                    _ ≤ n := by exact_mod_cast n₀_div_le_n
                rwa [div_le_iff₀, mul_comm] at this
                grind only
        _ ≤ r i n := by grind

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

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

Tactic:
by grind

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

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

Tactic:
· exact h_ind (r i n) (by grind)

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.h.inl
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
ih : ∀ m_1 < x.length, ∀ ⦃x : List α⦄, x ∈ l → x.length = m_1 → x ∈ m∗ * n
hx : x ∈ m * l
⊢ x ∈ m∗ * n

Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := mem_mul.mp hx
        rw [length_append] at ih
        have hal : 0 < a.length := length_pos_iff.mpr <| ne_of_mem_of_not_mem ha hm
        specialize ih b.length (Nat.lt_add_left_iff_pos.mpr hal) hb rfl
        rw [← one_add_self_mul_kstar_eq_kstar, one_add_mul, mul_assoc]
        right
        exact ⟨_, ha, _, ih, rfl⟩

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : r.Rewrites u v
p : List (Symbol T N)
⊢ r.Rewrites (p ++ u) (p ++ v)

Tactic:
by
  rw [rewrites_iff] at *
  rcases hvw with ⟨x, y, hxy⟩
  use p ++ x, y
  simp_all

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
⊢ asympBound g a b =O[atTop] T

Tactic:
by
  calc asympBound g a b
    _ = (fun n => 1 * asympBound g a b n) := by simp
    _ ~[atTop] (fun n => (1 + ε n) * asympBound g a b n) := by
      refine IsEquivalent.mul (IsEquivalent.symm ?_) IsEquivalent.refl
      rw [Function.const_def, isEquivalent_const_iff_tendsto one_ne_zero,
        ← Function.comp_def (fun n => 1 + ε n) Nat.cast]
      exact Tendsto.comp isEquivalent_one_add_smoothingFn_one.tendsto_const
        tendsto_natCast_atTop_atTop
    _ =O[atTop] T := R.smoothingFn_mul_asympBound_isBigO_T

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ x ∈ {x | (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept} ↔
    x ∈ {x | M1.evalFrom s1 x ∈ M1.accept} ∨ x ∈ {x | M2.evalFrom s2 x ∈ M2.accept}

Tactic:
↑Set.mem_ofPred

Goal state after:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ (M1.union M2).evalFrom (s1, s2) x ∈ (M1.union M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∨ M2.evalFrom s2 x ∈ M2.accept
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
⊢ (M1.union M2).accepts = M1.accepts + M2.accepts

Tactic:
simp [accepts]

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ x ∈ {x | (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept} ↔
    x ∈ {x | M1.evalFrom s1 x ∈ M1.accept} ∧ x ∈ {x | M2.evalFrom s2 x ∈ M2.accept}

Tactic:
↑Set.mem_ofPred

Goal state after:
α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
s1 : σ1
s2 : σ2
x : List α
⊢ (M1.inter M2).evalFrom (s1, s2) x ∈ (M1.inter M2).accept ↔ M1.evalFrom s1 x ∈ M1.accept ∧ M2.evalFrom s2 x ∈ M2.accept
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ1 σ2 : Type v
M1 : DFA α σ1
M2 : DFA α σ2
⊢ (M1.inter M2).accepts = M1.accepts ⊓ M2.accepts

Tactic:
simp [accepts]

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

Goal state before:
pp: case bit.succ
b : Bool
m : ℕ
e : bit b m ≠ 0
IH : ∀ {n : ℕ}, m < 2 ^ n → m.size ≤ n
n : ℕ
h : bit b m < 2 ^ (n + 1)
⊢ m.size.succ ≤ n + 1

Tactic:
| succ n =>

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

Goal state before:
pp: b : ℝ
hb : b ∈ Set.Ioo 0 1
hb₀ : 0 < b
h_tendsto : Tendsto (fun x ↦ 1 / 2 * log x) atTop atTop
x : ℝ
hx_pos : 1 < x
hx : ∀ (y : ℝ), b * id x ≤ y → -log b < 1 / 2 * log y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ log x + -1 / 2 * log x ≤ log x + log b

Tactic:
by grind

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

Goal state before:
pp: case succ
n : ℕ
h : Even (n + 1)
⊢ n + 1 ^^^ 1 = n + 1 + 1

Tactic:
| succ n =>

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

Goal state before:
pp: case succ
n : ℕ
h : Odd (n + 1)
⊢ n + 1 ^^^ 1 = n + 1 - 1

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p) = ↑p + ↑p

Tactic:
Nat.cast_add,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑↑p + ↑↑p = ↑p + ↑p
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p + 1) = ↑p + ↑p + 1

Tactic:
Nat.cast_add,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p) + ↑1 = ↑p + ↑p + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p) + ↑1 = ↑p + ↑p + 1

Tactic:
Nat.cast_add,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑↑p + ↑↑p + ↑1 = ↑p + ↑p + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

Tactic:
← IH

Goal state after:
case bit1.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = (m.cmp n).swap
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.lt Ordering.gt

Tactic:
← IH

Goal state after:
case bit1.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.gt Ordering.gt).swap =
    Ordering.casesOn (m.cmp n).swap Ordering.lt Ordering.lt Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (n.cmp m) Ordering.lt Ordering.gt Ordering.gt

Tactic:
← IH

Goal state after:
case bit0.bit1
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (Ordering.casesOn (m.cmp n) Ordering.lt Ordering.lt Ordering.gt).swap =
    Ordering.casesOn (m.cmp n).swap Ordering.lt Ordering.gt Ordering.gt
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = n.cmp m

Tactic:
← IH

Goal state after:
case bit0.bit0
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ (m.cmp n).swap = (m.cmp n).swap
Module: Mathlib.Data.List.ReduceOption

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

Tactic:
reduceOption_length_eq,

Goal state after:
α : Type u_1
l : List (Option α)
⊢ l.length = (filter Option.isSome l).length + (filter Option.isNone l).length
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true

Tactic:
reduceOption_length_eq,

Goal state after:
α : Type u_1
l : List (Option α)
⊢ (filter Option.isSome l).length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case nil
α : Type u_1
⊢ (¬∀ (x : Option α), x ∈ [] → x.isSome = true) ↔ none ∈ []

pp: case cons
α : Type u_1
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → x.isSome = true) ↔ none ∈ tail✝
⊢ (¬∀ (x : Option α), x ∈ head✝ :: tail✝ → x.isSome = true) ↔ none ∈ head✝ :: tail✝

Tactic:
· simp

Goal state after:
case cons
α : Type u_1
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → x.isSome = true) ↔ none ∈ tail✝
⊢ (¬∀ (x : Option α), x ∈ head✝ :: tail✝ → x.isSome = true) ↔ none ∈ head✝ :: tail✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
m n : PosNum
⊢ ↑(↑m + ↑n) = ↑m + ↑n

Tactic:
Nat.cast_add,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
m n : PosNum
⊢ ↑↑m + ↑↑n = ↑m + ↑n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
m n : Num
⊢ ↑(↑m + ↑n) = ↑m + ↑n

Tactic:
Nat.cast_add,

Goal state after:
α : Type u_1
inst✝ : AddMonoidWithOne α
m n : Num
⊢ ↑↑m + ↑↑n = ↑m + ↑n
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: case refine_2.refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝¹ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a✝ c✝ : σ
h : c✝ ∈ f a✝
x✝ : ReflTransGen (fun a b ↦ b ∈ f a) c✝ b
IH : b ∈ eval f c✝
⊢ b ∈ eval f a✝

Tactic:
· refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH⟩)
      rw [h]
      apply Part.mem_some

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

Goal state before:
pp: Γ : Type ?u.9
Γ' : Type ?u.8
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ ListBlank Γ'

Tactic:
apply l.liftOn (fun l ↦ ListBlank.mk (List.map f l))
  rintro l _ ⟨i, rfl⟩; refine Quotient.sound' (Or.inl ⟨i, ?_⟩)
  simp only [PointedMap.map_pt, List.map_append, List.map_replicate]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
n : ℕ
⊢ (map f l).nth n = f.f (l.nth n)

Tactic:
by
  refine l.induction_on fun l ↦ ?_
  simp only [ListBlank.map_mk, ListBlank.nth_mk, ← List.getD_default_eq_getI]
  rw [← List.getD_map _ _ f]
  simp

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

Goal state before:
pp: Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
⊢ ListBlank Γ'

Tactic:
by
  apply l.liftOn (fun l ↦ ListBlank.mk (l.flatMap f))
  rintro l _ ⟨i, rfl⟩; obtain ⟨n, e⟩ := hf; refine Quotient.sound' (Or.inl ⟨i * n, ?_⟩)
  rw [List.flatMap_append, mul_comm]; congr
  induction i with
  | zero => rfl
  | succ i IH =>
    simp only [IH, e, List.replicate_add, Nat.mul_succ, add_comm, List.replicate_succ,
      List.flatMap_cons]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑0 = ↑(pos one) >>> (n + 1)

Tactic:
rw [Nat.shiftRight_eq_div_pow]
    symm
    apply Nat.div_eq_of_lt
    simp

Goal state after: