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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a ↦ Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n ↦ map (f a.1) ↑(decode n)
⊢ Computable₂ fun a n ↦ (decode n).bind (f a)

Tactic:
refine this.of_eq fun a => ?_

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a ↦ Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n ↦ map (f a.1) ↑(decode n)
a : α × ℕ
⊢ (Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n ↦ map (f a.1) ↑(decode n)) =
    (↑fun p ↦ (fun a n ↦ (decode n).bind (f a)) p.1 p.2) a
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a ↦ Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)
a : α
⊢ (Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)) =
    Option.casesOn (o a) (Part.some (f a)) (g a)

Tactic:
rcases o a with - | b

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a ↦ Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)
a : α
⊢ (Nat.casesOn (encode Option.none) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)) =
    Option.casesOn Option.none (Part.some (f a)) (g a)

case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a ↦ Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)
a : α
b : β
⊢ (Nat.casesOn (encode (Option.some b)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)) =
    Option.casesOn (Option.some b) (Part.some (f a)) (g a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
this :
  ∀ (a' : α),
    b ∈ f.fix a' → ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n

Tactic:
by
      rcases this _ h 0 (by simp [F]) with ⟨n, hn₁, hn₂⟩
      exact ⟨_, ⟨⟨_, hn₁⟩, fun {m} mn => hn₂ m mn (Nat.zero_le _)⟩, hn₁⟩

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 < ack m (ack (m + 1) n)

Tactic:
calc
      n + 1 + 1 ≤ m + (m + 1 + n + 1) := by lia
      _ ≤ m + ack (m + 1) n := by gcongr; exact add_add_one_le_ack ..
      _ < ack m (ack (m + 1) n) := add_lt_ack ..

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 : ℝ
⊢ (∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)) → 0 < x → f x = 0

Tactic:
hx

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)
⊢ 0 < x → f x = 0
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case case2
m : ℕ
hm : (pappAck m).eval 1 = Part.some (ack m 1)
⊢ (pappAck m.succ).eval 0 = Part.some (ack m.succ 0)

Tactic:
simp [pappAck, hm]

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case case3
m n : ℕ
hmn₁ : (pappAck.step (pappAck m)).eval n = Part.some (ack (m + 1) n)
hmn₂ : (pappAck m).eval (ack (m + 1) n) = Part.some (ack m (ack (m + 1) n))
⊢ (pappAck.step (pappAck m)).eval n.succ = Part.some (ack m.succ n.succ)

Tactic:
simp [hmn₁, hmn₂]

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

Goal state before:
pp: p x : ℝ
⊢ 1 < x → deriv (fun z ↦ z ^ p * (1 - ε z)) x = deriv (fun x ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x ↦ 1 - ε x) x

Tactic:
hx

Goal state after:
p x : ℝ
hx : 1 < x
⊢ deriv (fun z ↦ z ^ p * (1 - ε z)) x = deriv (fun x ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x ↦ 1 - ε x) x
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p x : ℝ
⊢ 1 < x →
    deriv (fun x ↦ 1 - ε x) x = x⁻¹ / log x ^ 2 →
      deriv (fun x ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x ↦ 1 - ε x) x =
        p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)

Tactic:
hx

Goal state after:
p x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 - ε x) x = x⁻¹ / log x ^ 2 →
    deriv (fun x ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x ↦ 1 - ε x) x =
      p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p x : ℝ
⊢ 0 < x →
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / log x ^ 2

Tactic:
hx

Goal state after:
p x : ℝ
hx : 0 < x
⊢ p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / log x ^ 2
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p x : ℝ
⊢ 1 < x → deriv (fun x ↦ x ^ p * (1 + ε x)) x = deriv (fun x ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x ↦ 1 + ε x) x

Tactic:
hx

Goal state after:
p x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ x ^ p * (1 + ε x)) x = deriv (fun x ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x ↦ 1 + ε x) x
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p x : ℝ
⊢ 1 < x →
    deriv (fun x ↦ 1 + ε x) x = -x⁻¹ / log x ^ 2 →
      deriv (fun x ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x ↦ 1 + ε x) x =
        p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)

Tactic:
hx

Goal state after:
p x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 + ε x) x = -x⁻¹ / log x ^ 2 →
    deriv (fun x ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x ↦ 1 + ε x) x =
      p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p x : ℝ
⊢ 0 < x →
    p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / log x ^ 2

Tactic:
hx

Goal state after:
p x : ℝ
hx : 0 < x
⊢ p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / log x ^ 2
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
hp : p = 0
x : ℝ
⊢ deriv (fun x ↦ 1 - ε x) x = x⁻¹ / log x ^ 2 → 1 < x → ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖ = x⁻¹ / log x ^ 2

Tactic:
hx

Goal state after:
p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x ↦ 1 - ε x) x = x⁻¹ / log x ^ 2
⊢ 1 < x → ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖ = x⁻¹ / log x ^ 2
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

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

Tactic:
hx

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

Goal state before:
pp: p : ℝ
hp : p = 0
x : ℝ
⊢ deriv (fun x ↦ 1 + ε x) x = -x⁻¹ / log x ^ 2 → 1 < x → ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖ = x⁻¹ / log x ^ 2

Tactic:
hx

Goal state after:
p : ℝ
hp : p = 0
x : ℝ
hx : deriv (fun x ↦ 1 + ε x) x = -x⁻¹ / log x ^ 2
⊢ 1 < x → ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖ = x⁻¹ / log x ^ 2
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

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

Tactic:
hx

Goal state after:
p : ℝ
hp : p = 0
h₁ : (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z ↦ z⁻¹ / log z ^ 2
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ log 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)
x : ℝ
⊢ x ≠ 0 →
    1 < x →
      deriv (fun x ↦ x ^ p a b * (1 - ε x)) x =
        deriv (fun z ↦ z ^ p a b) x * (1 - ε x) + x ^ p a b * deriv (fun z ↦ 1 - ε z) x

Tactic:
hx

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)
x : ℝ
hx : x ≠ 0
⊢ 1 < x →
    deriv (fun x ↦ x ^ p a b * (1 - ε x)) x =
      deriv (fun z ↦ z ^ p a b) x * (1 - ε x) + x ^ p a b * deriv (fun z ↦ 1 - ε z) 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)
x : ℝ
⊢ 0 < x → x ^ p a b * x⁻¹ = x ^ (p a b - 1)

Tactic:
hx

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)
x : ℝ
hx : 0 < x
⊢ x ^ p a b * x⁻¹ = x ^ (p a b - 1)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
⊢ (∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) → 0 ≤ x → 0 ≤ f x

Tactic:
hx

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ 0 ≤ x → 0 ≤ f x
Module: Mathlib.Computability.AkraBazzi.SumTransform

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

Tactic:
hx

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 - ε x) x = (-deriv ε) x
Module: Mathlib.Computability.AkraBazzi.SumTransform

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

Tactic:
hx

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 + ε x) x = deriv ε x
Module: Mathlib.Computability.AkraBazzi.SumTransform

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

Tactic:
hx

Goal state after:
x : ℝ
hx : 1 < x
⊢ deriv (fun x ↦ 1 - ε x) x = -deriv ε x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
⊢ (∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) → 0 ≤ x → f x ≤ 0

Tactic:
hx

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ 0 ≤ x → f x ≤ 0
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
⊢ f x ≠ 0 → 0 ≠ f x

Tactic:
hx

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
hx : f x ≠ 0
⊢ 0 ≠ f x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
⊢ (∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) →
    ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)

Tactic:
hx

Goal state after:
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
⊢ 0 ≤ f x → f x = |f x|

Tactic:
hx

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
hx : 0 ≤ f x
⊢ f x = |f 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)
x : ℝ
⊢ x ≠ 0 →
    1 < x →
      deriv (fun x ↦ x ^ p a b * (1 + ε x)) x =
        deriv (fun z ↦ z ^ p a b) x * (1 + ε x) + x ^ p a b * deriv (fun z ↦ 1 + ε z) x

Tactic:
hx

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)
x : ℝ
hx : x ≠ 0
⊢ 1 < x →
    deriv (fun x ↦ x ^ p a b * (1 + ε x)) x =
      deriv (fun z ↦ z ^ p a b) x * (1 + ε x) + x ^ p a b * deriv (fun z ↦ 1 + ε z) x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

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

Tactic:
rw [← iff_eventuallyEq hmain]

Goal state after:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hmain : f =ᶠ[atTop] fun x ↦ |f x|
⊢ GrowsPolynomially f
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
x : ℝ
⊢ f x ≤ 0 → (-f) x = |f x|

Tactic:
hx

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
x : ℝ
hx : f x ≤ 0
⊢ (-f) x = |f x|
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 fun x ↦ |f x|

Tactic:
rw [← iff_eventuallyEq hmain]

Goal state after:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun x ↦ |f x|
⊢ GrowsPolynomially (-f)
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)
x : ℝ
⊢ 0 < x → x ^ p a b * x⁻¹ = x ^ (p a b - 1)

Tactic:
hx

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)
x : ℝ
hx : 0 < x
⊢ x ^ p a b * x⁻¹ = x ^ (p a b - 1)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
⊢ ∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (c₁ / 3 * (f x + g x)) (3 * c₂ * (f x + g x))

Tactic:
have hx_lb : 1 / 2 * f x ≤ f x + g x := by
      calc f x + g x ≥ f x - ‖g x‖ := by
                rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le (g x)
           _ ≥ f x - 1 / 2 * f x := by gcongr
           _ = 1 / 2 * f x := by ring

Goal state after:
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
⊢ ∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (c₁ / 3 * (f x + g x)) (3 * c₂ * (f x + g x))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
⊢ 1 / 2 * ‖f u‖ = 1 / 2 * f u

Tactic:
by congr; simp only [norm_eq_abs, abs_eq_self, hfu_nonneg]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: 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 : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
n x✝ : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) cf (Nat.pair a m)
              if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x✝
h :
  ∃ a,
    evaln (k + 1) cf n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x✝
x : ℕ
⊢ (if x = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x✝ →
    (if x = 0 then some (unpair n).2 else evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x✝

Tactic:
by_cases x0 : x = 0 <;> simp [x0]

Goal state after:
case neg
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 : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
n x✝ : ℕ
h✝ :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) cf (Nat.pair a m)
              if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x✝
h :
  ∃ a,
    evaln (k + 1) cf n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x✝
x : ℕ
x0 : ¬x = 0
⊢ evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x✝ →
    evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)) = some x✝
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 y : ℕ
hy : y ∈ 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 y)) →
    ∃ 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

Tactic:
hx

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 y : ℕ
hy : y ∈ Nat.rec (cf.eval n₁) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m
hx : x ∈ cg.eval (Nat.pair n₁ (Nat.pair m y))
⊢ ∃ 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.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ f u - ‖g u‖ ≥ f u + 1 / 2 * f u

Tactic:
rw [sub_eq_add_neg]
                  gcongr
                  refine le_of_neg_le_neg ?_
                  rwa [neg_neg, ← neg_mul, ← neg_div]

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
⊢ x ∈ l → x ∈ m∗ * n

Tactic:
hx

Goal state after:
case a
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
x : List α
hx : x ∈ l
⊢ x ∈ m∗ * n
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l m : Language α
⊢ (l * m).reverse = m.reverse * l.reverse

Tactic:
simp only [mul_def, reverse_eq_image, image2_image_left, image2_image_right, image_image2,
    List.reverse_append]

Goal state after:
α : Type u_1
l m : Language α
⊢ image2 (fun a b ↦ b.reverse ++ a.reverse) l m = image2 (fun a b ↦ a.reverse ++ b.reverse) m l