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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
n : ℕ
hn : ⌈(b i)⁻¹⌉₊ < n
hn' : 1 < n
h₁ : 0 < b i
⊢ ↑n ∈ Set.Ioi 1

Tactic:
rwa [Set.mem_Ioi, Nat.one_lt_cast]

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

Goal state before:

Tactic:
(fun (n : ℕ) => 1 / log (b i * n) - 1 / log n)
    _ =ᶠ[atTop] fun (n : ℕ) => (log n - log (b i * n)) / (log (b i * n) * log n) := by
      filter_upwards [eventually_gt_atTop 1, R.eventually_log_b_mul_pos] with n hn hn'
      have h_log_pos : 0 < log n := Real.log_pos <| by simp_all
      simp only [one_div]
      rw [inv_sub_inv (by have := hn' i; positivity) (by aesop)]
    _ =ᶠ[atTop] (fun (n : ℕ) ↦ (log n - log (b i) - log n) / ((log (b i) + log n) * log n)) := by
      filter_upwards [eventually_ne_atTop 0] with n hn
      have : 0 < b i := R.b_pos i
      rw [log_mul (by positivity) (by simp_all), sub_add_eq_sub_sub]
    _ = (fun (n : ℕ) => -log (b i) / ((log (b i) + log n) * log n)) := by ext; congr; ring
    _ ~[atTop] (fun (n : ℕ) => -log (b i) / (log n * log n)) := by
      refine IsEquivalent.div (IsEquivalent.refl) <| IsEquivalent.mul ?_ (IsEquivalent.refl)
      have : (fun (n : ℕ) => log (b i) + log n) = fun (n : ℕ) => log n + log (b i) := by
        ext; simp [add_comm]
      rw [this]
      exact IsEquivalent.add_isLittleO IsEquivalent.refl
        <| IsLittleO.natCast_atTop (f := fun (_ : ℝ) => log (b i))
          isLittleO_const_log_atTop
    _ = (fun (n : ℕ) => -log (b i) / (log n) ^ 2) := by ext; congr 1; rw [← pow_two]

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
⊢ StrictAnti fun p ↦ ∑ i, a i * b i ^ p

Tactic:
rw [← Finset.sum_fn]
  refine Finset.sum_induction_nonempty _ _ (fun _ _ => StrictAnti.add) univ_nonempty ?terms
  refine fun i _ => StrictAnti.const_mul ?_ (R.a_pos i)
  exact Real.strictAnti_rpow_of_base_lt_one (R.b_pos i) (R.b_lt_one 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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
this : 0 < b i
⊢ q (b i * ↑n) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)

Tactic:
simp only [q, mul_rpow (by positivity : (0 : ℝ) ≤ b i) (by positivity : (0 : ℝ) ≤ n)]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
this : 0 < b i
⊢ b i ^ p a b * ↑n ^ p a b * (1 - ε (b i * ↑n)) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) =
    b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: case hc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ x ^ p a b) x

pp: case hd
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1 + ε x) x

Tactic:
<;>

Goal state after:
case hc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ x ^ p a b) x

case hd
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
x : ℝ
hx : x ≠ 0
hx' : 1 < x
⊢ DifferentiableAt ℝ (fun x ↦ 1 + ε x) 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
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
this : 0 < b i
⊢ q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)

Tactic:
simp only [q, mul_rpow (by positivity : (0 : ℝ) ≤ b i) (by positivity : (0 : ℝ) ≤ n)]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
h_main_norm : (fun n ↦ ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n ↦ ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖
h_main : (fun n ↦ q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n ↦ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
n : ℕ
hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
this : 0 < b i
⊢ b i ^ p a b * ↑n ^ p a b * (1 + ε (b i * ↑n)) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) =
    b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
⊢ (fun b ↦ succ.comp b)^[0] zero = Code.const 0

pp: case succ
n✝ : ℕ
a✝ : (fun b ↦ succ.comp b)^[n✝] zero = Code.const n✝
⊢ (fun b ↦ succ.comp b)^[n✝ + 1] zero = Code.const (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
⊢ (fun b ↦ succ.comp b)^[0] zero = Code.const 0

case succ
n✝ : ℕ
a✝ : (fun b ↦ succ.comp b)^[n✝] zero = Code.const n✝
⊢ (fun b ↦ succ.comp b)^[n✝ + 1] zero = Code.const (n✝ + 1)
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 ∈ evaln (k + 1) zero n
⊢ n < k + 1

pp: case succ
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h : x ∈ evaln (k + 1) succ n
⊢ n < k + 1

pp: case left
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h : x ∈ evaln (k + 1) left n
⊢ n < k + 1

pp: case right
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h : x ∈ evaln (k + 1) right n
⊢ n < k + 1

pp: case pair
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h : x ∈ evaln (k + 1) (a✝¹.pair a✝) n
⊢ n < k + 1

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

pp: case prec
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h : x ∈ evaln (k + 1) (a✝¹.prec a✝) n
⊢ n < k + 1

pp: case rfind'
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝ : Code
h : x ∈ evaln (k + 1) a✝.rfind' 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 ∈ evaln (k + 1) zero n
⊢ n < k + 1

case succ
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h : x ∈ evaln (k + 1) succ n
⊢ n < k + 1

case left
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h : x ∈ evaln (k + 1) left n
⊢ n < k + 1

case right
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
h : x ∈ evaln (k + 1) right n
⊢ n < k + 1

case pair
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h : x ∈ evaln (k + 1) (a✝¹.pair a✝) n
⊢ n < k + 1

case comp
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h : x ∈ evaln (k + 1) (a✝¹.comp a✝) n
⊢ n < k + 1

case prec
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝¹ a✝ : Code
h : x ∈ evaln (k + 1) (a✝¹.prec a✝) n
⊢ n < k + 1

case rfind'
k n x : ℕ
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
a✝ : Code
h : x ∈ evaln (k + 1) a✝.rfind' n
⊢ n < k + 1
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
k n x : ℕ
h : x ∈ evaln (k + 1) zero n
⊢ x ∈ zero.eval n

pp: case succ
k n x : ℕ
h : x ∈ evaln (k + 1) succ n
⊢ x ∈ succ.eval n

pp: case left
k n x : ℕ
h : x ∈ evaln (k + 1) left n
⊢ x ∈ left.eval n

pp: case right
k n x : ℕ
h : x ∈ evaln (k + 1) right n
⊢ x ∈ right.eval n

pp: case pair
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : x ∈ evaln (k + 1) (a✝¹.pair a✝) n
⊢ x ∈ (a✝¹.pair a✝).eval n

pp: case comp
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : x ∈ evaln (k + 1) (a✝¹.comp a✝) n
⊢ x ∈ (a✝¹.comp a✝).eval n

pp: case prec
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : x ∈ evaln (k + 1) (a✝¹.prec a✝) n
⊢ x ∈ (a✝¹.prec a✝).eval n

pp: case rfind'
k : ℕ
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : x ∈ evaln (k + 1) a✝.rfind' n
⊢ x ∈ a✝.rfind'.eval n

Tactic:
<;>

Goal state after:
case zero
k n x : ℕ
h : x ∈ evaln (k + 1) zero n
⊢ x ∈ zero.eval n

case succ
k n x : ℕ
h : x ∈ evaln (k + 1) succ n
⊢ x ∈ succ.eval n

case left
k n x : ℕ
h : x ∈ evaln (k + 1) left n
⊢ x ∈ left.eval n

case right
k n x : ℕ
h : x ∈ evaln (k + 1) right n
⊢ x ∈ right.eval n

case pair
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : x ∈ evaln (k + 1) (a✝¹.pair a✝) n
⊢ x ∈ (a✝¹.pair a✝).eval n

case comp
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : x ∈ evaln (k + 1) (a✝¹.comp a✝) n
⊢ x ∈ (a✝¹.comp a✝).eval n

case prec
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : x ∈ evaln (k + 1) (a✝¹.prec a✝) n
⊢ x ∈ (a✝¹.prec a✝).eval n

case rfind'
k : ℕ
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : x ∈ evaln (k + 1) a✝.rfind' n
⊢ x ∈ a✝.rfind'.eval n
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case pos
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n x : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
h₂ : (if m = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
m0 : m = 0
⊢ ∃ a,
    (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x

pp: case neg
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n x : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
h₂ : (if m = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
m0 : ¬m = 0
⊢ ∃ a,
    (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x

Tactic:
<;>

Goal state after:
case pos
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n x : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
h₂ : (if m = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
m0 : m = 0
⊢ ∃ a,
    (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x

case neg
k : ℕ
cf : Code
hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n
n x : ℕ
left✝ : n ≤ k
m : ℕ
h₁ : evaln (k + 1) cf n = some m
h₂ : (if m = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
m0 : ¬m = 0
⊢ ∃ a,
    (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x
Module: Mathlib.Computability.Language

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
⊢ (if 0 + 1 = 0 then 0 else 1) = (if 0 = 0 then 0 else 1) + 1

pp: case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n✝ : ℕ
⊢ (if n✝ + 1 + 1 = 0 then 0 else 1) = (if n✝ + 1 = 0 then 0 else 1) + 1

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
⊢ (if 0 + 1 = 0 then 0 else 1) = (if 0 = 0 then 0 else 1) + 1

case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n✝ : ℕ
⊢ (if n✝ + 1 + 1 = 0 then 0 else 1) = (if n✝ + 1 = 0 then 0 else 1) + 1
Module: Mathlib.Computability.Language

Goal state before:
pp: case succ.mpr.nil
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
hn : [].length = n + 1
hS : ∀ y ∈ [], y ∈ l
⊢ ∃ a ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = [].flatten

pp: case succ.mpr.cons
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
a : List α
S : List (List α)
hn : (a :: S).length = n + 1
hS : ∀ y ∈ a :: S, y ∈ l
⊢ ∃ a_1 ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a_1 ++ b = (a :: S).flatten

Tactic:
<;>

Goal state after:
case succ.mpr.nil
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
hn : [].length = n + 1
hS : ∀ y ∈ [], y ∈ l
⊢ ∃ a ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a ++ b = [].flatten

case succ.mpr.cons
α : Type u_1
l : Language α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
a : List α
S : List (List α)
hn : (a :: S).length = n + 1
hS : ∀ y ∈ a :: S, y ∈ l
⊢ ∃ a_1 ∈ l, ∃ b, (∃ S, b = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l) ∧ a_1 ++ b = (a :: S).flatten
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
l m : Language α
h : m * l ≤ m
n : ℕ
⊢ m * l ^ n ≤ m

Tactic:
induction n with
    | zero => simp
    | succ n ih => grw [pow_succ, ← mul_assoc m (l ^ n) l, ih, h]

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:
rw [rewrites_iff] at *

Goal state after:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
⊢ ∃ p_1 q, p ++ u = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ v = p_1 ++ r.output ++ q
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 (u ++ p) (v ++ p)

Tactic:
rw [rewrites_iff] at *

Goal state after:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
hvw : ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
p : List (Symbol T N)
⊢ ∃ p_1 q, u ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ v ++ p = p_1 ++ r.output ++ q
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
r : ContextFreeRule T N
x : Symbol T N
u v : List (Symbol T N)
h : r.Rewrites u v
⊢ r.reverse.Rewrites (x :: u).reverse (x :: v).reverse

Tactic:
simpa using h.reverse.append_right _

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case e'_2
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
⊢ g = g.reverse.reverse

pp: case e'_3
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
e_2✝ : g = g.reverse.reverse
⊢ u = u.reverse.reverse

pp: case e'_4
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
e_2✝ : g = g.reverse.reverse
⊢ v = v.reverse.reverse

Tactic:
<;>

Goal state after:
case e'_2
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
⊢ g = g.reverse.reverse

case e'_3
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
e_2✝ : g = g.reverse.reverse
⊢ u = u.reverse.reverse

case e'_4
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
h : g.reverse.Derives u.reverse v.reverse
e_2✝ : g = g.reverse.reverse
⊢ v = v.reverse.reverse
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t

Tactic:
by
  obtain ⟨n, m, hneq, heq⟩ :=
    Fintype.exists_ne_map_eq_of_card_lt
      (fun n : Fin (Fintype.card σ + 1) => M.evalFrom s (x.take n)) (by simp)
  wlog hle : (n : ℕ) ≤ m generalizing n m
  · exact this m n hneq.symm heq.symm (le_of_not_ge hle)
  refine
    ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n,
                    x.drop m, ?_, ?_, ?_, by rfl, ?_⟩
  · rw [List.take_append_drop, List.take_append_drop]
  · simp only [List.length_drop, List.length_take]
    omega
  · intro h
    have hlen' := congr_arg List.length h
    simp only [List.length_drop, List.length, List.length_take] at hlen'
    omega
  have hq : M.evalFrom (M.evalFrom s ((x.take m).take n)) ((x.take m).drop n) =
      M.evalFrom s ((x.take m).take n) := by
    rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]
  use hq
  rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc,
    List.take_append_drop, List.take_append_drop]

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ x ∈ (comap f M).accepts ↔ x ∈ List.map f ⁻¹' M.accepts

Tactic:
conv =>
    rhs
    rw [Set.mem_preimage, mem_accepts]

Goal state after:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ x ∈ (comap f M).accepts ↔ M.eval (List.map f x) ∈ M.accept
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h✝ : f true false = true
⊢ 0 = 0

pp: case neg
f : Bool → Bool → Bool
h✝ : ¬f true false = true
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
f : Bool → Bool → Bool
h✝ : f true false = true
⊢ 0 = 0

case neg
f : Bool → Bool → Bool
h✝ : ¬f true false = true
⊢ 0 = 0
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case false
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (false.toNat = 1) = false

pp: case true
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (true.toNat = 1) = true

Tactic:
<;>

Goal state after:
case false
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (false.toNat = 1) = false

case true
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (true.toNat = 1) = true
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: case zero
b : Bool
m : ℕ
h : m ≠ 0
⊢ shiftLeft' b m 0 ≠ 0

pp: case succ
b : Bool
m : ℕ
h : m ≠ 0
n✝ : ℕ
a✝ : shiftLeft' b m n✝ ≠ 0
⊢ shiftLeft' b m (n✝ + 1) ≠ 0

Tactic:
<;>

Goal state after:
case zero
b : Bool
m : ℕ
h : m ≠ 0
⊢ shiftLeft' b m 0 ≠ 0

case succ
b : Bool
m : ℕ
h : m ≠ 0
n✝ : ℕ
a✝ : shiftLeft' b m n✝ ≠ 0
⊢ shiftLeft' b m (n✝ + 1) ≠ 0
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
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ^ p ≤ (c₂ * f x) ^ p

Tactic:
by gcongr; exact (hf₁ u hu).2

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

Goal state before:
pp: f : Bool → Bool → Bool
⊢ bitwise f = fun n ↦
    binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
      (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) n

Tactic:
funext x y

Goal state after:
f : Bool → Bool → Bool
x y : ℕ
⊢ bitwise f x y =
    binaryRec (motive := fun x ↦ ℕ → ℕ) (fun n ↦ bif f false true then n else 0)
      (fun a m Ia n ↦ binaryRec (bif f true false then bit a m else 0) (fun b n x ↦ bit (f a b) (Ia n)) n) x y
Module: Mathlib.Data.Num.Bitwise

Goal state before:
pp: case false
⊢ (false::zero false) = zero false

pp: case true
⊢ (true::zero true) = zero true

Tactic:
<;>

Goal state after:
case false
⊢ (false::zero false) = zero false

case true
⊢ (true::zero true) = zero true
Module: Mathlib.Data.Num.Bitwise

Goal state before:
pp: case false
⊢ (false::zero (decide ¬false = true)) = nz (msb false)

pp: case true
⊢ (true::zero (decide ¬true = true)) = nz (msb true)

Tactic:
<;>

Goal state after:
case false
⊢ (false::zero (decide ¬false = true)) = nz (msb false)

case true
⊢ (true::zero (decide ¬true = true)) = nz (msb true)