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

Goal state before:
pp: case pair
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), (fun n ↦ pair (f n) (g n)) n < ack m n

Tactic:
| @pair f g hf hg IHf IHg =>

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: ⊢ Primrec pappAck.step

Tactic:
by
  apply_rules
    [Code.primrec₂_curry.comp, Code.primrec₂_prec.comp, Code.primrec₂_comp.comp,
      _root_.Primrec.id, Primrec.const]

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)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑x)

Tactic:
have h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1) := by
    refine DifferentiableOn.mul
      (DifferentiableOn.mono (differentiableOn_rpow_const _) fun z hz => ?_)
        differentiableOn_one_sub_smoothingFn
    rw [Set.mem_compl_singleton_iff]
    rw [Set.mem_Ioi] at hz
    exact ne_of_gt <| zero_lt_one.trans hz

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 : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑x)
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
⊢ ∀ (b : ℝ), max n₀ 2 ≤ b → f b = f (max n₀ 2)

Tactic:
refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step

Goal state after:
case base
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
⊢ ∀ x ∈ Set.Ico (max n₀ 2) (2 * max n₀ 2), f x = f (max n₀ 2)

case step
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)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (fun n ↦ ε (b i * ↑n) - ε ↑n) ~[atTop] fun n ↦ -log (b i) / log ↑n ^ 2

Tactic:
calc (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: g : ℝ → ℝ
α : Type u_2
inst✝ : Fintype α
a b : α → ℝ
n : ℕ
⊢ asympBound g a b n = ↑n ^ p a b * (1 + ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1))

Tactic:
simp [asympBound_def, sumTransform, mul_add, mul_one]

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

Goal state before:
pp: case bn_gt_one
α : 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
⊢ b i * ↑n ∈ Set.Ioi 1

pp: case le
α : 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
⊢ b i * ↑n ≤ ↑n

Tactic:
case bn_gt_one =>
            calc 1 = b i * (b i)⁻¹ := by rw [mul_inv_cancel₀ (by positivity)]
                _ ≤ b i * ⌈(b i)⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
                _ < b i * n := by gcongr

Goal state after:
case le
α : 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
⊢ b i * ↑n ≤ ↑n
Module: Mathlib.Computability.Language

Goal state before:
pp: case a.h.inl
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : ∀ m_1 < a.length + b.length, ∀ ⦃x : List α⦄, x ∈ l → x.length = m_1 → x ∈ m∗ * n
hx : a ++ b ∈ m * l
hal : 0 < a.length
⊢ a ++ b ∈ m∗ * n

Tactic:
specialize ih b.length (Nat.lt_add_left_iff_pos.mpr hal) hb rfl

Goal state after:
case a.h.inl
α : Type u_1
l m n : Language α
hm : [] ∉ m
h : l = m * l + n
a : List α
ha : a ∈ m
b : List α
hb : b ∈ l
ih : b ∈ m∗ * n
hx : a ++ b ∈ m * l
hal : 0 < a.length
⊢ a ++ b ∈ m∗ * n
Module: Mathlib.Computability.DFA

Goal state before:
pp: case cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : (∀ y ∈ S, y ∈ {x}) → M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, y ∈ {x}
ha : a = x
⊢ M.evalFrom (M.evalFrom s a) S.flatten = s

Tactic:
ha,

Goal state after:
case cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : M.evalFrom s x = s
a : List α
S : List (List α)
ih : (∀ y ∈ S, y ∈ {x}) → M.evalFrom s S.flatten = s
hS : ∀ y ∈ a :: S, y ∈ {x}
ha : a = x
⊢ M.evalFrom (M.evalFrom s x) S.flatten = s
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
⊢ f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)

Tactic:
have fu_nonneg : 0 ≤ f u := hf_nonneg₂ u hu.1

Goal state after:
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 ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case bit.bit
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (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
yb : Bool
y : ℕ
hyb : bit yb y ≠ 0
a✝ :
  bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 ↦
        bit (f xb b)
          (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 n))
      y
⊢ bitwise f (bit xb x) (bit yb y) =
    ⋯ ▸
      bit (f xb (bit yb y).bodd)
        (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
          (bit yb y).div2)

Tactic:
bitwise_of_ne_zero hxb hyb,

Goal state after:
case bit.bit
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (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
yb : Bool
y : ℕ
hyb : bit yb y ≠ 0
a✝ :
  bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 ↦
        bit (f xb b)
          (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 n))
      y
⊢ bit (f (bit xb x).bodd (bit yb y).bodd) (bitwise f (bit xb x / 2) (bit yb y / 2)) =
    ⋯ ▸
      bit (f xb (bit yb y).bodd)
        (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
          (bit yb y).div2)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case inl.refine_2
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 : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
j : ℕ
hj : i < j
⊢ (a ^^^ v).testBit j = a.testBit j

Tactic:
· simp only [testBit_xor, hi' _ hj, Bool.bne_false]

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

Goal state before:
pp: case inr.inl.refine_2
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 : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
j : ℕ
hj : i < j
⊢ (b ^^^ v).testBit j = b.testBit j

Tactic:
· simp only [testBit_xor, hi' _ hj, Bool.bne_false]

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

Goal state before:
pp: case inr.inr.refine_2
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 : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
j : ℕ
hj : i < j
⊢ (c ^^^ v).testBit j = c.testBit j

Tactic:
· simp only [testBit_xor, hi' _ hj, Bool.bne_false]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ Countable { f // Partrec f }

Tactic:
apply Function.Surjective.countable (f := fun c => ⟨eval c, eval_part.comp (.const c) .id⟩)
  intro ⟨f, hf⟩; simpa using! exists_code.1 hf

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

Goal state before:
pp: b : PosNum
⊢ ↑(1 + b) = ↑1 + ↑b

Tactic:
one_add b,

Goal state after:
b : PosNum
⊢ ↑b.succ = ↑1 + ↑b
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
x : List α
⊢ x ∈ (fun x ↦ a :: x) ⁻¹' M.acceptsFrom S ↔ x ∈ M.acceptsFrom (M.stepSet S a)

Tactic:
simp [cons_mem_acceptsFrom M]

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

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

Tactic:
simp only [reduceOption, filterMap, id]

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

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

Tactic:
simp only [reduceOption, filterMap, id]

Goal state after:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
⊢ (fun x_1 ↦ x ++ x_1) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.evalFrom S x)

Tactic:
by
  ext y; simp [append_mem_acceptsFrom M]

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

Goal state before:
pp: case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b

Tactic:
exact Nat.add_lt_add this this

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

Goal state before:
pp: case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a

Tactic:
exact Nat.add_lt_add this this

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ M.IsPath s t [] ↔ s = t

Tactic:
isPath_iff

Goal state after:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ (t = s ∧ [] = [] ∨ ∃ t_1 a x, t_1 ∈ M.step s a ∧ M.IsPath t_1 t x ∧ [] = a :: x) ↔ s = t
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m n : Num
⊢ (m.cmp n).swap = n.cmp m

Tactic:
cases m <;> cases n <;> try { rfl }

Goal state after:
case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case rfind
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
hf : Partrec ↑f✝
this : Partrec fun a ↦ ↑f✝ (a.2 ::ᵥ a.1)
⊢ Partrec fun v ↦ Nat.rfind fun n ↦ Part.some (decide (f✝ (n ::ᵥ v) = 0))

Tactic:
have :=
      ((Primrec.eq.decide.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp
        this).to₂.partrec₂

Goal state after:
case rfind
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
hf : Partrec ↑f✝
this✝ : Partrec fun a ↦ ↑f✝ (a.2 ::ᵥ a.1)
this : Partrec₂ fun a ↦ ↑fun b ↦ decide (id (f✝ ((a, b).2 ::ᵥ (a, b).1)) = 0)
⊢ Partrec fun v ↦ Nat.rfind fun n ↦ Part.some (decide (f✝ (n ::ᵥ v) = 0))
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b : ℕ
⊢ (∃ a ∈ Nat.rfind fun n_1 ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔
    ∃ a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome), ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
refine
        exists_congr fun a => (and_congr (iff_of_eq ?_) Iff.rfl).trans (and_congr_right fun h => ?_)

Goal state after:
case refine_1
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
⊢ (a ∈ Nat.rfind fun n_1 ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) =
    (a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome))

case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ m → List.Vector ℕ n
h : Vec f
⊢ Computable f

Tactic:
simpa only [ofFn_get] using vector_ofFn fun i => to_part (h i)

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
d₁ d₂ : ManyOneDegree
a b c d : ℕ → Prop
hl₁ : a ≤₀ b
hr₁ : b ≤₀ a
hl₂ : c ≤₀ d
hr₂ : d ≤₀ c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
of_eq_of

Goal state after:
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
d₁ d₂ : ManyOneDegree
a b c d : ℕ → Prop
hl₁ : a ≤₀ b
hr₁ : b ≤₀ a
hl₂ : c ≤₀ d
hr₂ : d ≤₀ c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
h : q₁✝ ∈ stmts₁ (branch p q₁ q₂)
hs : SupportsStmt S (branch p q₁ q₂)
⊢ SupportsStmt S q₁✝

Tactic:
simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs

Goal state after:
case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ = branch p q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S q₁✝
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : Γ → σ → Λ
h : q₁ ∈ stmts₁ (goto l)
hs : SupportsStmt S (goto l)
⊢ SupportsStmt S q₁

Tactic:
simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs

Goal state after:
case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : Γ → σ → Λ
hs : ∀ (a : Γ) (v : σ), l a v ∈ S
h : q₁ = goto l
⊢ SupportsStmt S q₁
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ halt
hs : SupportsStmt S halt
⊢ SupportsStmt S q₁

Tactic:
simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs

Goal state after:
case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
hs : True
h : q₁ = halt
⊢ SupportsStmt S q₁
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝ : Dir
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S q₁
h : q₁ ∈ stmts₁ (move a✝ q)
hs : SupportsStmt S (move a✝ q)
⊢ SupportsStmt S q₁

Tactic:
simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs

Goal state after:
case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝ : Dir
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = move a✝ q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S q₁
h : q₁ ∈ stmts₁ (write a✝ q)
hs : SupportsStmt S (write a✝ q)
⊢ SupportsStmt S q₁

Tactic:
simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs

Goal state after:
case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = write a✝ q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S q₁
h : q₁ ∈ stmts₁ (load a✝ q)
hs : SupportsStmt S (load a✝ q)
⊢ SupportsStmt S q₁

Tactic:
simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
      at h hs

Goal state after:
case load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset Λ
q₁ : Stmt Γ Λ σ
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → SupportsStmt S q → SupportsStmt S q₁
hs : SupportsStmt S q
h : q₁ = load a✝ q ∨ q₁ ∈ stmts₁ q
⊢ SupportsStmt S q₁
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
⊢ SupportsStmt S (branch p q₁' q₂') → (stepAux (branch p q₁' q₂') v T).l ∈ Finset.insertNone S

Tactic:
intro hs

Goal state after:
case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (stepAux (branch p q₁' q₂') v T).l ∈ Finset.insertNone S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a✝ : Γ → σ → Λ
v : σ
T : Tape Γ
⊢ SupportsStmt S (goto a✝) → (stepAux (goto a✝) v T).l ∈ Finset.insertNone S

Tactic:
intro hs

Goal state after:
case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a✝ : Γ → σ → Λ
v : σ
T : Tape Γ
hs : SupportsStmt S (goto a✝)
⊢ (stepAux (goto a✝) v T).l ∈ Finset.insertNone S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
⊢ SupportsStmt S halt → (stepAux halt v T).l ∈ Finset.insertNone S

Tactic:
intro hs

Goal state after:
case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
hs : SupportsStmt S halt
⊢ (stepAux halt v T).l ∈ Finset.insertNone S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a✝ : Dir
q : Stmt Γ Λ σ
IH : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q → (stepAux q v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
⊢ SupportsStmt S (move a✝ q) → (stepAux (move a✝ q) v T).l ∈ Finset.insertNone S

Tactic:
intro hs

Goal state after:
case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a✝ : Dir
q : Stmt Γ Λ σ
IH : ∀ (v : σ) (T : Tape Γ), SupportsStmt S q → (stepAux q v T).l ∈ Finset.insertNone S
v : σ
T : Tape Γ
hs : SupportsStmt S (move a✝ q)
⊢ (stepAux (move a✝ q) v T).l ∈ Finset.insertNone S