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

Goal state before:
pp: m : ℕ
⊢ ack (m + 1) 0 = ack m 1

Tactic:
by rw [ack]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ ack (m + 1) (n + 1) = ack m (ack (m + 1) n)

Tactic:
by rw [ack]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 2 ^ (n + 3) + 3 - (3 + 3) = 2 * 2 ^ (n + 3) - 3

pp: case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)

Tactic:
Nat.add_sub_add_right

Goal state after:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 2 ^ (n + 3) - 3 = 2 * 2 ^ (n + 3) - 3

case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, c * f ↑n ≤ f u

Tactic:
obtain ⟨c, hc_mem, hc⟩ := hf.eventually_atTop_ge hb
  exact ⟨c, hc_mem, hc.natCast_atTop⟩

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

Goal state before:
pp: case zero
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 : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u ∈ Set.Icc (c₁ * f x₀) (c₂ * f x₀)
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
⊢ ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-1) * x₀) x₀ → f z = 0

Tactic:
simp only [hx₀, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx

Goal state after:
case zero
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₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
⊢ ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-1) * x₀) x₀ → f z = 0
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case inl
p : ℝ
hp : p = 0
h₁ : (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖) =ᶠ[atTop] fun z ↦ z⁻¹ / log z ^ 2
⊢ GrowsPolynomially fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖

Tactic:
refine GrowsPolynomially.congr_of_eventuallyEq h₁ ?_

Goal state after:
case inl
p : ℝ
hp : p = 0
h₁ : (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖) =ᶠ[atTop] fun z ↦ z⁻¹ / log z ^ 2
⊢ GrowsPolynomially fun z ↦ z⁻¹ / log z ^ 2
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case inl
p : ℝ
hp : p = 0
h₁ : (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z ↦ z⁻¹ / log z ^ 2
⊢ GrowsPolynomially fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖

Tactic:
refine GrowsPolynomially.congr_of_eventuallyEq h₁ ?_

Goal state after:
case inl
p : ℝ
hp : p = 0
h₁ : (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z ↦ z⁻¹ / log z ^ 2
⊢ GrowsPolynomially fun z ↦ z⁻¹ / log z ^ 2
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 : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ 0 ≤ g ↑n

Tactic:
simp_all

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

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 + ε x) x = deriv ε x

Tactic:
rw [deriv_fun_add]

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1) x + deriv ε x = deriv ε x

case hf
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1) x

case hg
x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ ε 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
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * ↑n)
⊢ 1 < ↑n

Tactic:
simp_all

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 : n ≠ 0
this : 0 < b i
⊢ ↑n ≠ 0

Tactic:
simp_all

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
⊢ ∃ a, ?m.28 a = ?m.29

Tactic:
by rw [← Set.mem_range]; exact R.one_mem_range_sumCoeffsExp

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

Goal state before:
pp: case inl.inr
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, g x ≤ 0
⊢ GrowsPolynomially fun x ↦ f x * g x

Tactic:
have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonneg hx₁, abs_of_nonpos hx₂]

Goal state after:
case inl.inr
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, g x ≤ 0
hmain : (fun x ↦ f x * g x) =ᶠ[atTop] fun x ↦ -|f x| * |g x|
⊢ GrowsPolynomially fun x ↦ f x * g x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
⊢ GrowsPolynomially fun x ↦ f x * g x

Tactic:
suffices GrowsPolynomially fun x => |f x| * |g x| by
    cases eventually_atTop_nonneg_or_nonpos hf with
    | inl hf' =>
      cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]
        rwa [iff_eventuallyEq hmain]
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonneg hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg
    | inr hf' =>
      cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain]
        exact this
  intro b hb
  have hf := hf.abs b hb
  have hg := hg.abs b hb
  obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf
  obtain ⟨c₃, hc₃_mem, c₄, hc₄_mem, hg⟩ := hg
  refine ⟨c₁ * c₃, by change 0 < c₁ * c₃; positivity, ?_⟩
  refine ⟨c₂ * c₄, by change 0 < c₂ * c₄; positivity, ?_⟩
  filter_upwards [hf, hg] with x hf hg
  intro u hu
  refine ⟨?lb, ?ub⟩
  case lb => calc
    c₁ * c₃ * (|f x| * |g x|) = (c₁ * |f x|) * (c₃ * |g x|) := by ring
    _ ≤ |f u| * |g u| := by
           gcongr
           · exact (hf u hu).1
           · exact (hg u hu).1
  case ub => calc
    |f u| * |g u| ≤ (c₂ * |f x|) * (c₄ * |g x|) := by
           gcongr
           · exact (hf u hu).2
           · exact (hg u hu).2
    _ = c₂ * c₄ * (|f x| * |g x|) := by ring

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case refine_2
f : ℕ →. ℕ
⊢ (∃ c, c.eval = f) → Nat.Partrec f

Tactic:
rintro ⟨c, rfl⟩
    induction c with
    | zero => exact Nat.Partrec.zero
    | succ => exact Nat.Partrec.succ
    | left => exact Nat.Partrec.left
    | right => exact Nat.Partrec.right
    | pair cf cg pf pg => exact pf.pair pg
    | comp cf cg pf pg => exact pf.comp pg
    | prec cf cg pf pg => exact pf.prec pg
    | rfind' cf pf => exact pf.rfind'

Goal state after:
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' : ℝ := ⋯
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
⊢ 0 ≤ 1 + ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1)

Tactic:
refine add_nonneg zero_le_one <| Finset.sum_nonneg fun j _ => ?_

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 / ↑j ^ (p a b + 1)
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' : ℝ := ⋯
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
⊢ 0 ≤ 1 + ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1)

Tactic:
refine add_nonneg zero_le_one <| Finset.sum_nonneg fun j _ => ?_

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 : α), 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
j : ℕ
x✝ : j ∈ range (r i n)
⊢ 0 ≤ g ↑j / ↑j ^ (p a b + 1)
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
⊢ 1 + l∗ * l = l∗

Tactic:
rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar]

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ p ++ u = p ++ x ++ [Symbol.nonterminal r.input] ++ y ∧ p ++ v = p ++ x ++ r.output ++ y

Tactic:
simp_all

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 p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ ∃ p_1 q, u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q

Tactic:
use x, y ++ p

Goal state after:
case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ u ++ p = x ++ [Symbol.nonterminal r.input] ++ (y ++ p) ∧ v ++ p = x ++ r.output ++ (y ++ p)
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case h
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v p x y : List (Symbol T N)
hxy : u = x ++ [Symbol.nonterminal r.input] ++ y ∧ v = x ++ r.output ++ y
⊢ u ++ p = x ++ [Symbol.nonterminal r.input] ++ (y ++ p) ∧ v ++ p = x ++ r.output ++ (y ++ p)

Tactic:
simp_all

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

Goal state before:
pp: f : Bool → Bool → Bool
m n : ℕ
⊢ bitwise (swap f) m n = bitwise f n m

Tactic:
induction m using Nat.binaryRec' generalizing n with

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

Goal state before:
pp: n i : ℕ
⊢ n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i

Tactic:
refine eq_of_testBit_eq fun j => ?_

Goal state after:
n i j : ℕ
⊢ (n &&& 2 ^ i).testBit j = ((n.testBit i).toNat * 2 ^ i).testBit j
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
x✝ : 0 ≤ p ∨ p < 0
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun x ↦ f x ^ p) x) (c₂ * (fun x ↦ f x ^ p) x)

Tactic:
cases le_or_gt 0 p with

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

Goal state before:
pp: case h
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w✝ : List (Option α)
h : l = l₁ ++ w✝
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w✝ = replicate m none ++ some a :: replicate n none
⊢ True ∧ True ∧ True

Tactic:
and_self

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

Goal state before:
pp: α : Type u_1
l : List (Option α)
x : α
⊢ (l.concat (some x)).reduceOption = l.reduceOption.concat x

Tactic:
simp only [reduceOption_nil, concat_eq_append, reduceOption_append, reduceOption_cons_of_some]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
⊢ ¬Disjoint S (M.reverse.stepSet S' a) ↔ ¬Disjoint S' (M.stepSet S a)

Tactic:
simp only [Set.not_disjoint_iff, mem_stepSet, reverse_step, Set.mem_ofPred_eq]

Goal state after:
α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
t : σ
hx : M.IsPath s t x
right✝ : M.IsPath t u y
⊢ M.IsPath s u (x ++ y)

Tactic:
induction x generalizing s <;> cases hx <;> tauto

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ M.IsPath s₁ s₁ (List.replicate 0 none)

Tactic:
apply IsPath.nil

Goal state after:
Module: Mathlib.Computability.Halting

Goal state before:
pp: case pos
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c ↦ c.eval ∈ C
h : Computable fun a ↦ decide ((fun c ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun b ↦ if c.eval ∈ C then g b else f b
H : c.eval ∈ C
⊢ g ∈ C

Tactic:
simp_all

Goal state after:
Module: Mathlib.Computability.Halting

Goal state before:
pp: case neg
C : Set (ℕ →. ℕ)
f g : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
fC : f ∈ C
w✝ : DecidablePred fun c ↦ c.eval ∈ C
h : Computable fun a ↦ decide ((fun c ↦ c.eval ∈ C) a)
c : Code
e : c.eval = fun b ↦ if c.eval ∈ C then g b else f b
H : c.eval ∉ C
⊢ g ∈ C

Tactic:
simp_all

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

Goal state before:
pp: p : PosNum
⊢ castNum <$> (pos p).ppred = (↑(pos p)).ppred

Tactic:
rw [ppred, Option.map_eq_map, Option.map_some, Nat.ppred_eq_some.2]

Goal state after:
p : PosNum
⊢ (↑p.pred').succ = ↑(pos p)
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
s : Part ℕ
hf : RecursiveIn {fun x ↦ s} f
g : ℕ →. ℕ
hg : g ∈ {fun x ↦ s}
⊢ Partrec g

Tactic:
rw [Set.mem_singleton_iff.mp hg]; exact .const' s

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: d₁ d₂ d₃ : ManyOneDegree
⊢ d₁ ≤ d₂ → d₂ ≤ d₃ → d₁ ≤ d₃

Tactic:
induction d₁ using ManyOneDegree.ind_on
  induction d₂ using ManyOneDegree.ind_on
  induction d₃ using ManyOneDegree.ind_on
  apply ManyOneReducible.trans

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

Goal state before:
pp: case some
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
v : σ
L : ListBlank Γ
q : Stmt Γ Λ σ
R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))

Tactic:
induction q generalizing v L R with

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

Goal state before:
pp: case prim.prec
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval ↑v = pure <$> ↑f v
cg : Code
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval ↑v = pure <$> ↑g v
⊢ ∃ c,
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval ↑v = pure <$> (↑fun v ↦ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head) v

Tactic:
simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg

Goal state after:
case prim.prec
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf cg : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval ↑v = Part.some (pure (f v))
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval ↑v = Part.some (pure (g v))
⊢ ∃ c,
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval ↑v = pure <$> (↑fun v ↦ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head) v
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ :
  (cf.prec cg).eval (n :: (↑v).tail) =
    pure (pure (Nat.rec (f (n ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (n ::ᵥ v.tail).tail)) (n ::ᵥ v.tail).head))
this✝ :
  ∀ (a b : ℕ),
    a + b = n →
      n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
        PFun.fix
          (fun v ↦
            (cg.eval (v.headI :: v.tail.tail)).bind fun x ↦
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a :: b :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)
this :
  PFun.fix
      (fun v ↦
        (cg.eval (v.headI :: v.tail.tail)).bind fun x ↦
          Part.some
            (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
            else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
      (0 :: n :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) 0 :: (↑v).tail) =
    Part.some
      (n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail)
⊢ ((cf.eval (↑v).tail).bind fun x ↦
      (PFun.fix
            (fun v ↦
              (cg.eval (v.headI :: v.tail.tail)).bind fun y ↦
                Part.some
                  (if v.tail.headI = 0 then Sum.inl ((v.headI + 1) :: (v.tail.headI - 1) :: y.headI :: v.tail.tail.tail)
                  else Sum.inr ((v.headI + 1) :: (v.tail.headI - 1) :: y.headI :: v.tail.tail.tail)))
            (0 :: n :: x.headI :: (↑v).tail)).bind
        fun x ↦ Part.some [x.tail.tail.headI]) =
    Part.some [g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail)]

Tactic:
simp_all

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

Goal state before:
pp: n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n : ℕ),
        a'' = n :: ↑v →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : ¬[f (n ::ᵥ v)].headI = 0
this :
  Sum.inl v' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∧
        v' ∈
          PFun.fix
            (fun v ↦
              (cf.eval v).bind fun y ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a'
⊢ Sum.inr (n.succ :: ↑v) ∈
    (cf.eval (n :: ↑v)).bind fun y ↦
      Part.some
        (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
        else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))

Tactic:
simp_all

Goal state after: