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

Goal state before:
pp: case zero
β : 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)
hi : 0 ≤ m b + 1
⊢ graph b 0 = List.map (fun x ↦ (x, f x)) (bindList b (m b + 1 - 0))

Tactic:
symm

Goal state after:
case zero
β : 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)
hi : 0 ≤ m b + 1
⊢ List.map (fun x ↦ (x, f x)) (bindList b (m b + 1 - 0)) = graph b 0
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case comp
n : ℕ
f : List.Vector ℕ n → ℕ
m✝ n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
g✝ : Fin n✝ → List.Vector ℕ m✝ → ℕ
a✝¹ : Primrec' f✝
a✝ : ∀ (i : Fin n✝), Primrec' (g✝ i)
hf : Primrec f✝
hg : ∀ (i : Fin n✝), Primrec (g✝ i)
⊢ Primrec fun a ↦ f✝ (ofFn fun i ↦ g✝ i a)

Tactic:
exact hf.comp (.vector_ofFn fun i => hg i)

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

Goal state before:
pp: n : ℕ
⊢ n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n

Tactic:
symm

Goal state after:
n : ℕ
⊢ Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n = n.sqrt
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
⊢ 1 ≤ 2 * 2

Tactic:
decide

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
⊢ 0 < 4

Tactic:
decide

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

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

Tactic:
filter_upwards [eventually_deriv_one_add_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos

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

Goal state before:
pp: case neg.inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
refine Or.inr (Or.inl ?_)

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

Goal state before:
pp: c x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo 0 1
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (x✝¹ * x) x, (fun x ↦ c) u ∈ Set.Icc (1 * (fun x ↦ c) x) (1 * (fun x ↦ c) x)

Tactic:
filter_upwards [] with x

Goal state after:
c x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo 0 1
x : ℝ
⊢ ∀ u ∈ Set.Icc (x✝¹ * x) x, c ∈ Set.Icc (1 * c) (1 * c)
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
⊢ ‖g x‖ ≤ 1 / 2 * f x

Tactic:
calc ‖g x‖ ≤ 1 / 2 * ‖f x‖ := hfg' x hbx
           _ = 1 / 2 * f x := by congr; exact norm_of_nonneg (hf₂ _ hbx)

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case prec
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 x : ℕ
⊢ x ∈
      Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
        (unpair n).2 →
    ∃ k,
      n ≤ k ∧
        Nat.rec (evaln (k + 1) cf (unpair n).1)
            (fun n_1 n_ih ↦
              (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
                evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
            (unpair n).2 =
          some x

Tactic:
generalize n.unpair.1 = n₁

Goal state after:
case prec
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 x n₁ : ℕ
⊢ x ∈ Nat.rec (cf.eval n₁) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) (unpair n).2 →
    ∃ 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)))
            (unpair n).2 =
          some x
Module: Mathlib.Computability.ContextFreeGrammar

Goal state before:
pp: T : Type u_1
N : Type u_2
⊢ reverse ∘ reverse = id

Tactic:
ext : 1; simp

Goal state after:
Module: Mathlib.Computability.DFA

Goal state before:
pp: case refine_3
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ List.drop (↑n) (List.take (↑m) x) ≠ []

Tactic:
intro h
    have hlen' := congr_arg List.length h
    simp only [List.length_drop, List.length, List.length_take] at hlen'
    omega

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

Goal state before:
pp: m k : ℕ
⊢ (m + 1) * (2 ^ k * 2) = (m + 1) * 2 ^ (k + 1)

Tactic:
Nat.pow_succ

Goal state after:
m k : ℕ
⊢ (m + 1) * (2 ^ k * 2) = (m + 1) * (2 ^ k * 2)
Module: Mathlib.Data.Nat.Size

Goal state before:
pp: m k : ℕ
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * 2 ^ (k + 1)

