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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] [] = List.map (g a) []

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
head✝ : β
tail✝ : List β
tail_ih✝ : List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] tail✝ = List.map (g a) tail✝
⊢ List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (head✝ :: tail✝) =
    List.map (g a) (head✝ :: tail✝)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
⊢ List.foldr (fun b s ↦ b ++ s) [] [] = [].flatten

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : List.foldr (fun b s ↦ b ++ s) [] tail✝ = tail✝.flatten
⊢ List.foldr (fun b s ↦ b ++ s) [] (head✝ :: tail✝) = (head✝ :: tail✝).flatten

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
⊢ List.foldr (fun b s ↦ s + 1) 0 [] = [].length

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun b s ↦ s + 1) 0 tail✝ = tail✝.length
⊢ List.foldr (fun b s ↦ s + 1) 0 (head✝ :: tail✝) = (head✝ :: tail✝).length

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ ↑(encode (Option.map f (decode n))).ppred = (↑(decode n)).bind fun a ↦ Part.some (encode (f a))

Tactic:
cases decode (α := α) n

Goal state after:
case none
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ ↑(encode (Option.map f Option.none)).ppred = (↑Option.none).bind fun a ↦ Part.some (encode (f a))

case some
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
val✝ : α
⊢ ↑(encode (Option.map f (Option.some val✝))).ppred = (↑(Option.some val✝)).bind fun a ↦ Part.some (encode (f a))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
i : ℕ
hi : i ≤ m b + 1
bindList_m_lt : ∀ (k : ℕ), ∀ b' ∈ bindList b k, m b' < m b + 1 - k
⊢ ∀ (a : β), a ∉ bindList b (m b + 1)

Tactic:
intro b'

Goal state after:
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
i : ℕ
hi : i ≤ m b + 1
bindList_m_lt : ∀ (k : ℕ), ∀ b' ∈ bindList b k, m b' < m b + 1 - k
b' : β
⊢ b' ∉ bindList b (m b + 1)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
⊢ ((Nat.pair <$> (↑(decode n)).bind fun a ↦ map encode (↑f a)) <*> (↑(decode n)).bind fun a ↦ map encode (↑g a)) =
    (↑(decode n)).bind fun a ↦ map encode ((↑fun a ↦ (f a, g a)) a)

Tactic:
cases decode (α := α) n

Goal state after:
case none
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
⊢ ((Nat.pair <$> (↑Option.none).bind fun a ↦ map encode (↑f a)) <*> (↑Option.none).bind fun a ↦ map encode (↑g a)) =
    (↑Option.none).bind fun a ↦ map encode ((↑fun a ↦ (f a, g a)) a)

case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
val✝ : α
⊢ ((Nat.pair <$> (↑(Option.some val✝)).bind fun a ↦ map encode (↑f a)) <*>
      (↑(Option.some val✝)).bind fun a ↦ map encode (↑g a)) =
    (↑(Option.some val✝)).bind fun a ↦ map encode ((↑fun a ↦ (f a, g a)) a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
⊢ Part.none = (↑(decode n)).bind fun a ↦ map encode ((fun x ↦ Part.none) a)

Tactic:
cases decode (α := α) n

Goal state after:
case none
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
⊢ Part.none = (↑Option.none).bind fun a ↦ map encode ((fun x ↦ Part.none) a)

case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
val✝ : α
⊢ Part.none = (↑(Option.some val✝)).bind fun a ↦ map encode ((fun x ↦ Part.none) a)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := ⋯
bindList : β → ℕ → List β := ⋯
graph : β → ℕ → List (β × σ) := ⋯
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph : ∀ {bs bs' : List β}, bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph (graph b i) (l b')))) (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
i : ℕ
ih : i ≤ m b + 1 → graph b i = List.map (fun x ↦ (x, f x)) (bindList b (m b + 1 - i))
hi : i + 1 ≤ m b + 1
⊢ ∀ x ∈ bindList b (m b - i),
    Option.map (fun x_1 ↦ (x, x_1))
        (g x (mapGraph (List.map (fun x ↦ (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l x))) =
      some (x, f x)

Tactic:
intro b'

Goal state after:
case succ
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph : ∀ {bs bs' : List β}, bs' ⊆ bs → mapGraph (List.map (fun x ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph (graph b i) (l b')))) (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
i : ℕ
ih : i ≤ m b + 1 → graph b i = List.map (fun x ↦ (x, f x)) (bindList b (m b + 1 - i))
hi : i + 1 ≤ m b + 1
b' : β
⊢ b' ∈ bindList b (m b - i) →
    Option.map (fun x ↦ (b', x))
        (g b' (mapGraph (List.map (fun x ↦ (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l b'))) =
      some (b', f b')
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case zero
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ Part.some (h a (y, i))) 0 =
    Part.some (Nat.rec (g a) (fun y IH ↦ h a (y, IH)) 0)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case succ
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
n✝ : ℕ
a✝ :
  Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ Part.some (h a (y, i))) n✝ =
    Part.some (Nat.rec (g a) (fun y IH ↦ h a (y, IH)) n✝)
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ Part.some (h a (y, i))) (n✝ + 1) =
    Part.some (Nat.rec (g a) (fun y IH ↦ h a (y, IH)) (n✝ + 1))

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec' f
hg : Vec g
i : Fin m.succ
⊢ Primrec' fun v ↦ ((fun v ↦ f v ::ᵥ g v) v).get 0

Tactic:
simp [*]

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

Goal state before:
pp: p : ℝ
⊢ (deriv fun x ↦ x ^ p * (1 + ε x)) =ᶠ[atTop] fun x ↦
    deriv (fun x ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun x ↦ 1 + ε x) x

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx
      rw [deriv_fun_mul]
      · exact differentiableAt_rpow_const_of_ne _ (by positivity)
      · exact differentiableAt_one_add_smoothingFn hx

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

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ 2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊ - 1) * x₀ ≤ x

Tactic:
rw [← le_div_iff₀ x₀_pos]

Goal state after:
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ 2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊ - 1) ≤ x / x₀
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: case ind
α : 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
x✝ : n < R.n₀ ∨ R.n₀ ≤ n
⊢ 0 < T n

Tactic:
cases lt_or_ge n R.n₀ with

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

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ (b : ℝ), n₀ ≤ b → ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∀ n ≥ 1,
    (∀ z ∈ Set.Ico (max n₀ 2) (2 ^ n * max n₀ 2), f z = f (max n₀ 2)) →
      ∀ z ∈ Set.Ico (2 ^ n * max n₀ 2) (2 ^ (n + 1) * max n₀ 2), f z = f (max n₀ 2)

Tactic:
intro n _ _ z _

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ (b : ℝ), n₀ ≤ b → ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
a✝² : n ≥ 1
a✝¹ : ∀ z ∈ Set.Ico (max n₀ 2) (2 ^ n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
a✝ : z ∈ Set.Ico (2 ^ n * max n₀ 2) (2 ^ (n + 1) * max n₀ 2)
⊢ f z = f (max n₀ 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
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ ↑n ^ p a b * #(Ico (r i n) n) • (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)) =
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1))

Tactic:
nsmul_eq_mul,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ ↑n ^ p a b * (↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1))) =
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1))
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₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ p a b * #(Ico (r i n) n) • (c₂ * g ↑n / ↑n ^ (p a b + 1)) =
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑n ^ (p a b + 1))

Tactic:
nsmul_eq_mul,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ p a b * (↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑n ^ (p a b + 1))) =
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑n ^ (p a b + 1))
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₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ ↑n ^ p a b * #(Ico (r i n) n) • (c₂ * g ↑n / ↑n ^ (p a b + 1)) =
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑n ^ (p a b + 1))

Tactic:
nsmul_eq_mul,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ ↑n ^ p a b * (↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑n ^ (p a b + 1))) =
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑n ^ (p a b + 1))
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₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ p a b * #(Ico (r i n) n) • (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)) =
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1))

Tactic:
nsmul_eq_mul,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
c₃ : ℝ
hc₃_mem : c₃ ∈ Set.Ioo 0 1
hc₃ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hc₁_pos : 0 < c₁
hc₃' : 0 < 1 - c₃
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, c₂ * g ↑n ≤ g u
hn₃ : ∀ (i : α), ↑(r i n) ≤ c₃ * ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : p a b + 1 < 0
⊢ ↑n ^ p a b * (↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1))) =
    ↑n ^ p a b * ↑(#(Ico (r i n) n)) * (c₂ * g ↑n / ↑(r i n) ^ (p a b + 1))
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
⊢ S.flatten = (filter (fun l ↦ !l.isEmpty) S).flatten

Tactic:
simp [List.flatten_filter_not_isEmpty]

Goal state after:
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Language α
⊢ (map f) (⨆ i, l ^ i) = ⨆ i, (map f) l ^ i

Tactic:
← map_pow

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
l : Language α
⊢ (map f) (⨆ i, l ^ i) = ⨆ i, (map f) (l ^ i)
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
a : List α
⊢ a.reverse ∈ l.reverse ↔ a ∈ l

Tactic:
mem_reverse,

Goal state after:
α : Type u_1
l : Language α
a : List α
⊢ a.reverse.reverse ∈ l ↔ a ∈ l
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: case tail
T : Type u_1
g : ContextFreeGrammar T
v w p b✝ c✝ : List (Symbol T g.NT)
a✝ : Relation.ReflTransGen g.Produces v b✝
last : g.Produces b✝ c✝
ih : g.Derives (p ++ v) (p ++ b✝)
⊢ g.Derives (p ++ v) (p ++ c✝)

Tactic:
exact ih.trans_produces <| last.append_left p

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Derives v w
p : List (Symbol T g.NT)
⊢ g.Derives (p ++ v) (p ++ w)

Tactic:
induction hvw with

Goal state after:
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Derives v w
p : List (Symbol T g.NT)
⊢ g.Derives (v ++ p) (w ++ p)

Tactic:
induction hvw with

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

Goal state before:
pp: f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (x % 2 = 1) = x.bodd

Tactic:
simp only [mod_two_of_bodd]

Goal state after:
f : Bool → Bool → Bool
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
x : ℕ
⊢ decide (x.bodd.toNat = 1) = x.bodd
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
c : Code
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
k₁ : ℕ
c₁ : Code
n₁ : ℕ
hl : Nat.pair k₁ (encode c₁) < Nat.pair k (encode c)
⊢ lup
      (List.map (fun n ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
        (List.range (Nat.pair k (encode c))))
      (k₁, c₁) n₁ =
    evaln k₁ c₁ n₁

Tactic:
simp [lup, List.getElem?_range hl, evaln_map, Bind.bind, Option.bind_map]

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

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

Tactic:
land_comm,

Goal state after:
n i : ℕ
⊢ n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case nil
α : Type u_1
⊢ [].length = (filter Option.isSome []).length

Tactic:
filter_nil,

Goal state after:
case nil
α : Type u_1
⊢ [].length = [].length
Module: Mathlib.Computability.NFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
⊢ a :: x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ a :: x ∈ M.acceptsFrom S ∧ p

Tactic:
have h : M.stepSet {s ∈ S | p} a = {s ∈ M.stepSet S a | p} := by
      ext s; simp only [stepSet, mem_ofPred_eq, mem_iUnion, exists_prop]; tauto

Goal state after:
case cons
α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
h : M.stepSet {s | s ∈ S ∧ p} a = {s | s ∈ M.stepSet S a ∧ p}
⊢ a :: x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ a :: x ∈ M.acceptsFrom S ∧ p
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
subst t

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