Tactic:
rw [shiftLeft', bit_val, Bool.toNat_true, Nat.add_assoc, ← Nat.mul_add_one,
      shiftLeft'_true_eq_mul_pow m k, Nat.mul_left_comm, Nat.mul_comm 2, Nat.pow_succ]

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

Goal state before:
pp: case succ
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

Tactic:
by_cases s0 : shiftLeft' b m n = 0

Goal state after:
case pos
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

case neg
b : Bool
m n : ℕ
IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : ¬shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun x ↦ (f x)⁻¹

Tactic:
by
  cases hf.eventually_atTop_zero_or_pos_or_neg with
  | inl hf' =>
    refine fun b hb => ⟨1, by simp, 1, by simp, ?_⟩
    have hb_pos := hb.1
    filter_upwards [hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x hx hx'
    intro u hu
    simp only [hx, inv_zero, mul_zero, Set.Icc_self, Set.mem_singleton_iff, hx' u hu.1]
  | inr hf_pos_or_neg =>
    suffices GrowsPolynomially fun x => |(f x)⁻¹| by
      cases hf_pos_or_neg with
      | inl hf' =>
        have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => |(f x)⁻¹| := by
          filter_upwards [hf'] with x hx₁
          rw [abs_of_nonneg (inv_nonneg_of_nonneg (le_of_lt hx₁))]
        rwa [iff_eventuallyEq hmain]
      | inr hf' =>
        have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹| := by
          filter_upwards [hf'] with x hx₁
          simp [abs_of_nonpos (inv_nonpos.mpr (le_of_lt hx₁))]
        rw [iff_eventuallyEq hmain]
        exact this.neg
    have hf' : ∀ᶠ x in atTop, f x ≠ 0 := by
      cases hf_pos_or_neg with
      | inl H => filter_upwards [H] with _ hx; exact (ne_of_lt hx).symm
      | inr H => filter_upwards [H] with _ hx; exact (ne_of_gt hx).symm
    simp only [abs_inv]
    have hf := hf.abs
    intro b hb
    have hb_pos := hb.1
    obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf b hb
    refine ⟨c₂⁻¹, by change 0 < c₂⁻¹; positivity, ?_⟩
    refine ⟨c₁⁻¹, by change 0 < c₁⁻¹; positivity, ?_⟩
    filter_upwards [hf, hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x hx hx' hx''
    intro u hu
    have h₁ : 0 < |f u| := by rw [abs_pos]; exact hx'' u hu.1
    refine ⟨?lb, ?ub⟩
    case lb =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).2
    case ub =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).1

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

Goal state before:
pp: m n : ℕ
h : m.size ≤ n
⊢ 2 > 0

Tactic:
decide

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

Goal state before:
pp: f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
x✝ : ℝ
⊢ f x✝ / g x✝ = f x✝ * (g x✝)⁻¹

Tactic:
rw [div_eq_mul_inv]

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

Goal state before:
pp: n : ℕ
⊢ 1 ≠ 0

Tactic:
decide

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

Goal state before:
pp: case bit.bit
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap f) m n = bitwise f n m
bn : Bool
n : ℕ
hn : n = 0 → bn = true
a✝ : bitwise (swap f) (bit bm m) n = bitwise f n (bit bm m)
⊢ bit (swap f bm bn) (bitwise (swap f) m n) = bit (f bn bm) (bitwise f n m)

Tactic:
ihm

Goal state after:
case bit.bit
f : Bool → Bool → Bool
bm : Bool
m : ℕ
hm : m = 0 → bm = true
ihm : ∀ (n : ℕ), bitwise (swap f) m n = bitwise f n m
bn : Bool
n : ℕ
hn : n = 0 → bn = true
a✝ : bitwise (swap f) (bit bm m) n = bitwise f n (bit bm m)
⊢ bit (swap f bm bn) (bitwise f n m) = bit (f bn bm) (bitwise f n m)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i ≠ true ∧ b.testBit i ≠ true ∧ c.testBit i ≠ true
⊢ v.testBit i ≠ true

Tactic:
Bool.eq_false_eq_not_eq_true

Goal state after:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i = false ∧ b.testBit i = false ∧ c.testBit i = false
⊢ v.testBit i = false
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.prec
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      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 (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Nat.rec
      (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' + 1) (encode (cf.prec cg)))))
        (k' + 1, cf) (unpair n).1)
      (fun n_1 n_ih ↦
        (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' + 1) (encode (cf.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun i ↦
          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' + 1) (encode (cf.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    Nat.rec (evaln (k' + 1) cf (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2

Tactic:
hg (Nat.pair_lt_pair_right _ lf)

Goal state after:
case succ.prec
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      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 (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Nat.rec (evaln k cf (unpair n).1)
      (fun n_1 n_ih ↦
        (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' + 1) (encode (cf.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun i ↦
          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' + 1) (encode (cf.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    Nat.rec (evaln (k' + 1) cf (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case succ.rfind'
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      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 cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ ((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' + 1) (encode cf.rfind'))))
          (k' + 1, cf) n).bind
      fun x ↦
      Nat.rec (some (unpair n).2)
        (fun n_1 n_ih ↦
          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' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x) =
    (evaln (k' + 1) cf n).bind fun a ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))

Tactic:
hg (Nat.pair_lt_pair_right _ lf)

Goal state after:
case succ.rfind'
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      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 cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ ((evaln k cf n).bind fun x ↦
      Nat.rec (some (unpair n).2)
        (fun n_1 n_ih ↦
          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' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x) =
    (evaln (k' + 1) cf n).bind fun a ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
⊢ (∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖) →
    (∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)) →
      0 ≤ x → ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)

Tactic:
h_ub

Goal state after:
f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃
h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹
c₂_cancel : c₂⁻¹ * c₂ = 1
c₁_cancel : c₁⁻¹ * c₁ = 1
x : ℝ
hf_pos : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
h_lb : ∀ (y : ℝ), b * id x ≤ y → c₁ * ‖g y‖ ≤ ‖f y‖
h_ub : ∀ (y : ℝ), b * id x ≤ y → ‖f y‖ ≤ c₂ * ‖g y‖
⊢ (∀ (y : ℝ), b * id x ≤ y → ∀ u ∈ Set.Icc (b * y) y, ‖g u‖ ∈ Set.Icc (c₃ * ‖g y‖) (c₄ * ‖g y‖)) →
    0 ≤ x → ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * c₂⁻¹ * c₃ * f x) (c₂ * c₄ * c₁⁻¹ * f x)
Module: Mathlib.Computability.EpsilonNFA

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

Tactic:
List.replicate_add,

Goal state after:
case h
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
n : ℕ
h✝ : M.IsPath s₁ s✝ (List.replicate n none)
⊢ M.IsPath s₁ t✝ (List.replicate n none ++ List.replicate 1 none)
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate (n✝ + 1) none)
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
List.replicate_add,

Goal state after:
case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate n✝ none ++ List.replicate 1 none)
⊢ s₂ ∈ M.εClosure {s₁}
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: x✝¹ x✝ : Num
⊢ x✝¹ + x✝ = x✝ + x✝¹

Tactic:
by simp_rw [← to_nat_inj, add_to_nat, add_comm]

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

Goal state before:
pp: x✝ : Num
⊢ 1 * x✝ = x✝

Tactic:
rw [← to_nat_inj, mul_to_nat, cast_one, one_mul]

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

Goal state before:
pp: ⊢ 0 ≤ 1

Tactic:
decide

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
decide

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

Goal state before:
pp: n : PosNum
⊢ (↑n.pred').succ = ↑n

Tactic:
rw [pred'_to_nat n, Nat.succ_pred_eq_of_pos (to_nat_pos n)]

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

Goal state before:
pp: n : PosNum
⊢ ↑n.bit0.size = n.bit0.natSize

Tactic:
rw [size, succ_to_nat, natSize, size_eq_natSize n]

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

Goal state before:
pp: n : PosNum
⊢ ↑n.bit1.size = n.bit1.natSize

Tactic:
rw [size, succ_to_nat, natSize, size_eq_natSize n]

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

Goal state before:
pp: n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ ↑zero
⊢ ¬1 ≤ ↑zero

Tactic:
decide

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

Goal state before:
pp: case lt
m n : PosNum
⊢ Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt

Tactic:
decide

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

Goal state before:
pp: case eq
m n : PosNum
⊢ Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt

Tactic:
decide

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

Goal state before:
pp: case gt
m n : PosNum
⊢ Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt

Tactic:
decide

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

Goal state before:
pp: case lt
m n : Num
⊢ Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt

Tactic:
decide

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

Goal state before:
pp: case eq
m n : Num
⊢ Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt

Tactic:
decide

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

Goal state before:
pp: case gt
m n : Num
⊢ Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt

Tactic:
decide

Goal state after:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i : Fin n
⊢ Partrec' (Fin.cases f (fun i v ↦ ↑(some (v.get i))) i.succ)

Tactic:
by simpa using! prim (Nat.Primrec'.get i)

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

Goal state before:
pp: case refine_2
Γ : Type ?u.5
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : ¬l₁.length ≤ l₂.length
h' : BlankExtends l₁ l₂
⊢ BlankExtends l₂ l₁

Tactic:
exact (BlankExtends.refl _).above_of_le h' (le_of_not_ge hl)

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
⊢ ∀ (l : ListBlank Γ), cons l.head l.tail = l

Tactic:
apply Quotient.ind'
  refine fun l ↦ Quotient.sound' (Or.inr ?_)
  cases l
  · exact ⟨1, rfl⟩
  · rfl

Goal state after: